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

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