Разработка методов анализа программных реализаций криптографических протоколов для обнаружения атак на основе формальной верификации и динамического анализа тема диссертации и автореферата по ВАК РФ 00.00.00, кандидат наук Писарев Илья Александрович

• Писарев Илья Александрович
• кандидат наук
• 2022

Оглавление диссертации кандидат наук Писарев Илья Александрович

ВВЕДЕНИЕ

ГЛАВА 1. АНАЛИЗ СОВРЕМЕННЫХ СРЕДСТВ ВЕРИФИКАЦИИ БЕЗОПАСНОСТИ КРИПТОГРАФИЧЕСКИХ ПРОТОКОЛОВ

1.1 Формальная верификация для анализа безопасности криптографических протоколов

1.2 Верификатор Avispa

1.3 Верификатор Scyther

1.4 Инструмент SPIN для анализа многопоточного программного обеспечения как средство анализа безопасности криптографических протоколов

1.5 Анализ программных реализаций криптографических протоколов

1.6 Выводы по первой главе

ГЛАВА 2. ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ БЕЗОПАСНОСТИ ИСХОДНЫХ КОДОВ

2.1 Общая схема верификации

2.2 Анализатор исходного кода для извлечения криптографического протокола формы Alice-Bob из программной реализации

2.3 Общий принцип для трансляции представления Alice-Bob в языки спецификаций

2.4 Алгоритм трансляции из формы описания протокола Alice-Bob в язык спецификации CAS+

2.5 Автоматизированная верификация с помощью Avispa

2.6 Выводы по второй главе

ГЛАВА 3. ДИНАМИЧЕСКИЙ АНАЛИЗ ИСХОДНЫХ КОДОВ С ИСПОЛЬЗОВАНИЕМ ЯЗЫКА PDA

3.1 Динамический анализ

3.2 Предобработка системы для применения динамического анализа

3.3 Язык PDA для описания модели атаки

3.2.1 Секция Projects

3.2.2 Секция Parameters

3.2.3 Секция MainProtocol1

3.2.4 Секция Model1

3.2.5 Секция Run

3.4 Выводы по третьей главе

ГЛАВА 4. ТЕСТИРОВАНИЕ РАЗРАБОТАННЫХ МЕТОДОВ И АНАЛИЗ ПОЛУЧЕННЫХ РЕЗУЛЬТАТОВ В СРАВНЕНИИ С СУЩЕСТВУЮЩИМИ ПОДХОДАМИ

4.1 Методика тестирования и анализа результатов

4.2 Тестирование и анализ на тестовом протоколе на основе Needham-Schroeder

4.3 Тестирование и анализ протокола электронного голосования на основе слепых посредников

4.4 Тестирование и анализ серверного P2P протокола из публичного репозитория GitHub

4.5 Тестирование и анализ протокола передачи данных CTP из публичного репозитория GitHub

4.6 Тестирование и анализ протокола защищенной передачи данных на основе алгоритма

двойного храповика из публичного репозитория GitHub

4.7 Результаты

4.8 Выводы по четвертой главе

ЗАКЛЮЧЕНИЕ

СПИСОК ОСНОВНЫХ СОКРАЩЕНИЙ И УСЛОВНЫХ ОБОЗНАЧЕНИЙ

СПИСОК ЛИТЕРАТУРЫ

СПИСОК РИСУНКОВ

СПИСОК ТАБЛИЦ

ПРИЛОЖЕНИЕ 1 Акты внедрения

ПРИЛОЖЕНИЕ 2 Свидетельство о регистрации программы для ЭВМ

Введение диссертации (часть автореферата) на тему «Разработка методов анализа программных реализаций криптографических протоколов для обнаружения атак на основе формальной верификации и динамического анализа»

ВВЕДЕНИЕ

Актуальность работы. Криптографические протоколы являются основой безопасности систем, использующих защищенную передачу данных между своими компонентами. В связи с развитием различных сервисов электронной коммерции, а также мобильных роботов, беспилотных летательных аппаратов, интернета вещей, вычислительные ресурсы в которых в большинстве случаев очень ограничены и не всегда возможно использовать хорошо известные протоколы, требуется выполнять качественный и глубокий анализ безопасности криптографических протоколов на всех этапах его разработки начиная от описания протокола на простейшем языке Alice-Bob, которое представляет собой максимально простое описание протокола в виде: одна сторона пересылает другой стороне некоторую информацию, содержащую различные данные (сообщения, ключи, временные метки, идентификаторы, случайные числа), и заканчивая практической реализацией на языке программирования в контексте разрабатываемой системы. Для оценки безопасности криптографических протоколов используется формальная верификация. Однако, формальная верификация способна обнаруживать уязвимости в криптографических протоколах до их перевода в программный код. А именно программный код является последней областью, которую требуется тщательно анализировать. Связи с этим актуальным является разработка методов, позволяющих проводить полноценную верификацию безопасности программных реализаций криптографических протоколов.

Степень разработанности темы. Существуют верификаторы (Scyther, Avispa, ProVerif, CryptoVerif, Tamarin Prover), которые позволяют проверить протокол на наличие уязвимостей и показать ход атак. В классической схеме разработки криптографических протоколов его сначала описывают на простейшем языке Alice-Bob и проверяют с помощью данных инструментов после чего реализуют на выбранном языке программирования в контексте

