Моделирование и верификация подсистемы управления доступом средства защиты информации Аккорд-Х

Введение

Подсистема управления доступом операционной системы  представляет собой средство защиты информации (СЗИ), содержащее большой объем исполняемого кода. По мере появления новых требований к таким СЗИ их сложность и объемы исполняемого кода возрастают. Это, как правило, приводит к появлению новых угроз безопасности и уязвимостей, которые чаще всего связаны с ошибками проектирования таких средств защиты. Во избежание данной проблемы при разработке подсистем управления доступом любой операционной системы (ОС), в том числе и ОС Linux, необходимо предварительно проводить моделирование их механизмов защиты. Для этого разрабатывают модели безопасности компьютерных систем [1-3]. Требования к разработке моделей безопасности регламентируются рядом нормативных документов [4-8]. Данные требования предназначены для компаний-разработчиков средств защиты информации, и их выполнение является обязательным при проведении работ по сертификации СЗИ в ФСТЭК России. В соответствии с требованиями нормативных документов в разрабатываемой модели безопасности средств управления доступом должны быть отражены реализуемые политики управления доступом и фильтрации информационных потоков. При этом для подтверждения корректности модели безопасности, и, тем самым, корректности работы СЗИ в части отсутствия логических ошибок в разграничении доступа, необходимо подтверждать соответствие модели заявленным требованиям. Наиболее объективным путем подтверждения соответствия модели требованиям является ее верификация с применением специальных инструментальных средств.

В данной статье рассматривается подход к верификации модели безопасности для подсистемы управления доступом, входящей в состав программно-аппаратного комплекса «Аккорд-Х» [9,10] производства компании «ОКБ САПР», а также некоторые особенности процесса верификации.

Материалы и методы

Существует множество подходов к моделированию произвольных систем или алгоритмов с целью их верификации на соответствие некоторым формально описанным свойствам [1-3,11]. В рамках данной работы был выбран подход к верификации с использованием темпоральной логики действия Лэмпорта (англ. TLA, Temporal Logic of Actions) и метода Model Checking [1-2,12,13] как наиболее доступного для понимания подхода, позволяющего в рамках формальной нотации на языке TLA+ описать все необходимые сущности и операции системы, а также свойства безопасности, необходимые для проверки во всех ее состояниях.

Моделирование на языке темпоральной логики действий Лэмпорта позволяет описывать и в дальнейшем верифицировать в автоматическом режиме системы, заданные в виде конечных автоматов [14]. В соответствии с этим при использовании данного подхода существуют некоторые ограничения на возможность верификации системы, так как метод Model Checking не осуществляет полноценную формальную верификацию системы. В соответствии с этим в рамках TLA+ нотации модели безопасности были введены модельные значения для некоторых сущностей системы: количества субъектов, объектов и пользователей. Такие ограничения на сущности системы, заданные модельными значениями, с одной стороны не могут повлиять на успешность или неуспешность верификации, а с другой – позволяют методу Model Checking завершить верификацию на этапе, когда для системы больше нет новых состояний: то есть когда все достижимые состояния уже проверены для данного количества сущностей системы.

 

В модели безопасности необходимо задать переменные – те сущности, которые будут изменяться при выполнении операций и изменение которых влечет за собой изменение состояния системы: A – множество произошедших доступов (вспомогательная переменная [15]); O – множество объектов, S – множество субъектов, U – множество учетных записей пользователей.

 

Любое изменение приведенных переменных модели переводит систему из одного состояния в другое, например, во множество произошедших доступов можно добавить новый элемент-кортеж – доступ субъекта с идентификатором s.sid к объекту с идентификатором o.oid по методу доступа r из множества Accesses:

 

Изменение тех или иных переменных модели должно описываться в операциях, которые могут выполняться в системе, и соответствующих методам доступа Accesses: чтение, запись, получение содержимого каталога, дозапись, поиск объекта, переименование объектов и контейнеров, создание и удаление пользователей, изменение прав пользователей, изменение атрибутов и уровня конфиденциальности объектов доступа, создание и удаление субъектов (процессов пользователей), удаление и создание объектов доступа.

