Пример многоуровневой модели

Чтобы не ограничиваться общими декларациями, приведем пример многоуровневых спецификаций для одного из системных вызовов ОС Linux. Полностью статья с этим примером будет опубликована в первом номере журнала «Труды ИСП РАН» в 2020 году («П.Н. Девянин, В.В. Кулямин и др. Интеграция мандатного и ролевого управления доступом и мандатного контроля целостности в верифицированной иерархической модели безопасности операционной системы»). Здесь мы с небольшими корректировками приводим часть статьи, которая показывает, как выглядит исходная абстрактная модель, и как она потом уточняется. Для понимания терминологии и обозначений можно прочитать монографию «П.Н. Девянин, Д.В. Ефремов, В.В. Кулямин, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков. Моделирование и верификация политик безопасности управления доступом в операционных системах // Горячая линия-Телеком, 2018».

В моделях на языке Event-B статическая часть называется контекстом и содержит описание базовых типов (называемых множествами), констант и аксиом; аксиомы задают типы констант и другие ограничения. Динамическая часть модели, называемая машиной, содержит описание элементов автомата – переменных состояния, событий и инвариантов.

Контекст базового слоя нашей модели политики управления доступом содержит следующие множества.

Корневой контейнер в иерархии сущностей соответствует константе \(Root \in EntityType\). Множество специальных административных ролей \(SpecialAdmRoles\) тоже является константой, содержащей отдельные роли для администрирования сущностей, субъектов, пользователей, обычных ролей и административных ролей. Далее используется конструкция \(partition(U,A,B,C)\), в Event-B означающая \(U=A \cup B \cup C\) и \(A \cap B=A \cap C=B \cap C=\emptyset\), эта конструкция может иметь любое число аргументов, больше двух, с аналогичным смыслом. Выполнены свойства:

Базовый слой нашей модели имеет следующие переменные состояния (определения типов переменных мы указываем здесь же, а не в отдельных инвариантах, как положено в Event-B).

Инварианты, в дополнение к типовым ограничениям, содержат ограничения корректности значений переменных. Для отображений \(EntityNames\) и \(Parent\) должно быть выполнено следующее.

На иерархии субъектов и ролей наложены следующие ограничения.

У сущности или роли может быть не более одного владельца: \(\forall r1,r2,e \cdot r1 \in Roles \wedge r2 \in Roles \wedge (e \mapsto Own) \in RoleRigths(r1) \cap RoleRights(r2) \Rightarrow r1=r2\).

Административное право \(read\) распространяется от ролей-родителей к детям: \(\forall a,r,p \cdot a \in AdmRoles \wedge r \in Roles \wedge p \in RParents(r) \wedge (p \mapsto Read) \in RoleAdmRights(a) \Rightarrow (r \mapsto Read) \in RoleAdmRights(a)\).

Список операций модели (событий Event-B) на базовом уровне следующий.

Например, спецификация события \(access\_write\_entity\) на базовом уровне такова.

Здесь параметр \(subject\) – это субъект, пытающийся получить доступ, \(entity\) – сущность, доступ к которой запрошен. Два первых охранных условия задают типы параметров. Третье условие утверждает, что чтобы получить доступ на запись в сущность, субъект должен иметь связанную с ним роль \(r\), имеющую право на запись в эту сущность. Четвертое условие означает, что для получения доступа субъект должен иметь доступ \(Execute\) ко всем членам некоторой цепочки включающих друг друга контейнеров, начинающейся с \(Root\) и заканчивающейся контейнером, содержащим нужную сущность (эта цепочка без корня обозначена как \(E\)).

Теперь рассмотрим, как выглядят уточненные спецификации этого же события в уточненных слоях модели. На слое, описывающем механизм мандатного контроля целостности (mandatory integrity control – MIC), к типам добавлено множество уровней целостности \(Integrity\) и две константы \(LowI\) и \(HighI\), принадлежащие этому множеству. Добавленные в переменные отображения \(EntityInt: Entities \to Integrity\) и \(SubjectInt: Subjects \to Integrity\) задают уровни целостности сущностей и субъектов. Отображение \(CCRI: Containers \to BOOL\) задает CCRI-флаги контейнеров. Если такой флаг для контейнера выставлен в \(TRUE\), то для доступа к сущностям внутри контейнера субъекту необходимо выполнить условия доступа к самому контейнеру. На этом слое добавлены события \(set\_user\_labels\) и \(set\_role\_labels\), позволяющие менять уровни целостности пользователей и ролей. Большая часть событий первого слоя уточнены при помощи добавления охранных условий, проверяющих соотношения уровней целостности параметров.