разрабатываемой системы. Однако, в таком случае сама реализация протоколов не проверяется несмотря на то, что при уязвимостях в программной реализации протокола на практике он перестает быть безопасным. При практической реализации протокол может быть модифицирован программистом для возможности использования протокола на практике либо могут быть допущены логические ошибки при реализации протокола, также могут быть использованы сторонние библиотеки с уже реализованными криптографическими протоколами, в которых также могут быть уязвимости. Кроме того, могут быть допущены ошибки при работе с программой, к примеру, пользователь, который должен выбирать, файл с данными, в котором содержится ключ шифрования, может выбрать не тот файл либо же сам файл будет изменен злоумышленником до момента запуска системы с криптографическим протоколом, это также может привести к уязвимостям криптографического протокола. Также сами формальные верификаторы не позволяют полноценно проанализировать протокол, поскольку в них используется абстрактное описание криптографического протокола без деталей практической реализации, а также в них не поддерживаются некоторые криптографические примитивы, такие как временные метки, режим симметричного шифрования, механизмы контроля целостности, неправильное использование которых может также приводить к уязвимостям в протоколе. Существуют работы, в которых поднимается проблема анализа безопасности исходных кодов криптографических протоколов. Описанные в них подходы позволяют извлечь структуру криптографических протоколов из исходного кода и перевести ее в простейший формат описания Alice-Bob. Далее из данного формата осуществляется трансляция в язык спецификации используемого верификатора безопасности, после чего с его помощью обнаруживаются атаки на криптографический протокол. При таком подходе становится возможным отследить случаи, когда протокол был изменен при реализации, например, добавлены дополнительные сообщения, содержащие служебные данные. Это

5

могут быть сообщения, содержащие длину посылаемой далее

последовательности, поскольку принимающей стороне необходимо знать

какой длины буфер данных ей нужно принять. Однако, такой подход не

позволяет защититься от ошибок при реализации протокола, а также не

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

требуют, чтобы в исходном коде системы были использованы специальные

аннотации в местах, где находится программная реализация

криптографического протокола. С их помощью упрощается процесс

извлечения формы Alice-Bob из исходного кода. Однако, при этом существует

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

дополнительно ложится необходимость дописывать аннотации помимо

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

накладывают ряд ограничений на возможность применения анализа

криптографических протоколов, поскольку реализованные системы, в

которых не были изначально описаны данные аннотации проверить, не

получится, либо потребуется сначала проводить анализ исходного кода

самостоятельно программистом, разбираться как работает чужой код,

дописывать, где необходимо данные аннотации, и только после этого можно

будет применить верификацию. Все эти проблемы усложняют процесс

разработки системы. Есть ряд работ, в которых предлагается специальная IDE

(Интегрированная среда разработки) для создания протоколов. Здесь протокол

описывается на простейшем языке Alice-Bob, и программа в реальном времени

проверяет безопасность протокола и в случае, если какие-то части протокола

приводят к ошибкам, то разработчику даются подсказки как это исправить,

чтобы протокол был безопасным. После создания безопасного протокола

можно сгенерировать безопасные участки исходных кодов, которые

представляют из себя реализацию криптографического протокола. При

данном подходе реализация протокола будет безопасной, однако, на выходе

получается блок кода, который программист должен будет встроить в систему

с соответствующими модификациями, которые в последствии не будут

6

проанализированы и могут содержать ошибки и изменения реализации протокола для возможности его использования в разрабатываемой системе. Во всех существующих подходах в том или ином виде протокол рассматривается в виде простейшего описания Alice-Bob отдельно от его практической реализации на языке программирования. Исходный код не анализируется должным образом в существующих методах верификации, что ограничивает возможности анализа протоколов. Таким образом, актуальным является разработка новых методов, которые позволили бы расширить возможности верификации безопасности криптографических протоколов.

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

Объектом исследования являются криптографические протоколы.

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

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

Для достижения поставленной цели были определены следующие задачи:

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

2. Разработать алгоритм извлечения протокола из исходного кода в форму Alice-Bob без использования аннотаций в коде.

3. Разработать алгоритм трансляции криптографических протоколов вида Alice-Bob в описание на языке спецификации для использования инструментов формальной верификации.

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

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

6. Разработать язык PDA (protocols dynamic analysis) для описания шаблонов атак при использовании динамического анализа.

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

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

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

Научная новизна:

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

2. Разработаны алгоритмы реализации метода автоматизированной верификации исходных кодов криптографических протоколов: анализатора исходного кода для извлечения протокола формы Alice-Bob, транслятора формы Alice-Bob в языки спецификации для использования средств формальной верификации. Создана реализация разработанных алгоритмов для программных реализаций на языке программирования C# и для языка спецификации CAS+.

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

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

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

5. Предложен новый язык PDA (protocol dynamic analyzer -динамический анализ протоколов) для описания шаблонов атак при применении динамического анализа. Язык отличается простотой и гибкостью описания элементов протокола.

На защиту выносятся следующие научные результаты:

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

2. Алгоритмы реализации метода автоматизированной верификации исходных кодов криптографических протоколов: анализатора исходного кода для извлечения протокола формы Alice-Bob, транслятора формы Alice-Bob в языки спецификации для использования средств формальной верификации.

