VIII Международная студенческая научная конференция Студенческий научный форум - 2016

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

Стоит отметить основные свойства таких средств [4]:

• уровень автоматизации (величина степени автоматизации, прямо пропорциональна качеству);

• простота модели (то есть, вероятны ошибки в формальной модели; чем сложнее формальная модель, тем больше вероятность ошибки);

• гибкость в смысле выразительных свойств модели (качество обратно пропорционально количеству ограничений на свойства, модулированные при разработке);

• ограничения на модель в теоретико-вычислительном смысле (при усложнении конфигураций моделирования увеличивается качество);

• наличие ложных срабатываний при определении уязвимостей протокола (допускается небольшая вероятность ложного обнаружения возможной атаки);

• извлечение алгоритма атаки (возможность узнать способ эксплуатации уязвимости предпочтительнее в сравнении с индикацией наличия уязвимости протокола, с точки зрения его разработки);

• наличие сообщества исследователей и разработчиков, применяющих определенное средство верификации (что подчеркивает качество и актуальность данного средства).

Можно выделить основные подходы к верификации протоколов безопасности (и соответственно три класса методов верификации) [3]:

1) проверка на модели;

2) логический вывод (на основе доказательства свойств);

3) подход, основанный на уточнении шаблонов.

Существуют средства, реализующие какой-либо подход в “чистом виде”, другие могут совмещать в себе несколько подходов.

Подход “проверка на модели”

Метод верификации, основанный на проверке на модели, использует представление системы, как набор состояний. При этом выделяется подмножество состояний с каким-либо нарушенным критерием безопасности.

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

К универсальным средствам проверки на модели относятся: SPIN, Murphi, а также FDR2 и PRISM.

Верификация протоколов безопасности с использованием SPIN и Murphi осуществляется за счёт представления поведения участников протокола в виде, напоминающем фрагмент программы, написанном на языке Си (со специальными конструкциями, которые задают обмен данными между участниками), затем необходимо подобным образом специфицировать поведение злоумышленника (включая перехват сообщений и генерацию новых сообщений на основе известной злоумышленником информации), и, наконец, описать критерии безопасности с использованием темпоральной логики (в терминах переменных, представляющих состояние/знание участников протокола и/или злоумышленника) [1].

FDR2 основан на использовании нотации CSP для описания поведения участников протокола и, в отличие от Murphi и SPIN, использует подход уточняющей проверки на модели (refinement model checking), который заключается в том, чтобы подтвердить соответствие модели, описывающей поведение системы, реализующей проверяемый протокол, и модели, которая задает требования для данного протокола [3].

PRISM напоминает SPIN и Murphi. Отличие подразумевает моделирование в вероятностных терминах [3], что достигается за счет расширения выразительных возможностей модели на основе возможности обозначить некоторые вариации переходов из одного состояния в другое с обозначением вероятности для каждой вариации.

Средства проверки на модели, ориентированные на верификацию протоколов безопасности. К данной категории средств относятся Casper, а также частично AVISPA. Casper представляет собой надстройку над FDR2. Он позволяет использование наиболее подходящих терминов при описании протоколов. Такое описание преобразуется в CSP-модель. Компоненты, входящие в состав средства AVISPA, OFMC, SATMC и TA4SP относятся к средствам, реализующим подход проверки на модели [7].

Выполнение протокола безопасности с помощью средств Casper и частично AVISPA – это работа машины состояний, при которой и цели протокола интерпретируются на основе критерий, определяющих подмножество множества состояний, в которые система попадать не должна. Но, в отличие от универсальных средств, как SPIN и Murphi, существуют способы, которые существенно уменьшают зону исследования состояния системы, что говорит о более широкой возможности применения данных средств [3].

Подход “Логический вывод”

Метод верификации, основанный на логическом выводе, включается в описании протокола и действий злоумышленника в рамках некоторой формальной логики, в рамках которой происходит формулирование критерия безопасности протокола как утверждения, затем необходимо его доказать, возможно, с использованием автоматических или автоматизированных средств [2].

При применении метода логического вывода различают средства автоматизации доказательств общего назначения и средства, специально ориентированные на работу с протоколами безопасности.

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

Использование Isabelle подразумевает самостоятельное построение логической теории и доказательства в ее рамках каких-либо утверждений. Автоматическое доказательство исключено из-за теоретических рамок. Но можно выполнить автоматически отдельные фрагменты логического вывода. То есть, пока какое-либо утверждение не доказано, невозможно сказать определенно, почему. Возможно, причина в его невыводимости (тогда можно говорить об его отрицании), или же потому, что еще не определен подходящий вывод. Можно сделать вывод, что эффективность работы с Isabelle во многом зависит от начальных предположений, которые разработчик протокола делает на основании своего опыта. Однако стоит отметить гибкость данного подхода.

