Препринты ИСП РАН


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

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

Аннотация

Компьютерная безопасность и мобильность являются одними из самых актуальных областей исследования и разработок. В первую очередь это связано с тем, что всё большее расспространение получают компьютеры, и с тем, что всё большее их число получают возможность связываться для распределенного решения задач. Настоящий обзор, основанный на изучении более 280 работ, описывает состояние дел в области верификации функций безопасности и мобильности. Обзор состоит из двух частей.

Первая часть посвящена вопросам, связанным с верификацией безопасности. В начале её рассматриваются стандарты безопасности, как наборы требований к «безопасным» системам. Перечисляются свойства безопасности. Для каждого свойства безопасности рассматриваются различные его модели – как набор относящихся к проблеме аспектов явления. Как отдельный круг проблем, имеющих наиболее давнии традиции в изучении и решении, рассматриваются криптографические протоколы.

Затем рассматриваются способы формального описания моделей: cпецификационные языки (универсальные и специального назначения), алгебры процессов, конечные автоматы , модальные логики, сети Петри, графическое моделирование.

Этими способами формального описания определяются методы формальной верификации свойств безопасности, описываемые в следующей главе. К ним относятся: верификация на основе конечных автоматов, проверка модели (model-checking), доказательство теорем (theorem proving), метод проверки типа (type checking). Рассматриваются и другие подходы.

Как необходимое дополнение формальной верификации рассматривается и тестирование свойств безопасности. В этой же главе описаны и наиболее характерные инструменты, поддерживающие верификацию свойств безопасности.

Вторая часть обзора рассматривает проблемы, характерные для класса распределенных мобильных систем. Структура второй части повторяет структуру первой: рассматриваются модели мобильности, способы их формального описания, верификации и тестирования. Общий вывод обзора: работы в этой области ведутся с нарастающим темпом, но пока нельзя сказать, что существует «серебрянная пуля» – общий способ решения всего круга проблем.

текст в формате pdf

Вернуться к архиву препринтов