ANIS: поддержка процессов верификации средств защиты информации на основе формальных моделей управления доступом

ANIS: поддержка процессов верификации средств защиты информации на основе формальных моделей управления доступом

ANIS — технология для поддержания процесса динамической верификации средств защиты информации с использованием формальной модели управления доступом. Технология разрабатывается в соответствии с ГОСТ Р 59453.4-2025, «Защита информации. Формальная модель управления доступом, Часть 4. Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом» и позволяет выполнять заложенные в документе задачи.

Особенности и преимущества

Не имеющая на данный момент аналогов технология, обеспечивающая поддержку мероприятий по динамической верификации программных систем с использованием формальных моделей, требуемых стандартом ГОСТ Р 59453.4-2025. ANIS включает в себя инструменты:

• разработки формальных моделей;
• импорта и экспорта формальных моделей в другие средства разработки;
• трансляции моделей в программный код для тестовых оракулов;
• интеграции процесса мониторинга целевой системы;
• адаптации собранных трасс исполнения к формату формальной модели;
• анализа собранных трасс исполнения;
• разработки тестов;
• запуска и отладки тестов;
• анализа покрытия по формальной модели;
• генерации отчетов.

Технология в будущем может быть расширена за счет инструментов:

• проверки формальных моделей;
• запуска онлайн-мониторинга целевой системы;
• интеграции нескольких формальных моделей разного уровня абстракции.

При разработке технологии ставилась задача упрощения обучения специалистов элементам формальных методов разработки и верификации программ. В связи с чем, помимо формального языка спецификаций Event-B, технология поддерживает и язык Python, что существенно упрощает ее внедрение в компаниях-разработчиках ПО.

Для кого предназначен ANIS

Для компаний, разрабатывающих средства защиты информации и их сотрудников:

• разработчиков формальных моделей;
• разработчиков тестов;
• инженеров, готовящих систему для сертификации.

Опыт внедрения

Технология разрабатывалась с учетом формальных моделей управления доступом операционных систем общего назначения, в частности, ОС Linux. Таким образом, была продемонстрирована работоспособность технологии для данного класса моделей. Также данная технология будет применима и для более простых формальных моделей и программных систем.

Разработанные прототипы инструментов используются в компании РусБИТех-Астра для тестирования на основе формальных моделей управления доступом Astra Linux.

Схема работы