Использование TLA+ для описания модели изолированной программной среды субъектов доступа

В работах [1, 2] описана необходимость в проведении моделирования и верификации средств защиты информации (СЗИ), а также перечислены конкретные нормативные документы Российской Федерации, в которых предъявляются требования в части верификации их функций защиты. Современные инструментальные средства верификации позволяют в автоматическом режиме проверить выполнение некоторых формальных свойств при работе СЗИ. Однако еще более примечательным преимуществом средств верификации является возможность в автоматическом режиме проверять математические модели безопасности компьютерных систем.

Большинство известных формальных моделей безопасности (Белла-ЛаПадула, Харрисона-Руззо-Ульмана и др.) сформулированы в математической нотации, с использованием подходящего для этого математического аппарата. При этом основным компонентом любой формальной модели является базовая теорема безопасности, с помощью которой обосновываются некоторые формальные свойства, гарантирующие безопасность системы или обрабатываемых в ней данных.

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

В задаче проверки формальных моделей безопасности могут помочь средства верификации. Для этого математическую нотацию необходимо перевести в нотацию на некотором формальном языке, пригодном для верификации (TLA+, EventB и др.), а затем сформулировать условия базовой теоремы безопасности в виде инвариантов или темпоральных свойств. В результате это позволяет:

1. Исключить человеческий фактор при проверке модели безопасности.
2. Проводить верификацию силами менее квалифицированных специалистов (с помощью запуска средств верификации).
3. Проверять выполнение условий базовой теоремы безопасности во всевозможных состояниях моделируемой системы.
4. Выявлять скрытые ошибки в математической нотации.

В [3] автором описана первая версия математической нотации модели изолированной программной среды субъектов доступа (ИПСС), которая является развитием субъектно-ориентированной модели изолированной программной среды (ИПС) [4, 5]. В отличие от ИПС в модели ИПСС производится другая декомпозиция системы на сущности: субъектами являются пользователи и системные сервисы (а не процессы пользователей, как в ИПС), а объектами – функционально ассоциированные с этими субъектами объекты (процессы) и объекты-данные с возможностью динамического изменения их состава во времени. Отличительной особенностью модели ИПСС является учет подсистемы защиты в качестве сущности системы, такой же, как и другие субъекты системы, и обоснование невозможности нарушения действующих правил управления доступом за счет свойства абсолютной корректности (изолированности) субъектов доступа.

К сожалению, математическая нотация модели не позволяет гарантировать выполнения формальных свойств безопасности во всех возможных состояниях системы, а экспериментальные исследования реализаций этой модели на практике требуют  повторного проведения даже при малых усовершенствованиях модели. В связи с этим в [6] проведена верификация модели ИПСС с использованием темпоральной логики действий Лэмпорта (TLA+) и метода Model Checking.

Спецификация модели ИПСС в TLA+ имеет следующие компоненты:

1. Начальное состояние – инициализация системы (Init), пример предиката инициализации модели ИПСС приведен на рисунке 1.
2. Переменные модели – сущности, которые могут изменяться в процессе работы (субъекты, объекты и др.).
3. Правила работы системы – возможные состояния и значения переменных модели, правила перехода из состояния в состояние – например, при осуществлении доступов субъектов к объектам.
4. Теорема, доказываемая при верификации и проверяющая специальные предикаты (формальные свойства системы) – инварианты и темпоральные свойства.

 

Рисунок 1 – Начальное состояние системы, описывающее переменные – активные и неактивные субъекты доступа, доступные объекты доступа, последовательность доступов

В качестве действий в системе могут совершаться запросы модели ИПСС: создание и удаление процессов, создание пользователей и системных субъектов, удаление субъектов, а также чтение, запись, создание, удаление и исполнение объектов доступа. Предусловиями являются предикаты, выполнение которых необходимо для совершения действия. Постусловия определяют каким образом после выполнения действия изменяются переменные модели, то есть какое новое состояние будет иметь система. Пример одного из действий системы, описанного в виде предикатов пред- и пост-условий его выполнения приведен на рисунке 2.

