Анализ подходов к верификации функций безопасности и мобильности

Description

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