Метод контроля выполнения политики безопасности в операционных системах семейства Windows тема диссертации и автореферата по ВАК РФ 05.13.19, кандидат наук Кочетков Евгений Викторович

• Кочетков Евгений Викторович
• кандидат наук
• 2021

Оглавление диссертации кандидат наук Кочетков Евгений Викторович

Введение

Глава 1. Многоуровневая модель политики безопасности

управления доступом операционных систем семейства Windows

1.1 Существующий мандатный контроль целостности в операционных системах семейства Windows

1.2 Подход к верификации моделей методом Model checking с использованием языка темпоральной логики действий Лэмпорта (TLA+)

1.3 Описание формальной модели многоуровневой политики безопасности управления доступом операционных систем семейства Windows

1.4 Предикаты действий и инварианты многоуровневой модели политики безопасности управления операционных систем семейства Windows

1.5 Вывод по главе

Глава 2. Метод контроля выполнения политики безопасности

операционных систем семейства Windows

2.1 Применение метода формальной верификации «Model cheсking» для решения задачи контроля выполнения политики безопасности операционной системы

2.2 Формальная модель выполнения процесса в операционной системе

2.3 Формальный логический язык задания функциональных ограничений

2.4 Выводы по главе

Глава

3. Научно-технические предложения по практической реализации метода контроля выполнения политики безопасности операционных систем семейства Windows

Стр.

3.1 Комплекс алгоритмов

3.2 Оценка эффективности метода контроля политики безопасности операционных систем семейства Windows (сравнение с аналогами)

3.3 Вывод по главе

Заключение

Список сокращений и условных обозначений

Словарь терминов

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

Список рисунков

Список таблиц

Приложение А. Базис аксиом безопасного выполнения

программного обеспечения

Приложение Б. Листинг многоуровневой модели политики

безопасности управления доступом

операционных систем семейства Windows

Б.1 Модуль многоуровневого разграничения доступа

Б.2 Модуль дискреционного разграничения доступа

Б.3 Модуль инициализации начальных значений

Б.4 Модуль вспомогательных операторов

Б.5 Модуль вспомогательных операторов выбора элементов из

множеств

Б.6 Модуль определения типов

Б.7 Основной модуль многоуровневой модели политики

безопасности управления доступом

Приложение В. Таблицы преобразования системных и

API-вызовов в действия процесса

Стр.

В.1 Таблица преобразования системных вызовов операционной

системы в действия процесса

В.2 Таблица преобразования системных ЛР1-вызовов операционной

системы в действия процесса

Приложение Г. Акт внедрения результатов

ООО «Киберполигон»

Приложение Д. Акт внедрения результатов АО «Аладдин Р.Д.»

Введение диссертации (часть автореферата) на тему «Метод контроля выполнения политики безопасности в операционных системах семейства Windows»

Введение

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

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

Степень разработанности темы исследования

Результаты исследований таких ученых, как П.Д. Зегжда, Д.П. Зегжда, А.В. Хорошилов, H.A. Гайдамакин, Дж. Кэрри, Р. Рид и др. в разработке формальных моделей обеспечения информационной безопасности и П.Н. Девяни-на — в области формализации и верификации политик безопасности управления доступом, доказывают принципиальную возможность достижения гарантированного уровня обеспечения целостности на основе применения формальных методов.

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

Объектом исследования является подсистема разграничения доступа и обеспечения целостности операционных систем семейства Windows.

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

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

Для достижения поставленной цели в работе решаются следующие задачи:

1. Анализ эффективности существующих средств антивирусной защиты от ВПО и технологий защиты от реализации уязвимостей программного обеспечения на уровне ядра в целях обеспечения целостности исполняемых и конфигурационных файлов операционной системы.

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

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

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

5. Разработка метода контролируемого выполнения политики безопасности операционной системы семейства Windows.

6. Разработка научно-технического предложения по практической реализации предложенного метода контроля выполнения политики безопасности операционных систем семейства Windows.

Научная новизна исследования состоит в следующем:

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

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

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

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

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

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

Положения, выносимые на защиту:

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

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

3. Научно-технические предложения по практической реализации метода контроля выполнения политики безопасности в операционных системах семейства Windows, отличающиеся применением полносистемной эмуляции для контроля системных вызовов.

Соответствие специальности научных работников

Полученные научные результаты соответствуют следующим пунктам раздела 2 «Области исследования» паспорта специальности научных работников 05.13.19 «Методы и системы защиты информации, информационная безопасность»: технологии идентификации и аутентификации пользователей и субъектов информационных процессов. Системы разграничения доступа. (п. 11); принципы и решения (технические, математические, организационные и др.) по созданию новых и совершенствованию существующих средств защиты информации и обеспечения информационной безопасности (п. 13).

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

Формальная постановка задачи

Разработать метод контроля выполнения политики безопасности M в операционных системах семейства Windows, обеспечивающий доказательство следующей теоремы:

Теорема 1. —M(a,A,SecPolicy) ^ —da € A, где:

a € {S x O x actions};

SecPolicy = DAC Л MAC Л FuncSpec;

a - доступ субъекта к объекту;

S - множество субъектов доступа;

O - множество объектов доступа;

actions - множество возможных действий субъекта по отношению к объекту;

SecPolicy - спецификация политики безопасности;

A - множество совершенных доступов субъекта к объекту;

M - предикат проверки относительно заданной модели политики безопасности SecPolicyc;

□ - темпоральный оператор «всегда в будущем»;

