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

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

4.1 Для верификации формальной модели управления доступом, описание которой соответствует критериям, установленным ГОСТ Р 59453.1, должен быть осуществлен выбор соответствующих инструментальных средств, для которых должны быть представлены свидетельства, что реализуемые ими формальные методы позволяют осуществить верификацию формальной модели. При этом выбранные инструментальные средства должны допускать полную, независимую от их разработчиков проверку корректности результатов их работы.

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

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

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

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