Препринт ИСП РАН 15, 2006 г.
Новости
Препринты Института системного программирования РАН, Препринт 15, 2006 г.
А.С. Косачев, В.Н. Пономаренко. Анализ подходов к верификации функций безопасности и мобильности. Стр. 1-128.
Аннотация
Компьютерная безопасность и мобильность являются одними из самых актуальных областей исследования и разработок. В первую очередь это связано с тем, что всё большее расспространение получают компьютеры, и с тем, что всё большее их число получают возможность связываться для распределенного решения задач. Настоящий обзор, основанный на изучении более 280 работ, описывает состояние дел в области верификации функций безопасности и мобильности. Обзор состоит из двух частей.
Первая часть посвящена вопросам, связанным с верификацией безопасности. В начале её рассматриваются стандарты безопасности, как наборы требований к «безопасным» системам. Перечисляются свойства безопасности. Для каждого свойства безопасности рассматриваются различные его модели – как набор относящихся к проблеме аспектов явления. Как отдельный круг проблем, имеющих наиболее давнии традиции в изучении и решении, рассматриваются криптографические протоколы.
Затем рассматриваются способы формального описания моделей: cпецификационные языки (универсальные и специального назначения), алгебры процессов, конечные автоматы , модальные логики, сети Петри, графическое моделирование.
Этими способами формального описания определяются методы формальной верификации свойств безопасности, описываемые в следующей главе. К ним относятся: верификация на основе конечных автоматов, проверка модели (model-checking), доказательство теорем (theorem proving), метод проверки типа (type checking). Рассматриваются и другие подходы.
Как необходимое дополнение формальной верификации рассматривается и тестирование свойств безопасности. В этой же главе описаны и наиболее характерные инструменты, поддерживающие верификацию свойств безопасности.
Вторая часть обзора рассматривает проблемы, характерные для класса распределенных мобильных систем. Структура второй части повторяет структуру первой: рассматриваются модели мобильности, способы их формального описания, верификации и тестирования. Общий вывод обзора: работы в этой области ведутся с нарастающим темпом, но пока нельзя сказать, что существует «серебрянная пуля» – общий способ решения всего круга проблем.