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

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

214 стр.

Научное издание

Формат 60х90/16 (145x215 мм)

Исполнение: в твердом переплете

ISBN 978-5-9912-0787-4

ББК 32.973.2-018.2я73

УДК 004.451.9:004.056

Аннотация

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

Для специалистов в области защиты информации, преподавателей, аспирантов; будет полезна студентам, обучающимся по направлениям подготовки и специальностям УГНПС «Информационная безопасность».

Оглавление

Предисловие

1. Формальные методы в разработке и сертификации средств защиты информации

2. Описание процесса моделирования и верификации механизма управления доступом операционной системы
2.1. Этап I. Формализация модели политики безопасности управления доступом и ее верификация
2.2. Этап II. Разработка спецификации системных вызовов ОС и доказательство ее соответствия с формальной моделью политики безопасности
2.3. Этапы III и IV. Исследование механизма управления доступом ОС
2.4. Замечание об используемой терминологии

3 Модель политики безопасности управления доступом - требования к составу и структуре модели. Базовый уровень МРОСЛ ДП-модели
3.1. Требования к составу и структуре модели
3.2. Базовый уровень МРОСЛ ДП-модели в математической нотации
3.3. Состояние системы: структуры данных модели
3.3.1. Элементы состояния системы
3.3.2. Условия консистентности модели
3.3.3. Де-юре правила перехода системы из состояния в состояние
3.3.4. Обоснование выполнения условий консистентности модели
4 Event-B спецификация базового уровня МРОСЛ ДП-модели

4.1. Формальные спецификации
4.2. Связь элементов МРОСЛ ДП-модели и элементов спецификации Event-B
4.3. Контекст
4.4. Машина
4.4.1. Переменные и инварианты
4.4.2. Событие инициализации
4.4.3. Реализация правила перехода системы из состояния в состояние в виде события
4.4.4. Использование вспомогательных параметров
4.4.5. Использование математической индукции
4.4.6. Разделение правила перехода системы из состояния в состояние на несколько событий
4.4.7. Отсутствующие в спецификации элементы МРОСЛ ДП-модели
4.4.8. Формализация свойств безопасности МРОСЛ ДП-мо\-дели
4.5. Верификация
4.6. Использование уточнения

5 Формальная функциональная спецификация
5.1. Построение соответствия между системными вызовами и правилами МРОСЛ ДП-модели
5.2. Пример формализации функциональной спецификации

6 Дедуктивная верификация модуля безопасности ядра ОС Linux
6.1. Подсистема LSM. Функционирование модуля безопасности ядра ОС Linux 12
6.2. Дедуктивная верификация кода на языке Си
6.2.1. Инструментарий
6.2.2. Пример спецификаций на языке ACSL
6.2.3. Текущие ограничения стека инструментов Frama-C/AstraVer
6.3. Процесс верификации: работы, планирование, координация
6.4. Согласование правил разработки кода
6.4.1. Работа с макросами
6.4.2. Разработка спецификаций
6.4.3. Планирование работ. Оценка сложности
6.4.4. Разработка спецификаций для функций ядра, которые использует модуль безопасности
6.4.5. Тактика верификации - рабочий цикл процесса
6.5. Пример

7 Динамический мониторинг
7.1. Управление доступом в ядре ОС Linux
7.2. Схема работы анализа
7.3. Сбор трасс ядра
7.4. Механизм воспроизведения трасс на Event-B спецификации
7.5. Интеграция дедуктивной верификации и динамического мониторинга при верификации модуля безопасности

Заключение

Используемые сокращения и обозначения

Литература

Приложения
Приложение A. Язык спецификаций Event-B
Приложение B. Среда разработки и верификации на языке Event-B

Рекомендуем

Книга

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