Формальная верификация

Формальная верификация

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

Символическая верификация протокола с использованием Tamarin

Протокол WireGuard, описанный в техническом документе и основанный на Noise, был формально верифицирован в символической модели с использованием Tamarin. Это означает, что существует математическое доказательство безопасности протокола WireGuard.

Что такое символическая верификация? Символическая верификация рассматривает криптографические примитивы как “чёрные ящики” с идеальными свойствами. Она проверяет, что протокол логически корректен, при условии, что используемые криптографические примитивы безопасны. Это позволяет обнаруживать логические ошибки в протоколе, такие как неправильная последовательность сообщений или утечка информации.

Протокол был верифицирован на наличие следующих свойств безопасности:

Это совместная работа Джейсона Доненфельда (Jason Donenfeld) и Кевина Милнера (Kevin Milner).

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

Прочитать документ по верификации WireGuard в Tamarin

Модель Tamarin

Модель Tamarin является открытым исходным кодом и может быть запущена повторно для независимой верификации:

git clone https://git.zx2c4.com/wireguard-tamarin/
cd wireguard-tamarin
make

Для работы требуются:

• Tamarin — инструмент для символической верификации протоколов
• m4 — макропроцессор
• GraphViz — визуализация графов
• Maude — система для написания и выполнения спецификаций

Пример использования: Исследователь может запустить модель Tamarin для проверки нового свойства безопасности или для подтверждения существующих результатов. Модель генерирует доказательства, которые могут быть проверены математически.

Вычислительное доказательство протокола в модели eCK

При попытке построить вычислительное доказательство WireGuard в модели eCK (extended Canetti-Krawczyk) оказалось, что протокол WireGuard не вписывается аккуратно в традиционную модель eCK, потому что сообщение подтверждения ключа является частью транспортного уровня. Это техническая деталь, связанная с тем, как моделируются этапы протокола.

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

Поэтому в этом документе доказывается вариант протокола WireGuard, который морально эквивалентен реальному протоколу, давая очень сильный результат.

Что такое “морально эквивалентный”? Это означает, что вариант протокола имеет ту же логическую структуру и свойства безопасности, но адаптирован для соответствия формальным требованиям модели eCK. Доказательство для варианта применимо и к реальному протоколу.

Это совместная работа Бенджамина Даулинга (Benjamin Dowling) и Кеннета Г. Патерсона (Kenneth G. Paterson).

Прочитать документ по вычислительному доказательству в модели eCK

Вычислительное доказательство протокола в модели ACCE

Эта диссертация строит механизированное криптографическое доказательство всего протокола WireGuard, включая сообщения транспортных данных, в вычислительной модели, подобной ACCE (Authenticated and Confidential Channel Establishment), с использованием CryptoVerif.

Что такое модель ACCE? Это модель для протоколов, которые устанавливают аутентифицированные и конфиденциальные каналы. Она учитывает как установление ключей, так и последующую передачу данных, что делает её особенно подходящей для WireGuard.

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

Доказанные свойства:

Модель доступна для скачивания и может быть использована в CryptoVerif 2.00.

Это работа Бенджамина Липпа (Benjamin Lipp).

Прочитать документ по вычислительному доказательству в модели ACCE

Символическая верификация протокола с использованием ProVerif

Проект Noise Explorer стремится формально верифицировать все шаблоны протокола Noise путём генерации моделей ProVerif.

Что такое ProVerif? Это популярный инструмент для автоматической верификации криптографических протоколов в символической модели. Он может автоматически находить атаки или доказывать свойства безопасности.

Модель, относящаяся к WireGuard, — это модель IK от Noise Explorer, которая может быть подключена к ProVerif для генерации доказательств различных свойств.

Что такое шаблон IK в Noise? Это конкретный шаблон рукопожатия, используемый WireGuard. Он определяет, в каком порядке отправляются ключи и как вычисляются общие секреты.

Это работа Надима Кобейсси (Nadim Kobeissi) и Картикеяна Баргавана (Karthikeyan Bhargavan).

Прочитать документ Noise Explorer

Верифицированная C-реализация Curve25519

HACL*

WireGuard использует 64-битную реализацию умножения скаляра Curve25519 из HACL*. Кривая специфицирована в F*, что позволяет доказывать свойства стратегий реализации. KreMLin преобразует её в верифицированный C-код.

Что такое HACL?* Это библиотека криптографических примитивов, написанных на F* и верифицированных по безопасности и корректности. Она обеспечивает математические гарантии того, что реализация Curve25519 свободна от ошибок и уязвимостей.

Что такое F?* Это функциональный язык программирования с зависимыми типами, который позволяет выражать и доказывать свойства программ. Он используется для написания спецификаций криптографических примитивов.

Что такое KreMLin? Это компилятор, который преобразует код F* в верифицированный C-код, сохраняя все доказательства свойств.

HACL* — совместная работа Жана Карима Зинзиндууэ (Jean Karim Zinzindohoué), Картикеяна Баргавана (Karthikeyan Bhargavan), Джонатана Протценко (Jonathan Protzenko) и Бенджамина Беурдуше (Benjamin Beurdouche).

Прочитать документ HACL*

Fiat-Crypto

WireGuard также использует 32-битную реализацию умножения скаляра Curve25519 из Fiat-Crypto. Кривая специфицирована в Coq, что позволяет доказывать свойства стратегий реализации и генерировать верифицированный C-код.

Что такое Fiat-Crypto? Это проект по генерации верифицированного криптографического кода из формальных спецификаций в Coq. Он автоматически генерирует реализации, которые математически доказано корректны.

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

Преимущество 32-битной реализации: Она оптимизирована для устройств с 32-битными процессорами, таких как старые смартфоны или встраиваемые системы, что делает WireGuard доступным для более широкого спектра устройств.

Fiat-Crypto — совместная работа Андреса Эрбсена (Andres Erbsen), Джейд Филипум (Jade Philipoom), Джейсона Гросса (Jason Gross), Роберта Слоана (Robert Sloan) и Адама Члипала (Adam Chlipala).

Прочитать документ Fiat-Crypto

Почему формальная верификация важна?

Формальная верификация обеспечивает уровень уверенности, который невозможно достичь только тестированием или экспертной оценкой. Вот почему это критически важно для WireGuard:

1. Математические гарантии — Верификация даёт математическое доказательство того, что протокол безопасен против определённых классов атак. Это не просто “вероятно безопасно” — это “доказано безопасно”.

2. Обнаружение тонких ошибок — Некоторые уязвимости могут быть обнаружены только формальными методами. Например, атаки на протоколы, которые полагаются на тонкие логические ошибки.

3. Независимая проверка — Модели с открытым исходным кодом позволяют любому исследователю независимо проверить результаты, что повышает доверие к протоколу.

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

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

Обзор уровней верификации

graph TD
    A[Формальная верификация WireGuard] --> B[Символическая верификация]
    A --> C[Вычислительная верификация]
    A --> D[Верификация реализации]
    
    B --> B1[Tamarin]
    B --> B2[ProVerif]
    
    C --> C1[eCK модель]
    C --> C2[ACCE модель]
    
    D --> D1[HACL* 64-bit]
    D --> D2[Fiat-Crypto 32-bit]
    
    style A fill:#88171a,color:#fff
    style B fill:#2c3e50,color:#fff
    style C fill:#2c3e50,color:#fff
    style D fill:#2c3e50,color:#fff

Ссылки

• Технический документ WireGuard
• Tamarin Prover
• Noise Protocol Framework
• HACL* библиотека
• Fiat-Crypto
• Coq доказательство теорем