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

     4 Общие положения

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

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

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

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

4.5 Язык описания формальной модели управления доступом должен быть математическим или формализованным и должен допускать полную независимую от разработчика формальной модели проверку корректности ее описания, заданных в ней условий безопасности, а также всех выполненных в модели доказательств.

Примечание - Для формализованного (машиночитаемого) описания формальной модели управления доступом можно использовать формальные методы, например, Alloy, ASM, B, Event-B, TLA+, VDM-SL, Z, языки которых позволяют строить абстрактные автоматные модели.

4.6 Для описанных в соответствии с 4.4 условий безопасности должна быть показана их взаимосвязь с режимами функционирования средства защиты информации, разрабатываемого согласно выполненному в соответствии с 4.3 описанию абстрактного автомата и реализующего заданные в соответствии с 4.2 политики управления доступом.

Пример - Использование математического языка для задания функции прав доступа ролей.

RR = {readr, writer, executer, ownr} - множество видов прав доступа, где readr - право доступа на чтение, - право доступа на запись, - право доступа на выполнение, - право доступа на владение;

E - множество объектов доступа (сущностей);

R - множество ролей;

PA: - функция прав доступа ролей к сущностям, задающая для каждой роли множество прав доступа этой роли к сущностям .