Средства логического вывода, ориентированные на верификацию протоколов безопасности. К данной категории средств можно отнести CAPLS, один из верификаторов, входящих в состав AVISPA (CLAtSE), и средство ProVerif.Эти средства используют разные подходы к верификации, и в отличие от Isabelle, позволяют получить какой-либо ответ о свойствах протокола, а также задавать модель протокола в терминах, соответствующих моделируемой предметной области.ProVerif является инструментом для автоматического анализ безопасности криптографических протоколов [2]. Поддержка данного средства продолжается, но не ограничиваясь этим, криптографические примитивы включают в себя: симметричное и асимметричное шифрование; цифровые подписи; хэш-функции; и не-интерактивные доказательства с нулевым знанием [5]. ProVerif способен обеспечить достижимость свойств, запись утверждений и эквивалентностей. Эти возможности особенно полезны в области компьютерной безопасности, так как они позволяют анализировать секретность и аутентификацию свойств. Кроме того, развивающиеся свойства, такие как неприкосновенность частной жизни, мониторинг и возможность проверки данных, также могут быть учтены.

Анализ протокола рассматривается с точки зрения неограниченного количества сессий и неограниченного пространства сообщений. Кроме того, ProVerif способен реконструировать атаку: когда свойство не может быть доказано, ProVerif пытается реконструировать трассировку выполнения, фальсифицируя нужное свойство [5].Основная цель ProVerif является проверка криптографических протоколов. Криптографические протоколы являются параллельными программами, которые взаимодействуют с помощью каналов связи общего пользования, такие как Интернет, чтобы достичь некоторых связанных с безопасностью целей. Эти каналы, как предполагается, контролируются очень мощной средой, которая захватывает злоумышленника с возможностями "Долев-Яо". Поскольку злоумышленник имеет полный контроль каналов связи, злоумышленник может: читать, изменять, удалять и вводить сообщения. Злоумышленник также может манипулировать данными, например, вычислить номер элемента кортежа и расшифровать сообщения, если он имеет необходимые ключи. То есть, смоделированные участники должны быть взаимно честными [2].

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

Редко ProVerif может дать ложный ответ о наличии атаки. ProVerif не может определить алгоритм атаки, а только сообщает о ее возможности без позволения построить сценарий.

Подход, основанный на уточнении шаблонов

Scyther – средство верификации протоколов, в котором реализован подход на уточнении шаблонов, подразумевает определение протокола как последовательность событий (передача сообщений, которыми обмениваются участники сеанса и сообщений, которые может вставлять злоумышленник) [6]. Что касается разработки данного средства, его можно разделить на два основные компоненты. Ядро набора инструментов Scyther является инструментом командной строки Scyther, который включает в себя характеризующие и верификационные алгоритмы. Это автономное средство является выполняет анализ протокола. Второй компонент был разработан для удобства пользователя, и содержит дополнительный графический пользовательский интерфейс для инструмента командной строки Scyther. Этот компонент выступает в качестве обертки для инструмента командной строки, а также предоставляет собой редактор протокола, и графический вывод атак или шаблонов трассировки. Текущая реализация доступна для платформ Linux и Windows [6].

Инструмент командной строки написан на языке Си, и оптимизирован для скорости верификации. Он принимает в качестве входных данных описание протокола и оптимальные параметры (такие как, границы или соответствие функций) и выводит сводный отчет и, необязательно, представления моделей шаблонов трассировки в XML или в виде графа [6]. XML-выход инструмента Scyther используется для экспериментов в отношении систематического анализа атак и их классификации.

Scyther успешно используется для верификации безопасности и конструкции протоколов, а также для поддержки теоретических исследований. Он сочетает в себе возможность верификации (доказать правильность протокола в рамках модели) и фальсификации (отыскать конкретную атаку). Так же возможна проверка синхронизации.

Данное средство широко используется студентами и исследователями, что приводит к открытию многих ранее неизвестных атак.

Объединенные подходы к верификации.

Средство AVISPA предоставляет удобные средства спецификации моделируемого протокола, тем не менее, ограничено в проверке свойств. Avispa – это набор приложений для построения и анализа формальных моделей протоколов безопасности. Модели протокола записываются в протокол на языке высокого уровня спецификации (HLPSL) [7]. Avispa описывает протоколы с указанием их свойств безопасности, а также Avispa включает набор инструментов для формального подтверждения протоколов.