Все операции в нотации TLA+ описываются в виде предикатов пред- и постусловий выполнения операции, например:

 

В предусловии ReadD описывается несколько предикатов соединенных операторами конъюнкции (логическое И) и дизъюнкции (логическое ИЛИ), смысл данного предусловия можно прочитать следующим образом – должны существовать субъект и объект, такие, что одновременно выполняются условия:

• либо субъект является администратором, либо должны одновременно выполняться свойства дискреционной и мандатной политик управления доступом (предикаты DAC_may_do и MAC_may_read);
• субъектом должен был быть предварительно выполнен поиск объекта доступа.

В постусловии Read(s,o) изменяется переменная с произошедшими доступами системы, а остальные переменные модели остаются неизменными.

Предикаты isUserAdmin, DAC_may_do и MAC_may_read реализованы следующим образом:

Где cl – уровень доступа субъекта или конфиденциальности объекта, ccnr – специальный атрибут, позволяющий для объекта делать исключение в рамках мандатной политики управления доступом [3].

Аналогичным образом в TLA+ нотации модели безопасности были описаны все остальные операции, соответствующие методам доступа Accesses с учетом характерных для них ограничений, в том числе дискреционного и мандатного управления доступом.

Начальное состояние системы описывается с помощью следующего предиката:

Множество произошедших доступов инициализируется пустым, в системе будут изначально существовать: две учетные записи пользователей u0 – администратор с максимальным уровнем конфиденциальности и u1 – модельный пользователь с минимальным уровнем конфиденциальности, соответствующие им субъекты-процессы s0 и s1, а также следующие объекты – корневой каталог файловой системы o0, вложенный контейнер o1 и файл этого контейнера o2. Данные модельные сущности выбраны для ускорения процесса верификации, множество объектов или субъектов может изначально быть пустым, но это приведет к значительно большему количеству состояний системы.

Условия или свойства безопасности, которые требуется описывать и проверять в рамках нотации TLA+ представляются в виде инвариантов или темпоральных свойств [12-13]. При этом в рамках данной модели безопасности за счет использования переменной истории (англ. history variable [15]) для множества всех совершенных доступов нет необходимости использовать темпоральные свойства, которые в отличие от инвариантов зависят от фактора времени и событий в прошлом или будущем. Все свойства безопасности описаны как предикаты, истинность которых проверяется в каждом возможном состоянии системы.

Для модели были описаны как инварианты, проверяющие правильность функционирования системы, так и инварианты безопасности. К первой группе относятся инварианты TypeInv (консистентность типов сущностей системы), OneAdminExists (существование в любой момент администратора системы), NoCyclesInContainers (отсутствие циклов в контейнерах). К инвариантам безопасности относятся MacSafety (невозможность существования вложенного в контейнер объекта с большим уровнем конфиденциальности), IntegrityInv (невозможность запуска измененных исполняемых файлов), LinksSafety (наследование уровня конфиденциальности всех ссылок от уровня объекта доступа).

Модель безопасности в TLA+ нотации описывается с помощью спецификации Spec, для которой задано начальное состояние Init и в дальнейшем могут выполняться различные действия из Next:

Формальное доказательство отсутствия противоречий в модели безопасности осуществляется с помощью проверки в автоматическом режиме рассмотренных ранее инвариантов в каждом возможном состоянии для спецификации Spec.

Результаты

Верификация разработанной модели проводилась с помощью инструментального средства TLC2 v2.15 на СВТ с Intel Core i5-9400 (3.80 ГГц) и объемом оперативной памяти 16 ГБ в 64-разрядной ОС Linux с ядром v5.4.38. Время, затраченное на верификацию с использованием 6 отдельных потоков, составляет от 12 минут до 24 часов в зависимости от выставленных опций верификации – проверки модели с итеративным углублением, начиная с заданной начальной глубины (опция dfid от 6 до 8). Общее количество различных проанализированных состояний – 2 776 895.

