Моделирование и верификация политик безопасности управления доступом в операционных системах

Авторы

П.Н. Девянин, Д.В. Ефремов, В.В. Кулямин, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков

Аннотация

Монография описывает процесс разработки и верификации формальных моделей безопасности управления доступом в операционных системах и реализующих их программных компонентов на примере отечественной защищенной операционной системы специального назначения Astra Linux Special Edition. Этот процесс направлен на получение адекватной оценки характеристик защищенности и безопасности операционных систем и достижение высокого уровня доверия к полученной оценке. Помимо этого, монография знакомит читателя с современными технологиями и инструментами моделирования и верификации, используемыми в подобных процессах. Представленный процесс направлен на обеспечение выполнения требований ГОСТ Р ИСО/МЭК 15408 «Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий» и профилей защиты операционных систем общего назначения (типа «А») третьего и второго классов защиты.

Спецификации, рассматриваемые в 4, 5 и 6 главах, можно скачать здесь. Образ виртуальной машины Virtualbox с установленными инструментами верификации можно скачать здесь.

Монография издана в 2019 году научно-техническим издательством «Горячая линия – Телеком».

Полный текст статьи в формате pdf

Ключевые слова

дедуктивная верификация, модель политики безопасности, функциональная спецификация, МРОСЛ ДП-модель, Event-B, модуль безопасности ядра, ACSL, Linux

Научная группа

Технологии программирования

Все публикации за 2018 год

Все публикации