При доказательстве теоремы в ходе верификации проверяется истинность специальных предикатов – инвариантов или темпоральных свойств, приведенных на рисунке 3. Инварианты должны выполняться во всех состояниях и для каждой реализации системы, а также за счет использования последовательности совершенных запросов к системе могут проверять условия, произошедшие в прошлом, например, при последнем переходе системы. Темпоральные свойства, в отличие от инвариантов, могут применять специальные темпоральные операторы TLA+ [6, 7], с помощью которых можно составлять предикаты, зависящие от времени выполнения и определенных событий в прошлом или будущем.

 

Рисунок 2 – Пост- и пред-условия для запроса на чтение объекта доступа

 

 

Рисунок 3 – Теорема, проверяемая при верификации спецификации модели ИПСС

В ходе создания TLA+ нотации модели ИПСС были выявлены скрытые ошибки, допущенные в математической нотации. Так, например, нарушались инварианты свойств корректности модели ИПСС, и один субъект мог опосредованно воздействовать на другой субъект доступа через операции порождения. Также была выявлена возможность некорректной работы самой моделируемой системы – она проходила этап инициализации, и далее в реализации было еще несколько состояний, но на определенном состоянии система переставала работать еще до появления пользователей, так как завершал работу единственный системный процесс (ядро ОС). Аналогично была выявлена ошибка с возможностью работы системы при завершении работы субъекта, разграничивающего  доступ (подсистемы управления доступом), или при удалении объекта, содержащего применяемые правила доступа.

Таким образом, при исправлении выявленных ошибок в TLA+ нотации кроме модификации свойств корректности и некоторых операций модели ИПСС были добавлены инварианты, представленные на рисунке 4:

1. OSKernelExists – инвариант для контроля работоспособности системы (постоянное наличие системного субъекта – ядра ОС).
2. SormInits – инвариант для контроля активизации подсистемы управления доступом.
3. OSUsabilityLiveness – темпоральное свойство для проверки работоспособности системы: в любой реализации системы обязательно кроме начальных системных субъектов должен активизироваться пользователь или еще один системный субъект.

 

Рисунок 4 – Дополнительные инварианты для устранения недостатков математической нотации модели ИПСС

Полный текст разработанной спецификации модели ИПСС доступен на сайте автора https://github.com/kanner/ipes-model.

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

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

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

1. Каннер А. М. Подход к верификации подсистемы управления доступом операционной системы LINUX // Комплексная защита информации: материалы XXV научно-практической конференции, 15–17 сентября 2020 г., М.: Медиа Группа «Авангард», 2020. С. 24–28.
2. Каннер А. М., Каннер Т. М. Моделирование и верификация подсистемы управления доступом средства защиты информации Аккорд-Х // Вопросы защиты информации. М., 2020. № 3. С. 6–10.
3. Kanner A.M. Correctness of Data Security Tools for Protection against Unauthorized Access and their Interaction in GNU/Linux // Global Journal of Pure and Applied Mathematics. – 2016. – Vol. 12, no. 3. – Pp. 2479–2501.
4. Щербаков, А. Ю. Современная компьютерная безопасность. Теоретические основы. Практические аспекты. М.: Книжный мир, 2009. — 352 с.
5. Щербаков, А. Ю. Хрестоматия специалиста по современной информационной безопасности. Том 1. Saarbrucken : Palmarium Academic Publishing, 2016. — 272 с.
6. Kanner A. M., Kanner T. M. Verification of a Model of the Isolated Program Environment of Subjects Using the Lamport’s Temporal Logic of Actions // Proceedings of the VII International Conference «Engineering & Telecommunication», IEEE, 2021 (in press).
7. Kanner A. M., Kanner T. M. Special Features of TLA+ Temporal Logic of Actions for Verifying Access Control Policies // Proceedings of Ural Symposium on Biomedical Engineering, Radioelectronics and Information Technology, IEEE, 2021 (manuscript submitted for publication).

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

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

Библиографическая ссылка: Каннер А. М. Использование TLA+ для описания модели изолированной программной среды субъектов доступа // Комплексная защита информации: материалы XXVI научно-практической конференции. Минск. 25–27 мая 2021 г. Минск: Издатель Владимир Сивчиков, 2021. С. 243–246.

---