Подход к верификации подсистемы управления доступом операционной системы linux

В настоящее время при разработке сертифицированных подсистем управления доступом любой операционной системы, в том числе и ОС Linux, необходимо предварительно проводить моделирование их механизмов защиты. Для этого разрабатывают модели безопасности компьютерных систем [1-3]. Требования к разработке моделей безопасности регламентируются следующими нормативными документами:

1. Требования по безопасности информации, устанавливающие уровни доверия к средствам технической защиты информации и средствам обеспечения безопасности информационных технологий [4];
2. ГОСТ Р ИСО/МЭК 15408-3-2013. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности [5];
3. ГОСТ Р (проект) Защита информации. Формальное моделирование политики безопасности. Часть 1. Формальная модель управления доступом [6];
4. ГОСТ Р (проект) Защита информации. Формальное моделирование политики безопасности. Часть 2. Верификация формальной модели управления [7].

В соответствии с требованиями перечисленных нормативных документов в разрабатываемой модели безопасности средств управления доступом должны быть отражены реализуемые политики управления доступом и фильтрации информационных потоков. При этом для подтверждения корректности модели безопасности, то есть корректности работы средства защиты с точки зрения отсутствия логических ошибок в разграничении доступа, необходимо подтверждать соответствие модели заявленным требованиям. Наиболее объективным путем подтверждения соответствия модели требованиям является ее верификация с применением специальных инструментальных средств.

В настоящее время существует ряд подходов к моделированию произвольных систем или алгоритмов с целью их верификации на соответствие некоторым формально описанным свойствам. Рассмотрим один из них – подход к верификации с использованием темпоральной логики действия Лэмпорта и метода Model Checking, позволяющий в рамках формальной нотации на языке TLA+ описать все необходимые сущности и операции системы, а также свойства безопасности, необходимые для проверки во всех ее состояниях.

Моделирование на языке темпоральной логики действий Лэмпорта позволяет описывать заданные в виде конечных автоматов системы и верифицировать их в автоматическом режиме.

В рамках TLA+ нотации модели безопасности были введены модельные значения для некоторых сущностей системы: количества субъектов (Subjects), объектов (Objects) и пользователей (User). Модельные значения приведены на рисунке 1.

 

Рисунок 1 – Модельные значения сущностей системы

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

В модели безопасности в виде переменных задаются сущности, которые будут изменяться при выполнении операций и изменение которых влечет за собой изменение состояния системы. Переменные приведены на рисунке 2.

 

Рисунок 2 – Переменные модели

Где:

A – множество произошедших доступов;

O – множество объектов;

S – множество субъектов;

U – множество учетных записей пользователей.

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

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

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

 

Рисунок 3 – Начальное состояние системы

Данные модельные сущности выбраны для ускорения процесса верификации, множество объектов или субъектов может изначально быть пустым, но это приведет к значительно большему количеству состояний системы.

Условия или свойства безопасности, которые требуется описывать и проверять в рамках нотации TLA+ представляются в виде инвариантов или темпоральных свойств. При этом в рамках данной модели безопасности за счет использования переменной истории для множества всех совершенных доступов нет необходимости использовать темпоральные свойства, которые в отличие от инвариантов зависят от фактора времени и событий в прошлом или будущем. Все свойства безопасности описаны как предикаты, истинность которых проверяется в каждом возможном состоянии системы.

Для модели были описаны как инварианты, проверяющие правильность функционирования системы, так и инварианты безопасности.  Пример инварианта безопасности – MacSafety – невозможность существования вложенного в контейнер объекта с большим уровнем конфиденциальности, приведен на рисунке 4.

 

Рисунок 4 – Пример инварианта модели

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

 

Рисунок 5 – Спецификация модели

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

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

Список литературы

1. Козачок, А. В. Спецификация модели управления доступом к разнокатегорийным ресурсам компьютерных систем // Вопросы кибербезопасности. 2018. № 4(28). С. 2–8.
2. Козачок, А. В. Спецификация модели управления доступом на языке темпоральной логики действий Лэмпорта // Труды Института системного программирования РАН. 2018. Т. 30, № 5. С. 147–162.
3. Девянин, П. Н. [и др.]. Моделирование и верификация политик безопасности управления доступом в операционных системах. М.: Горячая линия – Телеком. 2019. 212 с.
4. Требования по безопасности информации, устанавливающие уровни доверия к средствам технической защиты информации и средствам обеспечения безопасности информационных технологий (выписка) [Приказ ФСТЭК России от 30 июля 2018 г. №131] – М.: ФСТЭК России, 2018. – 17 с.
5. ГОСТ Р ИСО/МЭК 15408-3-2013. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности – М.: Стандартинформ, 2014. – 152 с.
6. ГОСТ Р (проект) Защита информации. Формальное моделирование политики безопасности. Часть 1. Формальная модель управления доступом – М.: Стандартинформ, 201x. – 36 с.
7. ГОСТ Р (проект) Защита информации. Формальное моделирование политики безопасности. Часть 2. Верификация формальной модели управления доступом – М.: Стандартинформ, 201x. – 36 с.

Автор: Каннер А. М.

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

Выходные данные: 13-15 сентября 2020 года, Московская область

---