DAC - дискреционное разграничение доступа;

MAC - мандатное разграничение доступа;

FuncSpec - функциональное ограничения на работу прикладного программного обеспечения.

Апробация работы. Основные результаты работы опубликованы в статьях [1; 3—10] в рецензируемых изданиях, входящих в перечень рекомендованных ВАК при Минобрнауки РФ. Публикации [1; 3; 11] проиндексированы в Scopus и WoS. В статье [4] осуществляется обоснование возможности применения верификации программ для обнаружения в них вредоносного кода. Разработка формальной модели выполнения процесса в операционной системы рассмотрена в [1]. Формальный логический язык задания функциональных требований к выполнению процессов рассмотрен в [7]. Комплекс алгоритмов, лежащий в основе метода контроля выполнения политики безопасности операционных систем семейства Windows, и подход к практической реализации разработанного решения представлены в статьях [8; 10; 2]. Работы [5; 6; 9] посвящены исследованию особенностей функционирования ВПО и методам их обнаружения, вопросам применения и эффективности современных средств антивирусной защиты. В работе [3] разработана формальная многоуровневая модель политики безопасности управления доступом операционных систем семейства Windows.

По теме диссертации опубликовано 10 научных работ, в том числе 8 в изданиях из перечня ВАК при Минобрнауки РФ, 2 — в изданиях, индексируемых в базах Scopus и WoS. Получено 5 свидетельств ФИПС о регистрации программ для ЭВМ.

Результаты работы обсуждались на следующих конференциях:

1. Межрегиональная научно-практическая конференция «Информационная безопасность и защита персональных данных. Проблемы и пути их решения», БГТУ, Брянск, Россия, 2014 [12].

2. Всероссийская научно-техническая конференция «Безопасные информационные технологии», МГТУ им. Н.Э. Баумана, Москва, 16 ноября, 2016 [13].

3. Международная конференция «Новые горизонты», БГТУ, Брянск, Россия, 2016, [14].

4. International conference on information technology and nanotechnology — 2017 : ITNT 2017, Самара, Россия, 2017, [15].

5. 26-я научно-техническая конференция методы и технические средства обеспечения безопасности информации, Санкт-Петербургский политехнический университет Петра Великого, 2017 [16].

6. Открытая конференция ИСП РАН им. В.П. Иванникова, 2017.

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

8. Международная научно-техническая конференция «Безопасные информационные технологии», МГТУ имени Н.Э. Баумана, 2021.

Личный вклад. Все представленные в диссертации результаты получены лично автором.

Объем и структура работы. Диссертация состоит из введения, трех глав, заключения и пяти приложений. Полный объем диссертации составляет 156 страниц, включая 14 рисунков и 14 таблиц. Список литературы содержит 42 наименования.

Глава 1. Многоуровневая модель политики безопасности управления доступом операционных систем семейства Windows

1.1 Существующий мандатный контроль целостности в операционных системах семейства Windows

Работа механизма обязательного контроля доступа Mandatory Access Control (MIC) заключается в том, что всем процессам, файлам, каталогам, а также другим именованным сущностям назначается определенный уровень целостности. При этом доступ субъектов к объектам осуществляется на основе модели безопасности Биба [1]. Целью данного механизма является использование политик управления целостностью и уровней целостности задействованных субъектов и объектов для ограничения доступа процессам, которые считаются потенциально менее надежными, по сравнению с доверенными процессами, работающими под той же учетной записью пользователя. С помощью задания различных уровней целостности MIC позволяет изолировать потенциально уязвимые приложения (например, приложения, ориентированные на работу в сети Интернет, офисные приложения), которые используются для открытия документов, полученных из недоверенных источников. Процессы с низким уровнем целостности имеют меньший доступ (ограничены права на запись в системные области, чем процессы с более высокими уровнями целостности) [2].

При этом можно выделить следующие основные ограничения MIC [3—5]:

— по умолчанию большинство файлов и каталогов имеют средний уровень целостности (Middle integrity), таким образом граница доверия между объектами становится размытой;

— процессу назначается низкий уровень целостности (Low integrity) только по инициативе самого процесса, чаще всего при работе в сети Интернет, однако большинство браузеров и других приложений этого не делает;

— при задании уровня целостности файлов не учитывается источник их получения, например, съемные носители, сетевые диски, а также файлы, полученные из сети, обладают явно более низким уровнем целостности, чем файлы, созданные самой ОС.

■ System

■ High Medium

■ Low U n trusted

Рисунок 1.1 — Распределение вредоносных программ по уровням обеспечения целостности Windows в момент их обнаружения

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

При этом результаты анализа уровней целостности, с которыми выполняются вредоносные программы в момент их детектирования поведенческими сиг-натурами4, показали, что большая часть вредоносных программ выполняются с высоким уровнем целостности. Распределение вредоносных программ, обнаруженных средствами антивирусной защиты, по уровням целостности Windows представлено на рисунке 1.1 [rusakov].

На основе представленных на рисунке 1.1 сведений можно сделать вывод, что при использовании штатного набора средств защиты ОС семейства Windows большинство вредоносных про-грамм выполняется с высоким уровнем целостности.

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

решений является автоматическая формальная верификация модели политики безопасности управления доступом с использованием метода Model checking, который является математически обоснованным способом доказательства того, что модель соответствует заданной для нее спецификации [6; 7] c использованием инструментальных средств [8; 9].