3. Метод динамического анализа, предназначенный для выявления уязвимостей в исходном коде, связанных с логикой работы протокола и обработкой нештатных ситуаций, вызванных активными атаками злоумышленника.

4. Алгоритм предобработки анализируемой системы для создания специальной среды, используемой при запуске динамического анализа.

5. Язык PDA для описания шаблонов атак при применении динамического анализа.

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

подтверждена моделированием атак в ходе реального исполнения тестируемых систем.

Теоретическая значимость:

1. Разработан метод автоматизированной формальной верификации исходных кодов криптографических протоколов.

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

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

Внедрение. Результаты диссертационного исследования были использованы для верификации безопасности системы электронного голосования на основе слепых посредников. Это позволило выявить ряд недоработок в программной реализации системы, которые приводили к уязвимостям протокола голосования. Кроме того, ряд результатов работы был использован в грантах РФФИ №2 19-37-90151 Аспиранты «Нахождение атак на криптографические протоколы в готовых системах с использованием автоматизированной верификации безопасности по исходным кодам с применением формальной верификации и динамического анализа» и №2 18-0701347 А «Разработка и исследование методов и алгоритмов организации электронных выборов на основе современных криптографических систем». Результаты также были использованы в ходе учебного процесса в рамках курса анализ безопасности протоколов.

Апробация работы. Основные результаты работы были представлены на «10th International Conference on Security of Information and Networks» SIN 2017 (Джайпур, Индия, 2017 г.), «Multidisciplinary Symposium on Computer Science and ICT» REMS 2018 (Ставрополь, Россия, 2018 г.), «nthlnternationalConferenceonSecurity of Information and Networks» SIN 2018 (Великобритания, Кардифф, 2018г.), «International Conference on Developments in eSystems Engineering» DeSE 2019 (Казань, Россия, 2019 г.).

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

Соответствие паспорту специальности. Диссертация соответствует Тема и содержание диссертации соответствуют п. 19 («Разработка методов анализа программных реализаций криптографических протоколов для обнаружения атак на основе формальной верификации и динамического анализа») паспорта научной специальности 2.3.6 - «Методы и системы защиты информации, информационная безопасность»

Публикации. Основные результаты по теме диссертации изложены в 13 научных печатных изданиях, из которых: 8 — индексированы SCOPUS, 5 — изданы в журналах, рекомендованных ВАК. По теме диссертационного исследования было получено свидетельство об официальной регистрации программы для ЭВМ.

Структура диссертации. Диссертационная работа состоит из введения, четырёх глав, заключения, приложений, списка сокращений и обозначений, а также списка литературы, содержащего 57 наименований. Основная часть работы содержит 115 страниц машинописного текста. Работа содержит 34 рисунка, 2 таблицы.

ГЛАВА 1. АНАЛИЗ СОВРЕМЕННЫХ СРЕДСТВ ВЕРИФИКАЦИИ БЕЗОПАСНОСТИ КРИПТОГРАФИЧЕСКИХ ПРОТОКОЛОВ

1.1 Формальная верификация для анализа безопасности криптографических протоколов

Верификация криптографических протоколов - актуальная и сложная задача. В связи с развитием различных сервисов электронной коммерции, а также мобильных роботов, беспилотных летательных аппаратов, Интернета вещей, вычислительные ресурсы в которых в большинстве случаев очень ограничены и не всегда возможно использовать хорошо известные протоколы. Любой разработанный протокол должен пройти процедуру верификации. Для оценки безопасности криптографического протокола используются формальные методы проверки. Существуют верификаторы, которые позволяют проверить протокол на наличие уязвимостей и выдать список атак (Scyther [1-2], Avispa [3-4], ProVerif [5-6], CryptoVerif [7-8], Tamarin Prover [9]). Однако, проверка данными верификаторами не гарантирует безопасности реализации протокола на языке программирования. Существуют работы, в которых производится верификация реализаций известных протоколов [1012]. Однако, в них не предлагаются общие решения для любого протокола. Существуют также работы, где они предлагаются [13-14]. Описанные там методы позволяют извлечь структуру криптографических протоколов из исходного кода. В основном в данных работах осуществляется извлечение структуры протоколов, чаще всего на основе аннотаций, оставленных в исходном коде, после чего осуществляется трансляция описания протокола для использования верификатора ProVerif. Также могут быть использованы и другие верификаторы. Данный метод хоть и является более эффективным по сравнению с верификацией безопасности протокола до его реализации, но все же имеет ряд недостатков. Главным недостатком является то, что излеченная структура абстрагируется от деталей реализации, что влечет за собой вероятность не обнаружения атак на протокол. Кроме того, и само

ограничение функционала средств верификации не позволяет проверить все возможные воздействия на протокол, которые влекут собой появления атак. Есть ряд работ [15-16], в которых предлагается специальная IDE для создания протоколов. Протоколы проходят верификацию в реальном времени при их написании и после чего можно сгенерировать участки кода на выбранном языке программирования для их использования в системе. У данного подхода также есть недостатки в виде, как уже говорилось ранее, несовершенства средств формальной верификации, а также то, что сгенерированные участки кода необходимо встраивать в разрабатываемую систему, что также может привести к ошибкам и уязвимостям в протоколе. Далее будут рассмотрены наиболее популярные верификаторы безопасности более подробно.

