Программные продукты и системы

Статьи из выпуска № 2 за 2025 год.

Упорядочить результаты по: Дате публикации | Заголовку статьи | Авторам

21. Динамическая верификация промышленных средств защиты информации на основе формальных моделей управления доступом [№2 за 2025 год]
Авторы: Петренко А.К., Ефремов Д.В., Корныхин Е.В., Кулямин В.В., Семенов В.А.
Просмотров: 2735
Работа посвящена методике верификации средств защиты информации (СЗИ) на соответствие формальным моде-лям безопасности. Поддержка такой верификации требуется современными стандартами разработки ПО с высоким уровнем доверия, а именно стандартами группы «Защита информации. Формальная модель управления доступом» и проектом стандарта «Защита информации. Системы с конструктивной информационной безопасностью. Методология разработки». В статье уточняется, что СЗИ – это механизм реализации требований информационной безопасности в программных системах. Обеспечение корректности и надежности его функционирования в рамках базовых программных систем промышленного уровня, таких как операционные системы или СУБД, является самостоятельной и достаточно сложной задачей. Отмечается, что при проектировании подобных систем основные свойства СЗИ должны быть заранее продуманы и точно описаны. Создавать и эффективно использовать строгие описания требований к СЗИ позволяют формальные методы разработки и верификации программ, но в классическом виде эти методы не удается масштабировать для таких крупных и сложных систем, как операционные системы или СУБД. Для верификации промышленной СЗИ предлагается использовать технику динамической верификации, в ходе которой сопоставляются трассы выполнения верифицируемой СЗИ и ее формальной модели. Поскольку мо-дель и ее реализация описаны на разных уровнях абстракции, сопоставление опирается на неклассическое отношение уточнения. Данное уточнение реализовано в виде специального медиатора, строящего последовательность событий в модели по набору событий в самой верифицируемой системе. В статье приводится алгоритм проверки полученной трассы событий на корректность в рамках формальной модели СЗИ.

◄ ← Предыдущая | 1 | 2 | 3