Актуальность проблемы разработки формальной модели политики безопасности управления доступом также связана с процессом внедрения ФСТЭК России «Требований безопасности информации к операционным системам», в частности выполнение требований функциональной компоненты ADV-SPM.1 «Формальная модель политики безопасности» [10].

Для семейства операционных систем Linux решение подобной задачи рассмотрено в работах [11—13].

1.2 Подход к верификации моделей методом Model checking с использованием языка темпоральной логики действий

Лэмпорта (TLA+)

Под верификацией модели методом Model checking понимается автоматическое доказательство соответствия поведения системы заданной для нее спецификации. Спецификация отражает условия, при выполнении которых для каждого состояния системы доказано наличие у модели требуемых свойств жизнеспособности (liveness) и безопасности (safety) [14, с. 120].

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

Свойство безопасности модели отражает невозможность перехода системы во множество запрещенных состояний. При моделировании работы лифта одним из запрещенных состояний является перемещение между этажами с открытыми дверями. Примером запрещенного состояния при моделировании раз-

граничения доступа к информации является факт несанкционированного доступа к ней [15—19]. В общем виде организация процесса верификации методом Model checking представляет собой последовательное выполнение следующих этапов [14, с. 13]:

1. Этап моделирования.

2. Этап автоматизированной верификации.

3. Этап анализа результатов.

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

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

Существуют различные способы задания модели. В рамках настоящего исследования для определения модели применяется нотация языка TLA+ [20; 21], близкая к математической, она обладает достаточной гибкостью и выразительными возможностями описания, а наличие верификатора TLC позволяет произвести ее автоматизированную верификацию.

Определение переменных системы производится с использованием выражения:

VARIABLESA, B,

где A, B - переменные, значение которых определяют состояние модели. Переход системы в следующее состояние происходит в результате изменения значе-

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

SwapA(a ,b) = АЛ' = (A \ a) U b , AUNCHENGEDB

где UNCHENGED - ключевой оператор языка TLA+, означающий, что переменные, перечисленные в кортеже, не изменились.

Результатом выполнения оператора SwapA является переход в новое состояние системы, при котором элемент a исключается из множества A, а элемент b включается. При этом значение переменной B не изменяется.

Задание начального состояния системы производится c использованием специального оператора Init. Пример определения начального состояния системы представлен следующим выражением:

Init = Л = {} A B = {}

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

— □ - оператор «всегда в будущем»;

— ♦ - оператор «однажды в будущем»;

— U - бинарный оператор «до тех пор пока»;

— S - бинарный оператор «с тех пор как».

В общем виде спецификация модели языке TLA+ имеет следующий вид:

Spec = Init A □[Next}vars

где Next - предикаты действий, изменяющие значения переменных модели, vars - картеж переменных модели. При моделировании объектов реального мира использование переменных, хранящих единственное значение из заданного домена значений недостаточно, ввиду того такие объекты характеризуются

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

Structure = [

id : {1,2} is-main : BOOLEAN ,

]

где BOOLEAN - встроенный тип данных, принимающий значения из множества {TRUE, FALSE}. Определение структуры эквивалентно определению следующего множества элементов:

Structure = {

[id : 1, is-main : TRUE ], [id : 1, is-main : FALSE ], [id : 2, is-main : TRUE ], [id : 2, is-main : FALSE ]

}

Преобразование определения структуры во множество элементов дает возможность проверить является ли некоторое множество A подмножеством Structure:

A С Structure

Обращение к элементам структуры производится с использованием разделителя «точка». При определении операторов модели могут быть использованы следующие функции TLA+:

— Len (x) возвращает длину картежа x;

— Cardinality(m) возвращает мощность множества m;

— Range(y) возвращает множество элементов, полученное из картежа y.

1.3 Описание формальной модели многоуровневой политики безопасности управления доступом операционных систем семейства

Windows

При определении структур субъектов и объектов с использованием TLA+ отсутствует строгая типизация (по умолчанию производится проверка только встроенных типов), однако проверка инвариантов типов является неотъемлемой частью спецификации, поскольку верификация производится методом «Model Checking».

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

Множества идентификаторов процессов, контейнеров, файлов и пользователей (значения модельные):

UserlDs = 0..2, GroupIDs = 0..2, SubjectlDs = 0..1, ObjectlDs = 0..6,

где UserlDs - множество идентификаторов пользователей; GroupIDs - множество идентификаторов групп; SubjectIDs - множество идентификаторов субъектов; ObjectIDs - множество идентификаторов объектов. Для разграничения доступа с учетом многоуровневой модели доступа были определены следующие множества уровней и категорий конфиденциальности и целостности:

ConfLevs = 0..2, IntLevs = 0..2,

ConfCats = {«C1», «C2»}, IntCats = {«II», «12»}, где ConfLevs - множество уровней конфиденциальности; IntLevs - множество уровней целостности; ConfCats - множество категорий конфиденциальности; IntCats - множество категорий целостности.

Множество разрешений на доступ к объекту заданы следующим выражением:

Permissions = {

«read», «write», «append»,

«create», «delete», «delete_subfolder»,

«change_perm», «change_owner», «execute», '

«read_attr», «write_attr»

}

где «read» - чтение содержимого объекта; «write» - изменение содержимого объекта; «append» - запись в конец содержимого объекта без его чтения; «create» -создание объекта; «delete» - удаление объекта; «delete_subfolder» - удаление дочерних каталогов; «change_perm» - изменение разрешений на доступ к объекту; «change_owner» - изменение владельца объекта; «execute» - исполнение объекта; «read_attr» - чтение атрибутов объекта; «write_attr» - изменение атрибутов объекта. Для сравнения уровней конфиденциальности и целостности в модели приняты следующие соответствия уровней абсолютным значениям (таблица 1).