1.2 Верификатор Avispa

Avispa представляет собой инструмент для автоматизированного анализа безопасности криптографических протоколов. Реализована под ОС linux. Архитектура включает в себя: транслятор HLPSL2IF, который переводит описание протокола из HLPSL [17] в специальный IF (Intermediate format), 4 модуля верификации OFMC [18] (on-the-fly Model-Checker), AtSe [19] (CL-based Attack Searcher), SATMC [20] (SAT-based Model-Checker), TA4SP [21] (Tree Automata-based Protocol Analyser). Принцип работы наиболее используемого модуля OFMC основан на использовании символьной проверки моделей с предварительно описанными в спецификации целями проверки и знанием сторон-участников. Для описания криптографических протоколов и их свойств безопасности используется модульный формальный язык HLPSL или более высокоуровневый язык спецификаций CAS+ [22]. В Avispa входит подсистема SPAN [23] (Security Protocol ANimator), который имеет транслятор для преобразования кода из языка CAS+ в HLPSL и позволяет визуализировать схемы взаимодействия сторон.

Язык спецификаций CAS+ является более простым в синтаксисе и позволяет быстро описать протокол. Пример описания части протокола Нидхема-Шрёдера [24] на языке CAS+ приведен ниже:

1 2

3

4

5

6

7

8

9

10 11 12

13

14

15

protocol NeedhamSchroederPublicKey; identifiers

A,B

Na,Nb

KPa,KPb

messages

1. A -> B

2. B -> A

3. A -> B

knowledge A B

user; number; public key;

{Na, A}KPb {Na, Nb}KPa {Nb}KPb

A,B,KPa,KPb; A,B,KPa,KPb;

В данном фрагменте описаны роли пользователей А, В, те данные, которые каждый пользователь знает (случайные числа Na, Nb, ключи KPa, KPb), порядок передачи сообщений и знания (knowledge) взаимодействующих сторон А,В.

Интерфейс программы показан на Рисунке 1. При использовании программы в результате проверки будет выдан соответствующий результат. В случае обнаружения атак покажется тип атаки и её ход в виде соответствующих изменений сообщений стороной злоумышленником. Если атак не обнаружено, то в выводе программы будет соответствующее сообщение, что все в порядке. С помощью кнопки «Protocol simulation» можно посмотреть схему взаимодействия сторон в протоколе. С помощью кнопки «Protocol simulation» можно посмотреть схему взаимодействия сторон в протоколе.

Рисунок 1 - Интерфейс программы

С помощью кнопки «Intruder simulation» (моделирование злоумышленника) можно посмотреть подобную схему, только с участием стороны злоумышленника, в которой отобразятся перехваченные им данные. С помощью кнопки «Attack simulation» можно увидеть схему атаки с участием злоумышленника, при условии, что в вашем протоколе обнаружилась какая-либо атака.

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

верификации, программная реализация криптографических протоколов при анализе не учитывается.

1.3 Верификатор Scyther

Scyther [25] - автоматизированный верификатор безопасности криптографических протоколов. Поддерживает временные метки, симметричные и асимметричные ключи, подпись, хеширование. В данном верификаторе описываются роли, порядок передачи сообщений, их содержимое и свойства безопасности. Проверка осуществляется в автоматическом виде. В качестве результата выдается список проверенных целей. В случае если цель не выполняется - можно посмотреть подробную информацию о найденных атаках. Поддерживается обнаружение атак на аутентификацию, атаки повтором, секретность. Протокол описывается на специальном языке. После чего можно провести его верификацию с помощью пункта меню «Verify». Пример описания и результатов верификации приведен на Рисунке 2.

Рисунок 2 - Пример описания и результат верификации

Также можно посмотреть ход атаки в виде схемы. Пример схемы приведен на Рисунке 3.

[Id 1] Protocol zad2, role R, claim type Secret

Рисунок 3 - Пример схемы атаки

Самая первая конструкция:

protocol имя протокола (I,R) {

}

Данная конструкция используется в начале описания протокола. Здесь указывается имя протокола, а внутри области, выделенной скобками, описывается сам протокол.

Role I {

}

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

Формирование значения переменной ni:

fresh ni: Nonce;

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

Использование переменной ni:

var ni: Nonce;

Значение подобной переменной присваивается при получении данного элемента из полученного текущей стороной сообщения.

Отправка сообщения:

send_1(I,R, Сообщение);

В параметрах указывается: роль отправителя, роль получателя и содержимое самого сообщения

Получение сообщения:

recv_1(I,R, Сообщение);

В параметрах указывается: роль отправителя, роль получателя и содержимое самого сообщения

Шифрование на открытом ключе:

{I,ni}pk(R)

В скобках перечисляются переменные, которые необходимо зашифровать. В данном случае это идентификатор I и случайное число ni. После скобок указывается тип ключа шифрования. Для асимметричного шифра это публичный ключ pk (public key). Также указывается сторона, публичный ключ которой используется. В данном случае это сторона R.

Шифрование на общем симметричном ключе:

{I,ni}k(I,R)

В скобках перечисляются переменные, которые необходимо защифровать. В данном случае это идентификатор I и случайное число ni. После скобок указывается тип ключа шифрования. Для симметричного шифра это публичный ключ k (key). Также указываются стороны, которые знают ключ шифрования. В данном случае это стороны I и R.

