Институт системного программирования им. В.П. Иванникова РАН


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

Авторы

А.С.Косачев, В.Н.Пономаренко.

Аннотация

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

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

Издание

Препринт Института системного программирования РАН, № 15, 2006.

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

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

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