Таблица 1 — Соответствие уровней конфиденциальности и целостности абсолютным значениям

Абсолютное значение Уровень конфиденциальности Уровень целостности

2 Высокий Низкий

1 Средний Средний

0 Низкий Высокий

Состояние многоуровневой модели политики безопасности управления доступом определяется набором значений каждого элемента из следующих переменных:

— множество доступов Л;

— множество объектов доступа О;

— множество субъектов доступа 5;

— множество пользователей и;

— множество групп пользователей С.

Список литературы диссертационного исследования кандидат наук Кочетков Евгений Викторович, 2021 год

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

1. Zune S. Mandatory access control by Biba model: M.C.Sc Dissertation / Zune S. — University of Computer Studies, 2018.

2. Gartaganis C. Comparative analysis of the Windows security XP, Vista, 7, 8 and 10 : Master's thesis / Gartaganis Charalampos. — Kiprus University, 2017.

3. Yile F. Research on the Security Problem in Windows 7 Operating System. // Eighth International Conference on Measuring Technology and Mechatronics Automation (ICMTMA) / под ред. editor. — 2016.

4. Zhu Z, Peng G. An analysis about the defects of Windows UAC mechanism // Chinese Conference on Trusted Computing and Information Security. — Springer. 2018. — С. 270—285.

5. Zhivov A., Lohse R. Windows // Deep Energy Retrofit. — Springer, 2020. — С. 39—62.

6. Havelund K., Peled D. Runtime Verification: From Propositional to FirstOrder Temporal Logic. — 2018.

7. First Order Logic For Program Code Functional Requirements Description / E. V. Kochetkov [и др.] // Вопросы кибербезопасности. — 2017. — Т. 21, № 3. — С. 2—7.

8. Kuppe M. A., Lamport L., Ricketts D. The TLA+ toolbox // F-IDE / под ред. editor. — 2019. — С. 50—62.

9. McMillan K. L. Eager abstraction for symbolic model checking // International Conference on Computer Aided Verification. — Springer. 2018. — С. 191—208.

10. Девянин П. О проблеме представления формальной модели политики безопасности операционных систем // Труды ИСП РАН. — 2017. — Т. 29, № 3. — С. 7—16.

11. Integrating RBAC, MIC, and MLS in verified hierarchical security model for operating system / P. N. Devyanin [и др.] // Programming and Computer Software. — 2020. — Т. 46, № 7. — С. 443—453.

12. Efremov D., Shchepetkov I. Runtime Verification of Linux Kernel Security Module // International Symposium on Formal Methods. — Springer. 2019. — С. 185—199.

13. Verifying the reliability of operating system-level information flow control systems in linux / L. Georget [и др.] // 2017 IEEE/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE). — IEEE. 2017. — С. 10—16.

14. Baier C. Katoen J. P. Principles of model checking. — MIT press, 2008.

15. Design and verification for transportation system security / B. Zheng [и др.] // Proceedings of the 52nd annual design automation conference. — 2015. — С. 1— 6.

16. Козачок А. В., Туан Л. Комплекс алгоритмов контролируемого разграничения доступа к данным, обеспечивающий защиту от несанкционированного доступа // Системы управления и информационные технологии. — 2015. — 3 (16). — С. 58—61.

17. Козачок А. В., Кочетков Е. В. Обоснование возможности применения верификации программ для обнаружения вредоносного кода // Вопросы кибербезопасности. — 2016. — 3 (16). — С. 25—32.

18. Стародубцев Ю. И., Бегаев А. Н., Козачок А. В. Способ управления доступом к информационным ресурсам мультисервисных сетей различных уровней конфиденциальности // Вопросы кибербезопасности. — 2016. — 3 (16). — С. 13—17.

19. Козачок А. В. Спецификация модели управления доступом к разнокатего-рийным ресурсам компьютерных систем // Вопросы кибербезопасности. — 2018. — 4 (28). — С. 2—8.

20. Kuppe M. A., Lamport L., Ricketts D. The TLA+ toolbox // arXiv preprint arXiv:1912.10633. — 2019.

21. Oliveira D. B. de, Cucinotta T, Oliveira R. S. de. Efficient formal verification for the Linux kernel // International Conference on Software Engineering and Formal Methods. — Springer. 2019. — С. 315—332.

22. Гайдамакин Н. ТЕМАТИКО-АТРИБУТИВНЫЙ СПОСОБ УПРАВЛЕНИЯ ДОСТУПОМ К ДОКУМЕНТАМ, СОДЕРЖАЩИМ СВЕДЕНИЯ, СОСТАВЛЯЮЩИЕ КОММЕРЧЕСКУЮ ТАЙНУ // Защита информации. Инсайд. — 2020. — Т. 96, № 1. — С. 38—50.

23. Bell D. E., LaPadula L. J. Secure Computer Systems: A Mathematical Model:[ESD-TR-73-278] //AD 771 543, Electronic Systems Division, Air Force Systems Command, Hanscom AFB. Т. 11. — 1973.

24. Zune S. Mandatory access control by Biba model // MC Sc Dissertation. University of Computer Studies, Yangon. — 2018.