Цели проверки называются claim. Цель секретность случайного числа ni:

claim_i1(I,Secret,ni);

Общая конструкция для целей - claim_[сторона][номер цели](Параметры). В данном случае параметры: роль, тип цели, переменная для проверки. Означает, что значение должно оставаться в секрете постоянно при исполнении протокола.

Цель синхронизация (не инъективная синхронизация):

claim_r3(R,Nisynch);

Означает, что исполнение протокола завершено, сообщения были посланы в правильном порядке и что содержимое сообщений на обеих сторонах после обмена совпадает.

Также есть ряд дополнительно используемых целей:

Niagree - исполнение протокола завершено и содержимое сообщений на обеих сторонах после обмена совпадает

Alive - другая сторона выполнила какие-то действия (отослала ответ)

Weakagree - когда инициатор А закончил исполнение протокола, явно с получателем В, а В ранее исполнял протокол явно с А. (То есть не факт, что B получил нужный ответ)

Список литературы диссертационного исследования кандидат наук Писарев Илья Александрович, 2022 год

СПИСОК ЛИТЕРАТУРЫ

1. El Madhoun N. An online security protocol for NFC payment: Formally analyzed by the scyther tool. / El Madhoun N., Guenane F., Pujolle G. // 2016 Second International Conference on Mobile and Secure Services (MobiSecServ). -IEEE, 2016. - pp. 1-7. doi:10.1109/MOBISECSERV.2016.7440225

2. Yang H. Verifying Group Authentication Protocols by Scyther. / Yang H., Oleshchuk V. A., Prinz A. // J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl. - 2016. - Т. 7. -no. 2. - pp. 3-19.

3. Mir O. A secure user anonymity and authentication scheme using AVISPA for telecare medical information systems. / Mir O., van der Weide T., Lee C. C. // Journal of medical systems. - 2015. - Т. 39. - no. 9. - pp. 89. doi:10.1007/s10916-015-0265-8

4. Amin R. Design of an enhanced authentication protocol and its verification using AVISPA. / Amin R. et al. // 2016 3rd International Conference on Recent Advances in Information Technology (RAIT). - IEEE, 2016. - pp. 404-409. doi:10.1109/RAIT.2016.7507899

5. Cheval V. A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. / Cheval V., Cortier V., Turuani M. // 2018 IEEE 31st Computer Security Foundations Symposium (CSF). - IEEE, 2018. - pp. 344-358.

6. Chothia T. Automatically checking commitment protocols in proverif without false attacks. International Conference on Principles of Security and Trust. / Chothia T., Smyth B., Staite C. // Springer, Berlin, Heidelberg, 2015. - pp. 137155. doi:https://doi.org/10.1007/978-3-662-46666-7_8

7. Blanchet B. Composition theorems for cryptoverif and application to TLS 1.3. // 2018 IEEE 31st Computer Security Foundations Symposium (CSF). -IEEE, 2018. - pp. 16-30. doi: 10.1109/CSF.2018.00009

8. Eswaraiah G. Automated proofs of signatures using bilinear pairings. / Eswaraiah G., Vishwanathan R., Nedza D. // 2018 16th Annual Conference on

Privacy, Security and Trust (PST). - IEEE, 2018. - pp. 1-10. doi:10.1109/PST.2018.8514201

9. Cremers C. Symbolic security analysis using the tamarin prover. // 2017 Formal Methods in Computer Aided Design (FMCAD). - IEEE, 2017. - pp. 5-5.

10. De Ruiter J. Protocol State Fuzzing of {TLS} Implementations. / De Ruiter J., Poll E. // 24th {USENIX} Security Symposium ({USENIX} Security 15).

- 2015. - pp. 193-206.

11. Cohn-Gordon K. A formal security analysis of the signal messaging protocol. / Cohn-Gordon K. et al. // 2017 IEEE European Symposium on Security and Privacy (EuroS&P). - IEEE, 2017. - pp. 451-466.

12. Beringer L Verified Correctness and Security of OpenSSL {HMAC}. / Beringer L. et al. // 24th {USENIX} Security Symposium ({USENIX} Security 15).

- 2015. - pp. 207-221.

13. Kobeissi N. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. / Kobeissi N., Bhargavan K., Blanchet B. // 2017 IEEE European Symposium on Security and Privacy (EuroS&P). - IEEE, 2017. - pp. 435-450. doi:10.1109/EuroSP.2017.38

14. Dowling B. A cryptographic analysis of the TLS 1.3 handshake protocol candidates. / Dowling B. et al. // Proceedings of the 22nd ACM SIGSAC conference on computer and communications security. - 2015. - pp. 1197-1210.

15. Garcia R. An IDE for the design, verification and implementation of security protocols. / Garcia R., Modesti P. // 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). - IEEE, 2017. - pp. 157-163. doi: 10.1109/ISSREW.2017.69

16. Modesti P. AnBx: Automatic generation and verification of security protocols implementations. International Symposium on Foundations and Practice of Security. // Springer, Cham, 2015. - pp. 156-173. doi:10.1007/978-3-319-30303-1 10

17. Von Oheimb D. The high-level protocol specification language HLPSL developed in the EU project AVISPA // Proceedings of APPSEM 2005 workshop. - 2005. - C. 1-17.