Инвариант, представляющий основное свойство безопасности механизма MIC, выглядит так.

В спецификацию события \(access\_write\_entity\) во втором слое добавлены следующие два условия.

Пятое охранное условие требует существования цепочки включающих друг друга контейнеров, начинающейся с \(Root\) и заканчивающейся контейнером, содержащим нужную сущность, для каждого из которых данный субъект должен иметь роль с правом доступа на \(Execute\), кроме того, каждый из этих контейнеров должен либо иметь опущенный \(CCRI\)-флаг, либо уровень целостности меньше или равный уровня целостности субъекта, запрашивающего доступ. Шестое условие требует, чтобы субъект, запрашивающий доступ на запись к сущности, имел уровень целостности, больше или равный уровню целостности этой сущности.

Третий слой модели (в дополнение к предыдущим слоям) описывает механизм мандатного управления доступом (mandatory access control – MAC), добавляя в рассмотрение уровни конфиденциальности \(Cnf\), определяемые как множество всех подмножеств некоторого непустого конечного множества \(Confidentiality\). Поскольку каждое конечное частично упорядоченное множество может быть изоморфно вложено в решетку множества всех подмножеств некоторого конечного множества, такое описание не накладывает значимых ограничений на структуру возможных уровней конфиденциальности.

В качестве переменных добавлены отображения \(EntityCnf: Entities \to Cnf\) и \(SubjectCnf: Subjects \to Cnf\), задающие уровни конфиденциальности сущностей и субъектов. Также добавлено отображение \(CCR: Containers \to BOOL\), описывающее \(CCR\)-флаги контейнеров. Если такой флаг для контейнера выставлен в \(TRUE\), то для доступа к сущностям внутри контейнера субъекту необходимо выполнить условия доступа к самому контейнеру. Снова, большинство событий уточнены с помощью охранных условий, проверяющих соотношения между уровнями конфиденциальности их параметров.

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

Следующие условия добавлены в спецификацию \(access\_write\_entity) в третьем модуле.

Седьмое условие здесь снова требует существования цепочки включающих друг друга контейнеров, начинающейся с \(Root\) и заканчивающейся контейнером, содержащим нужную сущность, для каждого из которых данный субъект должен иметь роль с правом доступа на \(Execute\), кроме того, каждый из этих контейнеров должен либо иметь опущенный \(CCRI\)-флаг, либо уровень целостности меньше или равный уровню целостности субъекта, запрашивающего доступ, и должен либо иметь опущенный \(CCR\)-флаг, либо уровень конфиденциальности меньше или равный уровню конфиденциальности субъекта. Восьмое условие говорит, что для получения доступа \(Write\) к сущности субъект должен иметь равный уровень конфиденциальности. Условия 5 и 7 вынуждено повторяют ограничения из условия 4, поскольку все эти ограничения должны быть выполнены для одной и той же цепочки контейнеров.

Последний модуль специфицирует модель информационных потоков между сущностями и субъектами. Для этого добавляются четыре переменных \(EEMFlows: Entities \to \mathcal{P}(Entities)\), \(ESMFlows: Entities \to \mathcal{P}(Subjects)\), \(SEMFlows: Subjects \to \mathcal{P}(Entities)\) и \(SSMFlows: Subjects \to \mathcal{P}(Subjects)\). Они представляют потоки на запись от сущностей к сущностям, от сущностей к субъектам, от субъектов к сущностям и от субъектов к субъектам. Отношение контроля между субъектами представлено отображением \(DeFactoOwn: Subjects \to \mathcal{P}(Subjects)\). Правило \(find\) из \(TGM\) трансформируется в два события, \(find\_entity\) и \(find\_subject\). Спецификация первого из них выглядит следующим образом.