25. Верификация автоматных программ / С. Вельдер [и др.]. — СПб : Наука, 2011. — С. 244.

26. Emerson E. A. The beginning of model checking: A personal perspective // 25 Years of Model Checking. — Springer, 2008. — С. 27—45.

27. Model checking / E. M. Clarke Jr [и др.]. — MIT press, 2018.

28. Yosifovich P., Solomon D. A., Ionescu A. Windows Internals, Part 1: System architecture, processes, threads, memory management, and more. — Microsoft Press, 2017.

29. Гордеев А. В. Операционные системы:[по направлению подгот."Информатика и вычисл. техника"]. — Издательский дом"Питер", 2009.

30. Короткое М., Степанов Е. Основы формальных логических языков. — СПб ГИТМО (ТУ), 2003.

31. Hafer T., Thomas W. Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree // Automata, Languages and Programming. — 1987. — С. 269—279.

32. ФСТЭК 1. Банк данных угроз безопасности информации [Электронный ресурс]. — URL: http://bdu.fstec.ru/.

33. Кочетков Е. В., Козачок А. В. Формальная модель функционирования процесса в операционной системе // Труды СПИИРАН. — 2017. — Т. 51, № 2. — С. 78—96.

34. Hertz J., Newsham T. Project triforce: Run afl on everything // NCC Group, Tech. Rep. — 2016.

35. Карпов Ю. Model Checking. Верификация параллельных и распределенных программных систем. — БХВ-Петербург, 2010. — С. 560.

36. Программное средство задания спецификаций программ на основе функциональных требований к ним : Свидетельство о государственной регистрации программы для ЭВМ № 2017611368 / Е. В. Кочетков, А. В. Козачок. — Заявл. 06.2016.

37. Программное средство построения модели исполняемого файла на языке Promela : Свидетельство о государственной регистрации программы для ЭВМ № 2016616577 / Е. В. Кочетков, А. В. Козачок. — Заявл. 06.2016.

38. Репозиторий исходного кода эмулятора «Qemu» // «Институт системного программирования им. В.П. Иванникова» [Электронный ресурс]. — URL: https://github.com/ispras/qemu/tree/plugins (дата обр. 09.10.2017).

39. Программное средство верификации моделей программ на языке Promela : Свидетельство о государственной регистрации программы для ЭВМ № 2016616578 / Е. В. Кочетков, А. В. Козачок. — Заявл. 06.2016.

40. GitHub - albertocasagrande/pyModelChecking: A Python model checking package [Электронный ресурс]. — URL: https : / / github . com / albertocasagrande/pyModelChecking (visited on 10/03/2017).

41. Программное средство генерации автомата безопасности для программы на основе спецификации функциональных требований : Свидетельство о государственной регистрации программы для ЭВМ № 2017611274 / Е. В. Кочетков, А. В. Козачок. — Заявл. 06.2016.

42. Documentation/QMP - QEMU [Электронный ресурс]. — URL: https://wiki. qemu.org/Documentation/QMP (дата обр. 09.10.2017).

Список рисунков

1.1 Распределение вредоносных программ по уровням обеспечения

целостности Windows в момент их обнаружения ............ 12

2.1 Схема процесса формальной верификации

методом «Model checking»......................... 42

2.2 Функциональная схема мониторинга исполнения программы..... 56

2.3 Функциональная схема безопасного исполнения программного кода . 57

3.1 Функция преобразования системного вызова в действие в ОС..... 61

3.2 Алгоритм контроля выполнения политики безопасности операционных систем семейства Windows................ 62

3.3 Преобразование множества трасс исполнения

программы в модель.............................. 66

3.4 Алгоритм формальной верификации «Model checking»........ 68

3.5 Пример разбора исходного выражения с использованием

операторов темпоральной логики на подвыражения ....................70

3.6 Алгоритм построение автомата безопасности............................73

3.7 Алгоритм мониторинга исполнения......................................74

3.8 Архитектура системы контролируемого

выполнения программного кода ..................... 76

3.9 Обобщенная архитектура системы

контролируемого выполнения программного кода ........... 78

3.10 Реализация метода контроля выполнения политики безопасности с использованием полносистемного эмулятора «QEMU» ........ 81

Список таблиц

1 Соответствие уровней конфиденциальности и целостности абсолютным значениям ....................................................18

2 Атрибуты элементов множества пользователей при инициализации . 28

3 Атрибуты элементов множества субъектов при инициализации ... 28

4 Атрибуты элементов множества объектов при инициализации .... 29

5 Действия многоуровневой модели политики безопасности операционных систем семейства Windows ................................32

6 Возможные операции в рамках модели..................................46

7 Категории субъекта и объектов в рамках модели ......................47

8 Обобщенное представление набора атомарных правил безопасного исполнения ..................................................................52

9 Соответствие класса ПО и класса безопасности ........................54

10 Программные средства реализации СКВПБ ............................80

11 Программные средства для создания изолированной программной среды Windows ..............................................................82

12 Снижение производительности при использовании СКВПБ............83

Приложение А

Базис аксиом безопасного выполнения программного обеспечения

p1 * p*

p1 * m*

p1 * e*

p1 n *

p1 d*

Процесс 1 категории Действие «Create»

- системный процесс может создать любой процесс

- выделение памяти в любом месте

- создание любого файла/каталога

- создание любого соединения

- создание любого устройства Действие «Open»

p1 A p* - системный процесс может открыть любой процесс p1 A e* - открытие любого файла/каталога p1 A d* - открытие любого устройства Действие «Delete»

