ГОСТ Р 59453.2-2021 Защита информации. Формальная модель управления доступом. Часть 2. Рекомендации по верификации формальной модели управления доступом

     6 Формализованное (машиночитаемое) описание формальной модели управления доступом

6.1 Для верификации формальная модель управления доступом должна иметь соответствующее ГОСТ Р 59453.1 формализованное (машиночитаемое) описание. Язык описания должен позволять выполнить требования к описанию формальной модели управления доступом и быть обеспечен инструментальными средствами для ее верификации, отвечающими критериям в соответствии с 5.3.

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

6.3 При переводе математического описания в формализованное (машиночитаемое) описание формальной модели управления доступом должны быть последовательно описаны:

- элементы состояний абстрактного автомата в математическом описании формальной модели;

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

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

Примеры перевода элементов математического описания формальной модели управления доступом в формализованное (машиночитаемое) описание приведены в приложении А.

6.4 Если при переводе математического описания в формализованное (машиночитаемое) описание формальной модели управления доступом проводилась корректировка математического описания, то скорректированное математическое описание должно соответствовать ГОСТ Р 59453.1.

6.5 Если полученное в соответствии с 6.2 формализованное (машиночитаемое) описание формальной модели управления доступом имеет несоответствия ее математическому описанию, то должны быть представлены свидетельства согласованности и непротиворечивости этих описаний.