18. Basin D. An on-the-fly model-checker for security protocol analysis / Basin D., Mödersheim S., Vigano L. // European Symposium on Research in Computer Security. - Springer, Berlin, Heidelberg, 2003. - C. 253-270.

19. Kasraoui M. Formal verification of wireless sensor key exchange protocol using AVISPA / Kasraoui M., Cabani A., Chafouk H. // 2014 International Symposium on Computer, Consumer and Control. - IEEE, 2014. - C. 387-390.

20. Armando A. SATMC: a SAT-based model checker for security protocols / Armando A., Compagna L. // European workshop on logics in artificial intelligence. - Springer, Berlin, Heidelberg, 2004. - C. 730-733.

21. Küsters R. Automata-based analysis of recursive cryptographic protocols / Küsters R., Wilke T. // Annual Symposium on Theoretical Aspects of Computer Science. - Springer, Berlin, Heidelberg, 2004. - C. 382-393.

22. Saillard R. CAS+ / Saillard R., Genet T. // March. - 2011. - T. 21. -C. 2011-2018.

23. Glouche Y. A security protocol animator tool for AVISPA / Glouche Y. et al. // ARTIST2 workshop on security specification and verification of embedded systems, Pisa. - 2006. - C. 1-7.

24. Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR // International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. - Springer, Berlin, Heidelberg, 1996. - C. 147-166.

25. Cremers C. J. F. The Scyther Tool: Verification, falsification, and analysis of security protocols // International conference on computer aided verification. - Springer, Berlin, Heidelberg, 2008. - C. 414-418.

26. Vreze A. Sdl2pml—Tool for automated generation of Promela model from SDL specification / Vreze A., Vlaovic B., Brezocnik Z. // Computer Standards & Interfaces. - 2009. - T. 31. - №. 4. - C. 779-786.

105

27. De Giacomo G. Linear temporal logic and linear dynamic logic on finite traces / De Giacomo G., Vardi M. Y. // IJCAI'13 Proceedings of the Twenty-Third international joint conference on Artificial Intelligence. - Association for Computing Machinery, 2013. - C. 854-860.

28. Mikk E. Implementing statecharts in PROMELA/SPIN //Proceedings. 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques. -IEEE, 1998. - C. 90-101.

29. Chaki S. ASPIER: An automated framework for verifying security protocol implementations / Chaki S., Datta A. // Computer Security Foundations Symposium, 2009. CSF'09. 22nd IEEE. - IEEE, 2009. - C. 172-185.

30. Goubault-Larrecq J. Cryptographic protocol analysis on real C code / Goubault-Larrecq J., Parrennes F. // International Workshop on Verification, Model Checking, and Abstract Interpretation. - Springer, Berlin, Heidelberg, 2005. - C. 363-379.

31. Goubault-Larrecq J. Cryptographic protocol analysis on real C code. / Goubault-Larrecq J., Parrennes F. // Technical report, Laboratoire Spécification et Vérification, Report LSV-09-18, 2009.

32. Jurjens J. Using interface specifications for verifying crypto-protocol implementations // Workshop on foundations of interface technologies (FIT). -2008.

33. Jurjens J. Automated security verification for crypto protocol implementations: Verifying the jessie project // Electronic Notes in Theoretical Computer Science. - 2009. - T. 250. - №. 1. - C. 123-136.

34. O'Shea N. Using Elyjah to analyse Java implementations of cryptographic protocols // Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS-2008). - 2008.

35. Backes M. Computationally sound verification of source code / Backes M., Maffei M., Unruh D. // Proceedings of the 17th ACM conference on Computer

and communications security. - ACM, 2010. - C. 387-398.

106

36. Bhargavan K. Cryptographically verified implementations for TLS // Proceedings of the 15th ACM conference on Computer and communications security. - ACM, 2008. - C. 459-468.

37. Bhargavan K. Verified reference implementations of WS-Security protocols / Bhargavan K., Fournet C., Gordon A. D. // International Workshop on Web Services and Formal Methods. - Springer, Berlin, Heidelberg, 2006. - C. 88106.

38. Bhargavan K. Verified interoperable implementations of security protocols // ACM Transactions on Programming Languages and Systems (TOPLAS). - 2008. - T. 31. - №. 1. - C. 5.

39. Bhargavan K. Verified implementations of the information card federated identity-management protocol // Proceedings of the 2008 ACM symposium on Information, computer and communications security. - ACM, 2008. - C. 123-135.

40. Bhargavan K. Cryptographically verified implementations for TLS //Proceedings of the 15th ACM conference on Computer and communications security. - ACM, 2008. - C. 459-468.

41. Garcia R. An IDE for the design, verification and implementation of security protocols / Garcia R., Modesti P. // 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), 2017. - C. 157-163.

42. Modesti P. AnBx: Automatic generation and verification of security protocols implementations // International Symposium on Foundations and Practice of Security. - Springer, Cham, 2015. - C. 156-173.

43. Babenko L., Automated verification of cryptographic protocol implementations / L. Babenko, I. Pisarev // Proceedings - International Conference on Developments in eSystems Engineering, DeSE. - 2019. - Vol. 0ctober-2019. -Art. No 9073110 - P. 849-854. - DOI 10.1109/DeSE.2019.00157.

