Доклады, выступления, видео и электронные публикации

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

Введение

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

Существующие в настоящее время наиболее известные формальные модели безопасности, например, Белла-ЛаПадулы, сформулированы в математической нотации, с использованием некоторого математического аппарата. При этом основным компонентом таких формальных моделей является базовая теорема безопасности, с помощью которой обосновываются формальные свойства, гарантирующие безопасность системы или обрабатываемых в ней данных. Для модели Белла-ЛаПадула формальным свойством, гарантирующим безопасность данных, является невозможность возникновения информационных потоков «сверху вниз» – утечки информации с большего уровня конфиденциальности на меньший уровень конфиденциальности.

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

В связи с этим для проверки формальных моделей безопасности предлагается использовать инструментальные средства автоматической верификации, а математическую нотацию перевести в нотацию на некотором формальном языке, пригодном для верификации, например, TLA+ (англ. Temporal Logic of Actions).  На основании данной нотации можно сформулировать условия базовой теоремы безопасности в виде инвариантов или темпоральных свойств.

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

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

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

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

При этом модель ИПСС имеет следующие основные отличия от модели ИПС:

  • Осуществляется учет подсистемы защиты в качестве сущности системы, такой же, как и другие субъекты системы.
  • Приводится обоснование невозможности нарушения действующих правил управления доступом за счет свойства абсолютной корректности (изолированности) субъектов доступа.

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

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

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

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

При доказательстве теоремы в ходе верификации проверяется истинность специальных предикатов – следующих инвариантов или темпоральных свойств:

 1.png

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

При создании TLA+ нотации модели ИПСС были выявлены скрытые ошибки математической нотации:

  • Нарушаются инварианты свойств корректности модели ИПСС, и один субъект может опосредованно воздействовать на другой субъект доступа через операции порождения.
  • Существует возможность некорректной работы моделируемой системы, которая проходит этап инициализации, принимает несколько состояний и в одном из таких состоянии система перестает работать еще до появления пользователей из-за завершения работы единственного системного процесса – ядра ОС.
  • Существует возможность работы системы при завершении работы субъекта, разграничивающего доступ или при удалении объекта, содержащего применяемые правила доступа.

Данные ошибки исправлены в TLA+ нотации. Для этого выполнена модификация свойств корректности и некоторых операций модели ИПСС, а также добавлены следующие инварианты:

 2.png

Где:

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

Заключение

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

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

Литература

  1. Каннер А. М. Подход к верификации подсистемы управления доступом операционной системы Linux // Комплексная защита информации: материалы XXV научно-практической конференции, 15-17 сентября 2020 г. М.: Медиа Группа «Авангард». 2020. С. 24-28.
  2. Каннер А. М., Каннер Т. М. Моделирование и верификация подсистемы управления доступом средства защиты информации Аккорд-Х // Вопросы защиты информации. М., 2020. № 3. С. 6-
  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. V. 12, no. 3. pp. 2479-2501.
  4. Щербаков А. Ю. Современная компьютерная безопасность. Теоретические основы. Практические аспекты. – М.: Книжный мир, 2009. 352 с.
  5. Щербаков А. Ю. Хрестоматия специалиста по современной информационной безопасности. Том 1. Saarbrucken : PalmariumAcademicPublishing, 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. 2020.
  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 (статья принята к публикации).

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

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

Библиографическая ссылка: Каннер А. М. Применение TLA+нотации для описания модели изолированной программной среды субъектов доступа и ее дальнейшей верификации // Вопросы защиты информации. М., 2021. № 3(134). С. 8–11.


Scientia potestas est
Кнопка связи