ГОСТ Р 59453.1-2021 Защита информации. Формальная модель управления доступом. Часть 1. Общие положения

     7 Доказательство выполнения условий безопасности

7.1 В рамках формальной модели управления доступом в соответствии с политиками управления доступом, заданными в соответствии с 4.2, формальное описание абстрактного автомата должно включать:

- условия безопасности состояний абстрактного автомата;

- условия безопасности переходов из состояний в состояния абстрактного автомата;

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

7.2 Если заданные в соответствии с 4.2 политики управления доступом включают политику дискреционного управления доступом, то описание абстрактного автомата в дополнение к 7.1 должно включать:

а) условия безопасности абстрактного автомата, реализующего дискреционное управление доступом, включающие как минимум ограничения:

1) на права доступа субъектов доступа (учетных записей пользователей) к объектам или субъектам доступа;

2) информационные потоки;

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

Пример - , где - множество реализуемых прав доступа субъектов доступа к субъектам или объектам доступа (сущностям) состоит из двух непересекающихся множеств, соответствующих (LP) и не соответствующих (NP) условиям безопасности;

, где - множество реализуемых доступов субъектов доступа к сущностям состоит из двух непересекающихся множеств, соответствующих (LA) и не соответствующих (NA) условиям безопасности;

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

7.3 Если заданные в соответствии с 4.2 политики управления доступом включают политику ролевого управления доступом, то описание абстрактного автомата в дополнение к 7.1 должно включать:

а) условия безопасности абстрактного автомата, реализующего ролевое управление доступом, включающие как минимум ограничения:

1) на роли, разрешенные для учетных записей пользователей;

2) текущие роли, которыми обладают субъекты доступа;

3) права доступа (привилегии) ролей;

4) отношения подчиненности в иерархии ролей;

5) права доступа субъектов доступа к объектам или субъектам доступа, которыми они могут обладать с использованием текущих ролей;

6) информационные потоки;

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

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

7.4 Если заданные в соответствии с 4.2 политики управления доступом включают политику мандатного контроля целостности, то описание абстрактного автомата в дополнение к 7.1 должно включать:

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

1) на уровни целостности субъектов доступа в зависимости от уровней целостности учетных записей пользователей, от имени которых они функционируют;

2) уровни целостности объектов доступа в составе объектов доступа (контейнеров);

3) уровни целостности для объектов доступа, функционально ассоциированных с субъектами доступа, в зависимости от уровней целостности субъектов доступа;

4) возможности управления одним субъектом доступа другим субъектом доступа в зависимости от их уровней целостности;