44. Babenko, L. Cryptographic protocols implementation security verification of the electronic voting system based on blind intermediaries / L. Babenko, I. Pisarev, E. Popova // ACM International Conference Proceeding Series

107

: Proceedings of the 12th International Conference on Security of Information and Networks, SIN 2019. - 2019. - Art. No 3357641. - DOI 10.1145/3357613.3357641.

45. Babenko, L. Protocols Security Analysis Using Modern Tools Of Verification / L. Babenko, I. Pisarev // CEUR Workshop Proceedings: 2018 Multidisciplinary Symposium on Computer Science and ICT, REMS 2018. - 2018.

- Vol. 2254. - P. 11-19.

46. Babenko, L. Cryptographic protocol security verification of the electronic voting system based on blinded intermediaries / L. Babenko, I. Pisarev // Advances in Intelligent Systems and Computing. - 2019. - Vol. 875. - P. 49-57. -DOI 10.1007/978-3-030-01821-4_6.

47. Бабенко Л. К. Алгоритм анализа исходного кода C# для извлечения структуры криптографических протоколов / Бабенко Л. К., Писарев И. А. // Вопросы кибербезопасности. - 2018. - №. 4 (28). - С. 46-53.

48. Писарев И. А., Бабенко Л. К. C# парсер для извлечения структуры криптографических протоколов из исходного кода //Труды Института системного программирования РАН. - 2019. - Т. 31. - №. 3. - С. 191-202. Pisarev, I. A. C# parser for extracting cryptographic protocols structure from source code / I. A. Pisarev, L. K. Babenko // Proceedings of the Institute for System Programming of the RAS. - 2019. - Vol. 31. - No 3. - P. 191-202. - DOI 10.15514/ISPRAS-2019-31(3)-15.

49. Goloveshkin A. V. Tolerant parsing with a special kind of' Any" symbol: the algorithm and practical application / Goloveshkin A. V., Mikhalkovich S. S. // Труды Института системного программирования РАН. - 2018. - Т. 30.

- №. 4.

50. Cervesato I. The Dolev-Yao intruder is the most powerful attacker // 16th Annual Symposium on Logic in Computer Science—LICS. - 2001. - Т. 1. -С. 1-2.

51. Babenko, L. Translation of Cryptographic Protocols Description from Alice-Bob Format to CAS+ Specification Language / L. Babenko, I. Pisarev //

Advances in Intelligent Systems and Computing. - 2020. - Vol. 1156 AISC. - P. 309-318. - DOI 10.1007/978-3-030-50097-9_32.

52. Бабенко, Л. К. Верификация безопасности криптографических протоколов по исходным кодам системы электронного голосования с применением множественного бросания бюллетеней / Л. К. Бабенко, И. А. Писарев // Известия ЮФУ. Технические науки. - 2019. - № 5(207). - С. 46-57. - DOI 10.23683/2311-3103-2019-5-46-57.

53. Бабенко, Л. К. Анализ безопасности протокола системы электронного голосования на основе слепых посредников с помощью инструмента AVISPA / Л. К. Бабенко, И. А. Писарев // Известия ЮФУ. Технические науки. - 2017. - № 7(192). - С. 227-238. - DOI 10.23683/23113103-2017-7-227-238.

54. Babenko, L. Modeling replay and integrity violations attacks for cryptographic protocols source codes verification of e-voting system based on blind intermediaries / L. Babenko, I. Pisarev // ACM International Conference Proceeding Series: 13th International Conference on Security of Information and Networks, SIN

2020. - 2020. - Art. No 3433597. - P. 1-3. - DOI 10.1145/3433174.3433597.

55. Babenko, L. Comprehensive Analysis of Cryptographic Protocol Implementations Using Formal Verification and Dynamic Analysis Using the PDA Language / L. Babenko, I. Pisarev // Lecture Notes in Networks and Systems. -

2021. - Vol. 229. - P. 428-443. - DOI 10.1007/978-3-030-77445-5_40.

56. Бабенко, Л. К. Язык PDA для динамического анализа криптографических протоколов / Л. К. Бабенко, И. А. Писарев // Вопросы кибербезопасности. - 2020. - № 5(39). - С. 19-29. - DOI 10.21681/2311-34562020-05-19-29.

57. Бабенко Л. К. Электронное голосование с применением множественного бросания бюллетеней / Бабенко Л. К., Писарев И. А. // Известия Южного федерального университета. Технические науки. - 2018. -№. 5 (199). - С. 48-56.

СПИСОК РИСУНКОВ

Рисунок 1 - Интерфейс программы........................... ...................................................... 16

Рисунок 2 - Пример описания и результат верификации.................. ....................................18

Рисунок 3 - Пример схемы атаки............................. .......................................................19

Рисунок 4 - Схема протокола электронного голосования.................. ...................................26

Рисунок 5 - Процесс создания криптографического протокола и возможные проблемы на каждом

из этапов...................................... ..............................................................................27

Рисунок 6 - Группы существующих методов, позволяющих обнаружить некоторые уязвимости в

программной реализации...............................................................................................28

Рисунок 7 - Дополнительная информация о размере сообщения.............. .............................30

Рисунок 8 - Атака злоумышленника на дополнение реальных данных............ .......................30