Результаты верификации описанной спецификации относительно заданных инвариантов позволяют утверждать о выполнении требований безопасности для всех возможных состояний модели управления доступом.

Верификация модели позволила выявить и устранить недостатки в реализации комплекса «Аккорд-Х», а также провести дальнейший анализ возможных скрытых каналов утечки информации при реализации мандатного управления доступом.

Заключение

В статье рассматривается подход, который был использован в процессе верификации модели безопасности для подсистемы управления доступом комплекса «Аккорд-Х». Данный подход позволил не только выполнить формальные требования существующих нормативных документов в области защиты информации, но и способствовал выявлению логических ошибок в работе подсистемы разграничения доступа, которые могли привести к нарушению конфиденциальности или целостности защищаемых данных.

Литература

1. Козачок, А. В. Спецификация модели управления доступом к разнокатегорийным ресурсам компьютерных систем // Вопросы кибербезопасности. 2018. № 4(28). С. 2–8.
2. Козачок, А. В. Спецификация модели управления доступом на языке темпоральной логики действий Лэмпорта // Труды Института системного программирования РАН. 2018. Т. 30, № С. 147–162.
3. Девянин, П. Н. [и др.]. Моделирование и верификация политик безопасности управления доступом в операционных системах. М.: Горячая линия – Телеком. 212 с.
4. Мозолина, Н. В. Формальное моделирование политики безопасности: к вопросу о стандартизации процесса // Комплексная защита информации. 2019. С. 96– 99.
5. Требования по безопасности информации, устанавливающие уровни доверия к средствам технической защиты информации и средствам обеспечения безопасности информационных технологий (выписка) [Приказ ФСТЭК России от 30 июля 2018 г. №131] – М.: ФСТЭК России, 2018. – 17 с.
6. ГОСТ Р ИСО/МЭК 15408-3-2013. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности – М.: Стандартинформ, 2014. – 152 с.
7. ГОСТ Р (проект) Защита информации. Формальное моделирование политики безопасности. Часть 1. Формальная модель управления доступом – М.: Стандартинформ, 201x. – 36 с.
8. ГОСТ Р (проект) Защита информации. Формальное моделирование политики безопасности. Часть 2. Верификация формальной модели управления доступом – М.: Стандартинформ, 201x. – 36 с.
9. Каннер А.М., Ухлинов Л.М. Управление доступом в ОС GNU/Linux // Вопросы защиты информации. 2012. № 3. С. 35–38.
10. Каннер А.М. Linux: о жизненном цикле процессов и разграничении доступа // Вопросы защиты информации. 2014. № 4. С. 37–40.
11. Klein, G. [et. al.]. seL4: formal verification of an OS kernel // Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. 2009. Pp. 207–220. DOI: https://doi.org/10.1145/1629575.1629596
12. Lamport, L. The Temporal Logic of Actions // ACM Trans. Program. Lang. Syst. 1994. Vol. 16, no. 3. Pp. 872–923. DOI: http://doi.acm.org/10.1145/177492.177726
13. Lamport, L. [et al.]. Specifying and verifying systems with TLA+ // Proceedings of the ACM SIGOPS 10th workshop. 2002. Pp. 45–48.
14. Kanner, A. M., Kanner, T. M. Testing Software and Hardware Data Security Tools Using the Automata Theory and the Graph Theory // Proceedings of Ural Symposium on Biomedical Engineering, Radioelectronics and Information Technology. 2020. Pp. 615–618.
15. Lamport, L., Merz, S. Auxiliary variables in TLA+ // arxiv.org preprint: 1703.05121. [электронный ресурс] URL: https://arxiv.org/pdf/1703.05121.pdf (дата обращения 01.09.2020)

Авторы: Каннер А. М.; Каннер(Борисова) Т. М.

Дата публикации: 14.10.2020

Библиографическая ссылка: Каннер А. М., Каннер (Борисова) Т. М. Моделирование и верификация подсистемы управления доступом средства защиты информации Аккорд-Х // Вопросы защиты информации. М., 2020. № 3. С. 6–10.

---