p1 A p2'3 - системный процесс может завершить любой процесс

p1 A p1 - системный процесс может завершить свою работу

p1 A oj Л p1 A ok - системный процесс может закрывать объекты, им

порожденные (Vo Е O' = {O\M})

Действие «Read»

- системный процесс может читать любой процесс

- чтение памяти в любом месте

- чтение любого файла/каталога

- чтение данных любого соединения

- чтение данных из любого устройства Действие «Write»

1 w *

p1 A m* - запись в память в рамках своего адресного простран-

ства

- запись в файл

- запись данных любого соединения

- запись данных из любого устройства Процесс 2 категории

Действие «Create»

p1 A- p*

p1 r * m*

p1 A- * e*

p1 A- * n*

p1 A- d*

p1 w > e

p1 w n

p1 w d

2 С 2 3

p2 - p2'3 - привилегированный процесс может создать процессы

2 С 2 3

p2 — m2 ' 3 - выделение памяти

p2 -- e*\{2 '4} - создание файла/каталога, кроме системной области p2 - n* - создание любого соединения —(p2 -- d*) - запрет на создание устройств Действие «Open»

2 o 2 3

p2 — p2 ' 3 - привилегированный процесс может открыть процесс p2 -— e*\{2} - открытие файла/каталога, кроме системной области p2 - d1 ' 2 - открытие устройства ввода/вывода Действие «Delete»

p2 - p2 - процесс может завершить свою работу

2 к» 2 d k „ p2 - oj Л p2 - oj - привилегированный процесс может закрывать объекты, им порожденные (Vo G O' = {O\M})

Действие «Read»

pf - pf - процесс может читать информацию о себе

2 г 3

p2 - m3 - чтение памяти в рамках своего адресного простран-

ства

p2 - e3 '4 '5 - чтение файла/каталога

p2 ej Л p2 - ej - чтение файла/каталога, созданного субъектом p2 - nj Л p2 - nj - чтение данных соединения, созданного субъектом p2 - dj' 2 Л p2 - d1 2 - работа с устройствами Действие «Write»

2 w 3

p2 - m3 - запись в память в рамках своего адресного простран-

ства

2 w 5

p2 - e5 - запись в файл

p2 ej Л p2 - ej - чтение файла/каталога, созданного субъектом p2 - nj Л p2 - nj - запись данных соединения, созданного субъектом p2 - dj ' 2 Л p2 - d1' 2 - работа с устройствами Процесс 3 категории Действие «Create»

3 С 3

p3 - p3 - процесс может создать пользовательский процесс

3 С 3

p3 - m3 - выделение памяти в своем адресном пространстве

р3 __ е3 , 5 - создание файла/каталога

3 с 2 3

р3 _ п2, 3 - создание локальных соединен]

—(р3 __ й*) - запрет на создание устройств

Действие «Open»

—(p3 A p*) - пользовательский процесс не может открыть процесс p3 A e3'4'5 - открытие файла/каталога, системных библиотек —(p3 A d*) - запрет на работу устройствами Действие «Delete»

p3 A p3 - процесс может завершить свою работу

p3 A ok Л p3 A ok - процесс может закрывать (завершать) объекты, им

порожденные (Vo Е O' = {O\M})

Действие «Read»

p3 A p3 - процесс может читать информацию о себе

3 r 3

p3 A m3 - чтение памяти в рамках своего адресного простран-

ства

p3 A e3'4'5 - чтение файла/каталога

p3 --A ej Л p3 A ej - чтение файла/каталога, созданного субъектом p3 A njk Л p3 -A njk - чтение данных соединения, созданного субъектом —(p3 -A d*) - запрет на работу устройствами

Действие «Write»

3 w 3

p3 A m3 - запись в память в рамках своего адресного простран-

ства

p3 -Aw e5 - запись в файл

p3 -A ej Л p3 A ej - чтение файла/каталога, созданного субъектом p3 A njk Л p3 A njk - запись данных соединения, созданного субъектом —(p3 A d*) - запрет на работу устройствами

Безопасно Действие «Create»

—(p* -A p*) - процесс не создает процессы

c3

p* A m3 - выделение памяти только в своем адресном пространстве p* -Ac e5 - только свои файлы и каталоги

—(p* -A n*) - запрет на создание любого соединения —(p* -A d*) - запрет на создание устройств Действие «Open»

—(p* -A p*) - процесс не может открыть процесс p* -A e4'5 - открытие системных библиотек и файла/каталога —(p* -A d*) - запрет на открытие устройства Действие «Delete»

j, d .л,

pi* - p* - процесс может завершить свою работу

p* - ej Л pi* - ej - процесс может закрывать (завершать) объекты, им

порожденные (Vo G O' = {O\M})

Действие «Read»

—(p* - p*) - процесс не может читать информацию о процессах

* r 3

p* - m3 - чтение памяти в рамках своего адресного простран-

ства

p* - e4'5 - чтение файла/каталога

—(p* - n*) - запрет на работу c сетью

—(p* - d*) - запрет на работу устройствами

Действие «Write»

w3

p* - m3 - запись в память в рамках своего адресного простран-

ства

p* - e5 - запись в файл

—(p* - n*) - запрет на работу c сетью

—(p* - d*) - запрет на работу устройствами

Приложение Б

Листинг многоуровневой модели политики безопасности управления доступом операционных систем семейства Windows

Б.1 Модуль многоуровневого разграничения доступа

10

15

20

25

MODULE MAC

EXTENDS Integers , TLC , FiniteSets , Sequences , Opers , Types , Inits, Select

\* Прeдикаты провёрки мандатного управлёния доступом

MAC_may_access_conf(s,o) ==

\/ "ccnr" \in o.ext_attr \/ /\ o.cl <= s.cl

/\ o.conf_cats \subseteq s.conf_cats

MAC_may_access_intg(s,o) == \/ "icnr" \in o.ext_attr \/ /\ o.il >= s.il

/\ o.int_cats \subseteq s.int_cats

MAC_may_read(s,o) ==

MAC_may_access_conf(s , o)

MAC_may_write(s,o) ==

/\ MAC_may_access_conf(s,o) /\ MAC_may_access_intg(s,o)

MAC_may_append(s,o) ==

/\ MAC_may_access_conf(s,o) /\ MAC_may_access_intg(s,o)

MAC_may_become_child(op,ch_cl,ch_conf_cats,ch_il,ch_int_cats) ==

/\ \/ /\ ch_cl <= op.cl

/\ \/ op.conf_cats = {}

5

40

45

50

55

60

65

X/ ch_conf_cats Xsubseteq op.conf_cats X/ "ccnr" Xin op.ext_attr

/X X/ /X c h _ il <= op.il

/X X/ op.int_cats = {}

X/ ch_int_cats Xsubseteq op.int_cats X/ "icnr" Xin op.ext_attr

MAC_may_become_child_subj (s , cl,conf_cats ,il,int_cats) =: /X cl <= s. cl

/X conf_cats Xsubseteq s.conf_cats /X il >= s.il

/X int_cats Xsubseteq s.int_cats

MAC_may_remove_ccnr (o) ==

X/ /X o.type Xin Containers

/X XA ch Xin SelectAllChilds (o) : /X ch . cl <= o . cl

/X ch.conf_cats Xsubseteq o.conf_cats X/ Xneg o.type Xin Containers

MAC_may_remove_icnr(o) ==

X/ /X o.type Xin Containers

/X XA ch Xin SelectAllChilds(o) : /X ch.il >= o.il

/X ch.int_cats Xsubseteq o.int_cats X/ Xneg o.type Xin Containers

MAC_may_change_cl(o,cl) ==

/X X/ cl <= ParentCont(o).cl

X/ "ccnr" Xin ParentCont(o).ext_attr /X X/ /X o. type Xin Containers

/X X/ /X XA ch Xin SelectAllChilds(o): /X ch. cl <= cl X/ "ccnr" Xin o.ext_attr X/ Xneg o.type Xin Containers

MAC_may_change_il(o,il) ==

/X X/ il <= ParentCont(o).il

X/ "icnr" Xin ParentCont(o).ext_attr /X X/ /X o. type Xin Containers

/X X/ /X XA ch Xin SelectAllChilds (o) : /X ch.il >= il

80

85

\/ "icnr" \in o.ext_attr \/ \neg o . type \in Containers

MAC_may_change_conf_cats(o,conf_cats) ==

/\ \/ "ccnr" \in ParentCont(o).ext_attr /\ \/ /\ o . type \in Containers

/\ \/ /\ \A ch \in SelectAllChilds(o) /\ ch . cl <= o . cl \/ "ccnr" \in o.ext_attr \/ \neg o.type \in Containers

Б.2 Модуль дискреционного разграничения доступа

MODULE DAC

EXTENDS Integers , TLC , FiniteSets , Sequences , Opers , Types , Inits, Select

5 \* Прёдикаты провeрки дискрёционного управлeния доступом

IsUserAdmin(s) ==

/\ SelectUser(s.uid).is_admin = TRUE

10 \* a \in {"read", "write","execute","append","create", \* "delete","read_attr","write_attr",

\* "change_perm","change_owner"}

DAC_may_do(s,o,a) ==

\/ o.owner = s.uid

15

\/ \E r \in o.aclus: /\ r [1] = s.uid /\ a \in r [2]

20 \/ \E g \in SelectUserGroups(s.uid):

/\ \E r \in o.aclgs:

/\ r [1] = SelectGroup(g) .gid /\ a \in r [2]

25 \* "execute

35

40

45

50

55

60

DAC_may_execute(s,o) ==

/\ o . type = "executable" /\ o.exec_attr # "deny"

/\ \/ IsUserAdmin(s)

\/ o.owner = s.uid

\/ \E r \in o.aclus: /\ r [1] = s.uid /\ "execute" \in r[2]

\/ \E g \in SelectUserGroups(s.uid): /\ \E r \in o.aclgs:

/\ r [1] = SelectGroup(g) .gid /\ "execute" \in r [2]

\* "change_perm" DAC_may_change_perm(s,o) == \/ o. owner = s. uid

\/ \E r \in o.aclus: /\ r [1] = s.uid /\ "change_perm" \in r[2]

\/ \E g \in SelectUserGroups(s.uid): /\ \E r \in o.aclgs:

/\ r [1] = SelectGroup(g) .gid /\ "change_perm" \in r[2]

\* "change_owner" DAC_may_change_owner(s,o) == \/ o. owner = s. uid

\/ \E r \in o.aclus: /\ r [1] = s.uid /\ "change_owner" \in r[2]

\/ \E g \in SelectUserGroups(s.uid): /\ \E r \in o.aclgs:

/\ r [1] = SelectGroup(g) .gid /\ "change_owner" \in r[2]

\* "check_child_perm"

75

80

85

DAC_may_access_cont_hierachy(s,op,a) == \/ \A oi \in Range(op):

\/ SelectObject(oi).owner = s.uid

\/ \E r \in SelectObject(oi).aclus: /\ r [1] = s.uid /\ a \in r [2]

\/ \E g \in SelectUserGroups(s.uid): /\ \E r \in SelectObject(oi).aclgs /\ r [1] = SelectGroup(g) .gid /\ a \in r [2]

DAC_may_access_cont_hierachy2(s,op,a) == \A oi \in Range(op):

DAC_may_do(s,SelectObject(oi), a)

Б.3 Модуль инициализации начальных значений

MODULE Inits

EXTENDS Integers , TLC , FiniteSets , Sequences , Types VARIABLES A, O, S, U, G 5 \* nepeMeHHtie Mo^e^u vars == <<A, O, S, U, G>>

\* model values \* root container 10 o0 == [oid |-> 1, owner |-> 0, poid |-> <<1>>, content |-> {}, cl |-> CONF_MIN_LEVEL, conf_cats |-> {}, il |-> INT_MIN_LEVEL , int_cats |-> {}, type |-> "root_container",

ext_attr |-> {"check_child_perm" , "ccnr"}, exec_attr |-> "deny",

30

35

40

45

50

55

aclgs |-> {<<0,FullRole>>,<<1,ReadRole>>} aclus|-> {}]

01 == [ oid |-> 2,

owner |-> 0,

poid |-> <<1>>,

content |-> {},

cl |-> CONF_MIN_LEVEL,

conf_cats |-> {},

il |-> INT_MIN_LEVEL ,

int_cats |-> {},

type |-> "container",

ext_attr |-> {"check_child_perm"},

exec_attr |-> "deny",

aclgs |-> {} ,

aclus|-> {}]

02 == [oid |-> 3,

owner | -> 0,

poid |-> <<1>> ,

content |-> {},

cl |-> CONF_MIN_LEVEL,

conf_cats |-> {},

il |-> INT_MIN_LEVEL ,

int_cats |-> {},

type |-> "executable",

ext_attr |-> {},

exec_attr |-> "app",

aclgs |-> {} ,

aclus|-> {<<0,ExecuteRole>>}]

03 == [oid | -> 4,

owner | -> 0, poid |-> <<1>>, content |-> { "C " } , cl |-> 2, conf_cats |-> {}, il |-> INT_MIN_LEVEL , int_cats |-> {}, type |-> "f ile " , ext_attr |-> {} , exec_attr |-> "deny", aclgs |-> {} ,

70

75

80

85

90

95

100

s0 == [sid |-> 0, uid |-> 0 ,

cl |-> CONF_MIN_LEVEL, conf _ cat s |-> {"C1" , "C2"} , il | -> 1 ,

int_cats |-> {" I1"} ,

content_readed |-> {} ]

s1 == [sid |-> 1, uid |-> 1, cl | -> 1 ,

conf_cats |-> {"C1 "} , il | -> 1 ,

int_cats |-> {"I1"} ,

content_readed |-> {} ]

u0 == [uid |-> 0 ,

groups |-> {0} , is_admin |-> TRUE, cl | -> 1 ,

conf _ cat s |-> {"C1" , "C2"} , il | -> 1 ,

int_cats |-> {" I1" ,"I2 "} ,

white_list_execute_objects |-> {} ]

u1 == [uid |-> 1,

groups | -> {1} , i s_admin |-> FALSE, cl | -> 1 ,

conf_cats |-> {"C1 "} , il | -> 1 ,

int_cats |-> {"I1"} ,

white_list_execute_objects |-> {} ]

\* Administrators g0 == [gid |-> 0,

role|-> FullRole]

\* Users gl == [gid |-> 1,

role|-> ReadRole]

Б.4 Модуль вспомогательных операторов

10

------------------------------- MODULE Opers

EXTENDS Integers , TLC , FiniteSets , Sequences

\* Select last element of tuple

Last(s) == s [Len(s)]

\* Set of all tuple elements

Range(s) == { s[x] : x \in DOMAIN s }

\* Tuple from all set elements

Tuples(s) == { <<x>> : x \in s}

5

Б.5 Модуль вспомогательных операторов выбора элементов из

множеств

MODULE Select

EXTENDS Integers , TLC , FiniteSets , Sequences , Randomization Opers, Types, Inits

\* Select only execute objects

SelectExecuteObjects == {o \in O: o.exec_attr = "app"} \* Select user by id

SelectUser(owner) == CHOOSE u \in U: u.uid = owner \* Select object by id

SelectObject(id) == CHOOSE o \in O: o.oid = id \* Select subject by id

5

20

25

30

35

40

45

50

SelectSubject(id) == CHOOSE s \in S: s.sid = id \* Select group by id

SelectGroup(id) == CHOOSE g \in G: g.gid = id \* Get Group Users

SelectGroupUsers(gid) == { u \in U: \E g \in u.groups: g = gid} \* Get User Subjects

SelectUserSubjects(uid) == { s \in S: s . sid = uid} \* Get User Groups

SelectUserGroups(uid) == SelectUser(uid).groups \* Select parent container

ParentCont(o) == SelectObject(Last(o.poid)) \* Select all Actions by oid

SelectOidActions(oid) == { a \in A: a[2] = oid} \* Select containers

SelectContainers == {o \in O: o.type \in Containers} \* Select Acl Users