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

     5 Выбор инструментальных средств верификации формальной модели управления доступом

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

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

5.3 Критерии выбора инструментальных средств верификации, реализующих формальные методы, поддерживающие соответствующий сформированным согласно 5.2 критериям язык формализованного (машиночитаемого) описания формальной модели управления доступом, должны быть основаны на оценке характеристик этих инструментальных средств, включая:

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

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

5.4 Должны быть представлены свидетельства соответствия выбранных согласно 5.3 инструментальных средств верификации критериям, сформулированным согласно 5.1.