tgoop.com/computersecuritybasics/53
Last Update:
Ключевые моменты лекции 4 /
Формальная верификация
Дисклеймер: поскольку я не занимаюсь формальной верификацией ПО на постоянной основе и каждый день, а область эта постоянно развивается, я дам основные понятия и ссылки. Есть области, например формальная верификация ПО, и еще криптография, где я обладаю некоторыми знаниями, но не считаю себя экспертом – для этого пришлось бы уделять им все имеющееся у меня время.
Тем не менее, перечислим известные и применяемые методы формальной верификации. Во-первых, это model checking (проверка на модели) - метод автоматической формальной верификации параллельных систем с конечным числом состояний, позволяет проверить, удовлетворяет ли заданная модель системы формальным спецификациям.
В качестве спецификации обычно используется модель, основанная на множестве состояний, включая множество начальных состояний, отношении переходов между состояниями и т.н. функция разметки (модель Крипке).
Обычно спецификации задаются на языке формальной логики, для ПО особенно удобно использовать темпоральную логику — булеву логику с добавлением операторов времени.
Для проверки на модели особенно важно проверить полноту спецификации модели. Если спецификация модели не охватывает все нужные свойства, то результаты проверки будут малополезны.
Основной проблемой для проверки на модели является возможный «экспоненциальный взрыв» сложности проверок.
Метод дедуктивной верификации реализует проверку правильности программы относительно ее спецификации, записанной на формальном языке спецификаций. Условия корректности программы генерируются автоматически по формулам логики и спецификации программы путем применения системы логических правил. Доказательство условий корректности проводится с помощью некоторой системы автоматического доказательства. Метод ограничен ситуациями математической неразрешимости.
Кроме этих двух методов, множество авторов упоминают множество других методов. Некоторые из них действительно существенно отличаются (например, вовлекают динамические методы), другие представляют собой комбинации или улучшения известных. Мы рассматривали также методы уточнения и генерации кода (refinement and code generation) и метод абстрактной интерпретации (abstract interpretation) описываемый в неплохой статье парой европейских ученых.
Источники
Книга Ю.Г.Карпов «Model Checking»
Слайды к лекциям на ВМК МГУ, содержат в т.ч. примеры из книжки Ю.Г.Карпова и компиляцию полезной информации по формальным методам
Слайды к курсу лекций в СПб Политехе
Методичка к курсу лекций в МГУ от автора из ИСП РАН
Материалы Института системного программирования РАН (ИСП РАН)
BY Computer security basics
Share with your friend now:
tgoop.com/computersecuritybasics/53