Методы формальной верификации 1.Верификация на основе конечных автоматов 2.Проверка модели (model-checking) 3.Доказательство теорем (theorem proving) 4.Метод. - презентация

1 Методы формальной верификации 1.Верификация на основе конечных автоматов 2.Проверка модели (model-checking) 3.Доказательство теорем (theorem proving) 4.Метод проверки типа (type checking) 5.Другие подходы

2 Доказательство теорем (theorem proving) D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Comm. of the ACM, vol. 20, no. 7, pp , July Реализуется путем статического определение характеристик информационного потока с помощью программ для доказательства теорем. Достоинства: большая точностью и малые накладные расходы. Инструмент Isabelle - применил Паульсон (Paulson) построен на основе метода доказательства теорем для анализа сложных протоколов Бисимуляция является основой эффективной методики доказательств, которая осуществляет доказательство классических свойств безопасности, а также устанавливает некоторую оптимизацию протокола Система TAPS и система Хуимы - специализированные алгоритмы и инструменты, основанные на методике доказательства теорем, которые настроены на анализ криптографических протоколов Раскручивающиеся условия - определения системы доказательств для процессов, обладающих свойством постоянной BNDC. Позволяет верифицировать, является ли процесс безопасным, простым инспектированием его синтаксиса, что дает возможность избежать проблемы взрыва состояний, допускает рекурсивные процессы, которые могут выполнять неограниченные последовательности действий, при этом, возможно, достигая бесконечного числа состояний. Методы доказательств теорем:

3 Метод проверки типа (type checking) Новый подход к формальному анализу протоколов, введенным Абади (Abadi) Принцип – Абади ввел тип untrusted (Un) для открытых сообщений, которые исходят от оппонента. В качестве оппонентов выступают все, кроме удостоверяющих принципалов. Сообщениям и каналам присваиваются типы (например, единица данных приватного типа появляется на открытом канале). Достоинства – является полностью автоматическим и способен оперировать с несколькими классами бесконечных систем. Недостатки – так как нарушения безопасности определены в терминах несогласованностей типа, требования безопасности, которые должны быть доказаны, должны быть сформулированы в спецификации в процессе её написания. Это отличает метод проверки типов от метода проверки модели, для которого любое свойство безопасности, которое может быть выражено в терминах темпоральной логики, может специфицироваться независимо, уже после того, как сам протокол специфицирован. M. Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5): , September 1999

4 Метод проверки типа (type checking) A. C. Myers. JFlow: Practical mostly-static information flow control. In Proc. ACM Symp. on Principles of Programming Languages, Jan. 1999, pp A. C. Myers, N. Nystrom, L. Zheng, and S. Zdancewic. Jif: Java information flow. Software release. July Компилятор Jif - метод проверки типа для статического управления информационным потоком Принцип - каждое выражение в программе имеет тип безопасности, который состоит из двух частей - обычного типа (например,int) и метки, которая описывает, как можно использовать значение. Безопасность гарантируется проверкой типов - компилятор Jif читает программу, содержащую размеченные типы, и проверка типов гарантирует, что программа не будет содержать несоответствующие информационные потоки во время выполнения.

5 G. Smith. A New Type System for Secure Information Flow. In Proc. 14th IEEE Computer Security Foundations Workshop (CSFW'01), June 11-13, Метод проверки типа (type checking) Принцип - рассматривается система типов, в которой все переменные программы классифицируются как L (открытый) или H (частный), что препятствует утечке информации о переменных H в L переменные. В многопотоковом императивном языке с вероятностным планированием это формализует свойство вероятностного невлияния. Кроме того, каждой команде присваивается тип в форме \tau_1 cmd \tau_2; это означает, что команда оперирует только переменными уровня \tau_1 (или выше) и имеет продолжительность, которая зависит только от переменных уровня \tau_2 (или ниже). Также используются типы в форме \tau cmd n для команд, которые заканчиваются точно за n шагов. Достоинства - можно предотвратить утечки информации, связанные со временем, если потребовать, чтобы никакое присваивание L-переменной не могло следовать за командой, продолжительность которой зависит от H-переменных. Появляется возможность использовать H-переменные более гибко; например, поток, в котором обрабатываются только H-переменные, всегда хорошо типизирован. Семантическая непротиворечивость (soundness) такой системы типов доказана с помощью понятия вероятностной бисимуляции. L и H классификация

6 Другие подходы B. Blanchet. Automatic Verification of Cryptographic Protocols: A Logic Programming Approach (invited talk). In 5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'03), pp. 1-3, Uppsala, Sweden, August ACM. Набор фраз Хорна (логическая программа) - методика автоматической верификации криптографических протоколов, основанная на промежуточном представлении протокола. Предназначена - верификация свойства безопасности протоколов, таких как конфиденциальность и аутентификация, полностью автоматическим способом. Достоинства - получаемые доказательства являются правильными для неограниченного числа сеансов протокола. Метод обоснования на основе слабейшего предусловия (Weakest Precondition reasoning). Предназначена - предназначался для верификации программ. Принцип - рассматривает три компонента: состояние до выполнения инструкции программы, инструкция программы непосредственно, и цель, которая должна быть истинна после того, как инструкция выполняется. Недостаток - трудность доказательства для сложных предикатов, для длинных программ, с большим количеством целей, доказательства могут быть невозможны.