Рисунок 9 - Общая схема верификации предлагаемым методом.............. .............................34

Рисунок 10 - Обнаруживаемые уязвимости предлагаемым методом............. .........................37

Рисунок 11 - Дерево для сообщения............................ ....................................................38

Рисунок 12 - Древовидная структура выражения в линейном виде............. ...........................39

Рисунок 13 - Пример работы алгоритма для нахождения структуры одного сообщения .... ........44

Рисунок 14 - Результат верификации тестового протокола ................ ..................................53

Рисунок 15 - Пример активной атаки злоумышленника................... .................................... 55

Рисунок 16 - Обнаруживаемые уязвимости предлагаемым методом............. ......................... 64

Рисунок 17 - Описание протокола............................ ....................................................... 68

Рисунок 18 - Результат верификации.......................... ..................................................... 69

Рисунок 19 - Описание протокола............................ ....................................................... 70

Рисунок 20 - Результат верификации.......................... ..................................................... 71

Рисунок 21 - Общая схема взаимодействия сторон (голосующий, сервер аутентификации, сервер

голосования)..................................... .......................................................................... 73

Рисунок 22 - Часть описания протокола.......................... ................................................. 75

Рисунок 23 - Верификация протокола с помощью Scyther................. .................................. 75

Рисунок 24 - Результат верификации с помощью Avispa.................. ................................... 76

Рисунок 25 - Результат верификации с помощью Avispa.................. ................................... 78

Рисунок 26 - Результат верификации с помощью Avispa.................. ................................... 80

110

Рисунок 27- Описание протокола............................ ........................................................82

Рисунок 28 - Результат верификации с помощью Avispa.................. ...................................83

Рисунок 29 - Описание протокола............................ .......................................................87

Рисунок 30 - Результат верификации с помощью Avispa.................. ...................................88

Рисунок 31 - Описание протокола............................ .......................................................92

Рисунок 32 - Результат верификации с помощью Scyther.................. ..................................93

Рисунок 33 - Описание протокола............................ .......................................................94

Рисунок 34 - Результат верификации с помощью Avispa.................. ...................................95

СПИСОК ТАБЛИЦ

Таблица 1 - Список частей сообщения 1......................... ..................................................50

Таблица 2 - Результаты тестирования при моделировании атак............... .............................98

ПРИЛОЖЕНИЕ 1 Акты внедрения

УТВЕРЖДАЮ

Директор Института КОМГТБНЛСР"Ь1Х технологии и ииформашфЯи»й безопасности Г.Е. Веселой ^^ 2022 г.

АКТ

об использовании результатов

кандидатской диссертации Писарева Ильи Александровича на тему: «Разработка методов анализа программных реализации криптографических протоколов для обнаружения а;ак наоснов^ верификации и динамического анализа» в гранте РФФИ № 18-07-01347 А

Настоящим подтверждается использование в гранте РФФИ X» 18-07-01347 А «Разработка и исследование методов и алгоритмов организации электронных выборов на основе современных криптографических систем» результатов диссертационной работы Писарева Ильи Александровича. В частности, с помощью разработанных методов верификации безопасности программных реализаций был проведен анализ безопасности для системы электронного голосования на основе слепых посредников. Это позволило выявить ряд недоработок в программной реализации системы, которые приводили к уязвимостям протокола голосования. Впоследствии уязвимости были исправлены, что обеспечило безопасность криптографического протокола электронного голосования на

практике.

Руководитель гранта РФФИ РФФИ № 18-07-01347 А, д.т.н., профессор

Си) Л.К. Бабенко

|||(> шни.|

я

■

УТВЕРЖДАЮ

к гор 11нститута

компьютерных технологии и

информаци

/ ^ '• 'Н.чц ЕИ I'

а кн<]Д

"Л беюпасности,

1Л

осзопасности Г.Е. Веселое 2022 г.

АКТ

• А • -

об использовании результатов

кандидатской диссертации Писарева Ильи Александровича на тему: «Разработка методов анализа программных реализаций криптографических протоколов для обнаружения атак на основе формальной верификации и динамического анализа» в учебном процессе

Настоящим подтверждается внедрение в учебный процесс научных и практических результатов диссертационной работы Писарева Ильи Александровича, полученных в области программных средств верификации безопасности криптографических протоколов:

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

2. Алгоритмы реализации метода автоматизированной верификации исходных кодов криптографических протоколов: анализатора исходного кода для извлечения протокола формы Alice-Bob, транслятора формы Alice-Bob в языки спецификации для использования средств формальной верификации.

3. Метод динамического анализа, предназначенный для выявления уязвимостей в исходном коде, связанных с логикой работы протокола и обработкой нештатных ситуаций, вызванных активными атаками злоумышленника.

4. Алгоритм предобработки анализируемой системы для создания специальной среды, используемой при запуске динамического анализа.

5. Язык PDA для описания шаблонов атак при применении динамического анализа.

Результаты представленной диссертации использованы при подготовке студентов по специальности 10.05.03 «Информационная безопасность автоматизированных систем» в дисциплине «Анализ безопасности протоколов»

Заведующий кафедрой БИ'1 к.т.н., доцент

Е.С. Абрамов

ПРИЛОЖЕНИЕ 2 Свидетельство о регистрации программы для ЭВМ