Методы динамической верификации промышленных средств защиты информации на основе формальных моделей управления доступом.

А. К. Петренко^abc, П. Н. Девянин^d, Д. В. Ефремов^c, А. А. Карнов^ac, Е. В. Корныхин^bc, В. В. Кулямин^abc, А. В. Хорошилов<sup>eabc

a</sup> Национальный исследовательский университет "Высшая школа экономики"
^b Московский государственный университет имени М. В. Ломоносова
^c Институт системного программирования им. В.П. Иванникова РАН
^d ООО «РусБИТех-Астра»
^e Московский физико-технический институт

Аннотация: В статье рассматриваются методы динамической верификации программных систем, представляющих собой средства защиты информации (СЗИ) или включающих такие средства в свой состав. Для обеспечения высокого уровня доверия и защищенности программных систем необходимо применять разные методы и технологии верификации, при этом важны не только потенциальная мощность метода, но возможность использовать его в реальных условиях промышленной разработки крупных и сложных программных систем. Строгость и точность верификации обеспечивают формальные методы, однако использование классических формальных методов диктует особые, крайне высокие требования к персоналу и влечёт за собой дополнительные трудозатраты. Статья предлагает технологию динамической верификации СЗИ, которая, с одной стороны, близка к техникам тестирования, поэтому проще для освоения инженерами-тестировщиками, и, с другой стороны, в качестве базы использует формальные модели управления доступом и спецификации внешних интерфейсов СЗИ, которые уже появляются у разработчиков ОС и СУБД, чья продукция должна соответствовать требованиям нового национального стандарта ГОСТ Р 59453.4-2025 «Защита информации. Формальная модель управления доступом. Часть 4. Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом». Данный стандарт также представлен в статье.

Ключевые слова: динамическая верификация, мониторинг, тестирование на основе моделей, формальная модель управления доступом, функциональная спецификация.

DOI: 10.15514/ISPRAS-2025-37(3)-19