Косачев А.С., Пономаренко В.Н. Анализ подходов к верификации функций безопасности и мобильности

М.: Институт системного программирования РАН, 2004. – 101 с. В данном документе представлен обзор методов верификации функций безопасности и мобильности. Обзор основан на изучении более 280 работ, описывает состояние дел в области верификации функций безопасности и мобильности.
Исследование выполнено в рамках проекта по гранту Российского фонда фундаментальных исследований № 04-07-90308 «Верификация функций безопасности и мобильности протоколов IP». Содержание:
Безопасность.
Стандарты безопасности.
Свойства безопасности.
Модели свойств безопасности.
Конфиденциальность.
Целостность.
Доступность.
Композиционность.
Криптографические протоколы.
Методы формальной спецификации.
Спецификационные языки.
Алгебры процессов.
Мультимножественная подстановка.
Конечные автоматы.
Модальные логики.
Сети Петри.
Графическое моделирование.
Методы формальной верификации.
Верификация на основе конечных автоматов.
Проверка модели (model-checking).
Доказательство теорем (theorem proving).
Метод проверки типа (type checking).
Другие подходы.
Тестирование свойств безопасности.
Тестирование на основе спецификаций.
Другие подходы.
Инструменты для тестирования свойств безопасности.
Мобильность.
Безопасность в мобильных системах.
Свойства мобильности.
Методы спецификации мобильности.
Спецификационные языки.
Алгебры процессов.
Модальные логики.
Конечные автоматы.
Сети Петри.
Графическое моделирование.
Другие подходы.
Методы верификации мобильности.
Проверка модели.
Тестирование мобильности.