Спецификация HLPSL переводится в промежуточный формат (IF), с помощью переводчика, который называется hlpsl2if [7]. IF – язык ниже уровнем, чем HLPSL. Сам переводчик вызывается автоматически. Спецификация протокола промежуточного формата (IF) затем входит в бэкэнды инструментов Avispa для его анализа, если цели безопасности удовлетворены или нарушены.

Всего Avispa включает в себя четыре компонента: OFMC, CLAtSe, SATMC и TA4SP. Список компонентов непрерывно пополняется новыми. Промежуточный формат (FI) разработан с той целью, что он будет прост для разработчиков других инструментов анализа для использования IF как языка ввода. Методы анализа четырех текущих компонентов средства Avispa дополняются (по крайней мере, частично, в том смысле, что некоторые основные методы являются общими для некоторых компонентов) и не эквивалентны, [7] могут возникнуть ситуации, в которых компоненты возвращают разные результаты. Если цель безопасности спецификации нарушается, компоненты Avispa обеспечивают отображение последовательности событий, приведших к данному нарушению. Интерфейс может также отображать след атаки в виде диаграммы последовательности сообщений.

Будучи комбинированным с точки зрения использования различных подходов к доказательству заданных свойств, оно жестко ограничивает набор свойств, подлежащих проверке (на уровне языка HLPSL). AVISPA, удовлетворяя требованиям по большинству параметров, не является гибким с точки зрения набора моделируемых свойств.

Универсальное в отношении проверяемых свойств средство Isabelle не позволяет описывать проверяемый протокол удобным образом, требуя для работы наличие специфических навыков [3].

Объединение и комбинирование разных средств верификации необходимо в условии отсутствия единственного совершенного средства при решении задач верификации.

Можно выделить два типа комбинированных средств верификации [3]:

1) применение определенных средств для проверки определенных свойств;

2) обобщение с помощью Isabelle.

Первый тип подразумевает то, что средства, которые направлены непосредственно на верификацию протоколов безопасности (такие как, AVISPA, ProVerif), применяются при верификации стандартных свойств (конфиденциальности, аутентификации), а универсальные средства используются при верификации усложненных свойств.

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

Комбинированное применение этих средств основано на принципе “определенное средство для определенного свойства”. Например, при проверке стандартных и широко известных свойств, таких как конфиденциальность и аутентификация в случае атаки “man-in-themiddle” (“человек посередине”), применяется средство AVISPA, адаптированное для подобных задач. Для верификации нестандартных свойств, таких как конфиденциальность и аутентификация в случае атаки “man-in-the-end” (“человек в конце”), и свойств, которые связаны с особенностями реализации модулей и тегов или с временными характеристиками протокола, используется средство Isabelle.

С помощью AVISPA спроектированы модели для проверки аутентификации при атаке “man-in-the-middle”. Модели с использованием Isabelle находятся на стадии разработки. Для исследования всех возможностей средства Isabelle, его применяют для доказательства стандартных свойств.

Можно сделать вывод, что не существует идеального средства верификации протоколов, которое смогло бы оптимизировать решение всех проблем. Для всесторонней верификации протокола безопасности требуется комбинация нескольких средств, позволяющая компенсировать недостатки одного средства верификации за счет достоинств другого. Подход комбинации средств подразумевает анализ и классификацию свойств существующих средств верификации (а также подходов, лежащих в их основе).

Список литературы

1. Анализ подходов к верификации функций безопасности [Текст]. Москва: Российская Академия Наук. Институт Системного программирования, 2004. – 101 с.

2. Десницкий, В. А. Разработка и верификация протокола обмена сообщениями для защиты программ на основе механизма “удаленного доверия” [Текст] / В. А. Десницкий // Защита информации. Инсайд, 2008. – 94 с.

3. Котенко, И. В. Верификация протоколов безопасности на основе комбинированного использования существующих методов и средств [Текст] / И. В. Котенко. — Труды СПИИРАН, 2009. – 310 с.

4. Черемушкин, А. В. Криптографические протоколы: основные свойства и уязвимости [Текст] / А. В. Черемушкин. – Москва: Институт криптографии, связи и информатики, 2009. – 360 с.

5. Blanchet, B. ProVerif: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial [Text] / B. Blanchet, B. Smyth, V. Cheval. - University of Birmingham, 2015. – 115 p.

6. Cremers, C. J. F. Scyther - Semantics and Verication of Security Protocols [Text] / C. J. F. Cremers. - Technische Universiteit Eindhoven, 1998. – 192 p.

7. HLPSL Tutorial: A Beginner’s Guide to Modelling and Analysing Internet Security Protocols [Text]. Information Society Technologies, The AVISPA team, 2006. – 53 p.

Код для цитирования: Скопировать