Верификационный театр: когда доверие к криптографии рушится

В каждой серьёзной книге по криптографии вы найдёте железное правило: «не изобретайте свои алгоритмы. Используйте проверенные библиотеки, которые прошли аудит. Доверяйте экспертам». Я сам повторяю это в курсе по криптографии для разработчиков. Это казалось незыблемым, как законы физики.

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

Исследователь Надим Кобейсси (Nadim Kobeissi) опубликовал научную работу под названием «Verification Theatre: False Assurance in Formally Verified Cryptographic Libraries». В ней описаны тринадцать уязвимостей в криптографических библиотеках libcrux, hpke-rs и libcrux-psq, которые позиционировались как «формально верифицированные». Эти библиотеки используются в мессенджере Signal — эталоне приватности и защищённых коммуникаций.

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

Что такое формальная верификация и почему она подвела

Давайте разберёмся, что вообще происходит.

Формальная верификация — это процесс математического доказательства того, что программа делает именно то, что должна. Не «мы протестировали и вроде работает», а «мы математически доказали, что это корректно». Звучит внушительно. И это действительно серьёзное достижение в области компьютерных наук.

Проекты вроде HACL* и Jasmin показали, что можно создавать код с машинно-проверенными доказательствами: корректности работы, защиты от утечек через тайминг-каналы, безопасности памяти. Это реальный прогресс.

Но есть проблема.

Как отмечают эксперты Symbolic Software, «формальная верификация на практике означает верификацию абстрактной модели с последующим доверием к тому, что компилятор, низкоуровневые процессорные инструкции, среда выполнения и аппаратура правильно реализуют эту модель. Это не верификация в том смысле, в каком пользователи понимают этот термин».

Иными словами, существует граница верификации — интерфейс между кодом с машинно-проверенными доказательствами и кодом, которому мы просто доверяем. И именно на этой границе происходят неприятности.

История с Signal

Давайте посмотрим на конкретный пример.

В ноябре 2025 года независимый исследователь Филиппо Вальсорда обнаружил, что библиотека libcrux-ml-dsa версии 0.0.3 производит разные публичные ключи и подписи на разных платформах при одинаковых входных данных. Одно и то же исходное случайное число (seed) генерировало разные ключи на Alpine Linux с процессором ARM64 и на macOS с Apple Silicon.

Проблема была в функции _vxarq_u64 — обёртке для специальной процессорной инструкции, реализующей операцию XAR в алгоритме SHA-3. Запасная версия кода (для процессоров без аппаратной поддержки SHA-3) передавала неправильные аргументы операциям сдвига битов, что приводило к повреждению хэшей SHA-3 на платформах ARM64.

В декабре 2025 года другой исследователь, GuuJiang, обнаружил баг в инкрементальном API ML-KEM (encapsulate1/encapsulate2), который приводил к несовместимости состояний между универсальной версией кода и оптимизированными версиями для разных процессоров. Это вызвало реальные сбои дешифрования в постквантовом протоколе Signal, затронув пользователей macOS, Windows, iOS и Android.

Самое интересное: Cryspen исправила эти баги, но не выпустила никакого бюллетеня безопасности. Уязвимость была задокументирована только благодаря тому, что сторонний разработчик Joe Birr-Pixton самостоятельно подал уведомление в базу RustSec.

Пять типов провалов верификации

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

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

Тип II: Неверифицированная логика протоколов. Криптографические примитивы реализованы корректно, но логика протокола, которая их использует, содержит дефекты. Например, отсутствие обязательной проверки на нулевое значение в X25519, или переполнение счётчика одноразовых чисел (nonce), что приводит к повторному использованию и компрометации шифрования.

Тип III: Неполнота спецификации. Код верифицирован относительно своей формальной спецификации, но спецификация не охватывает все свойства, необходимые для практического применения. К примеру, реализация ECDSA математически корректна по спецификации F*, но не включает нормализацию подписей (требование, чтобы определённая компонента подписи была в нижней половине диапазона значений), необходимую для Bitcoin Core и Ethereum.

Тип IV: Неверифицированная обёрточная логика. Верифицированное ядро корректно, но неверифицированный API-слой или код уровня алгоритма вводит дефекты. Например, обёртка генерации ключей Ed25519 применяет обрезание битов (clamping) к исходному значению перед хешированием, снижая эффективную случайность на 5 бит — ключ становится предсказуемее.

Тип V: Ошибки в спецификациях и доказательствах. Самое неприятное: формальная спецификация неверна, или доказательства содержат ложные утверждения, которые молча принимаются системой сборки. Например, спецификация декомпрессии в ML-KEM использует константу 1664 вместо 2^(d-1), а доказательство сериализации в ML-DSA содержит ошибку в определении границ.

Эксперты о доверии в криптографии

Проблема доверия в криптографии обсуждается давно. Ещё в 1984 году Кен Томпсон в своей знаменитой лекции «Reflections on Trusting Trust» показал, что можно внедрить бэкдор в компилятор таким образом, что он будет сам себя воспроизводить даже после удаления из исходного кода. Его мораль проста и жестока: «Вы не можете доверять коду, который не создали полностью сами».

Брюс Шнайер, один из ведущих экспертов по криптографии, постоянно подчёркивает важность независимой экспертизы. В своём блоге Schneier on Security он отмечает, что «рецензирование кода коллегами и экспертный анализ критически важны для безопасности криптографических систем» и что «математическая криптография обычно не является самым слабым звеном в цепи безопасности; эффективная защита требует комбинирования криптографии с другими мерами».

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

Как отмечают исследователи, даже в случае доверия к экспертам вроде Дэна Бернштейна (Dan Bernstein, создатель NaCl/libsodium) «мы сами можем изучить результаты их работы — алгоритмы», и «их коллеги тщательно проверяют работу друг друга». Но что делать, когда эта проверка оказывается неполной?

Сколько кода реально верифицировано

Исследование Кобейсси содержит отрезвляющую статистику. В экосистеме libcrux:

• Только 58,4% Rust-кода, составляющего развёртывание ML-KEM, имеет доказательства, проверенные автоматическим решателем логических формул (SMT-solver)
• 14,4% допущены к использованию с флагом --admit_smt_queries true (доказательства приняты без проверки)
• 11,8% аксиоматизированы через #[hax_lib::opaque]
• 15,4% вообще никогда не экстрагировались в F* для верификации

Версия кода для процессоров ARM с инструкциями NEON (используется во всех современных устройствах iOS и Android) полностью «допущена» без проверки — все 792 строки кода имеют доказательства корректности, которые система сборки приняла на веру, не проверяя.

Это не означает, что верификация бесполезна. Это означает, что утверждение «полностью верифицированная библиотека» требует уточнения: какая часть верифицирована, против каких свойств, для каких платформ?

Два подхода к прозрачности

Интересно сравнить подход Cryspen с подходом AWS к верификации своей библиотеки AWS-LC.

AWS-LC верифицирует подмножество AWS-LC (форк BoringSSL/OpenSSL) используя SAW для x86-64 и C-кода, NSym для ассемблера AArch64, Cryptol для спецификаций. В их README явно указано: «это репозиторий содержит спецификации, скрипты доказательств и другие артефакты, необходимые для формальной верификации частей AWS libcrypto».

Таблица верифицированных алгоритмов содержит явную документацию ограничений:

• Для SHA-2 (384/512): «NoEngine, MemCorrect» (не верифицированы с engine, только корректность памяти)
• Для HMAC-SHA384: специальные оговорки вроде «NoEngine, MemCorrect, IntZero, NoInline, ToolGap, LaxPointer», явно указывающие на ограничения верификации

AWS-LC запускает верификацию при каждом изменении кода для всех заявленных алгоритмов. Даже медленные проверки обязательны. У libcrux же проверка выполняется только в «мягком режиме» (lax mode — режим, где ошибки доказательств игнорируются); полная верификация запускается по расписанию или вручную, и даже на полных сборках параметр VERIFY_SLOW_MODULES=yes никогда не устанавливался ни в одной автоматической конфигурации.

Оба проекта имеют границы верификации. Оба не верифицируют абсолютно всё. Но критическое различие — в прозрачности: AWS-LC чётко документирует область верификации, а libcrux использовал девиз «the formally verified crypto library» («формально верифицированная криптобиблиотека»).

Так кому верить?

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

Если даже формально верифицированные библиотеки содержат уязвимости, если верификация от Cryspen пропустила баги, которые нашли независимые исследователи, то как быть с libsodium? С OpenSSL? С BoringSSL? С любой другой «проверенной» библиотекой?

Правда в том, что проблема не в формальной верификации как таковой. Проблема в том, что Кобейсси называет «верификационным театром» — создании видимости всеобъемлющей безопасности там, где на самом деле верифицирована лишь часть системы.

Вот что определяет верификационный театр:

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

Эшелонированная защита вместо слепого доверия

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

Вместо этого нужен системный подход:

1. Требуйте прозрачности верификации

Когда библиотека заявляет о формальной верификации, требуйте ответов:

• Какая часть кода верифицирована? В каких единицах это измеряется?
• Против каких свойств проведена верификация? (корректность, защита памяти, защита от утечек через время выполнения, независимость от секретных данных?)
• Для каких целевых платформ и архитектур?
• Какие доказательства проверены автоматически, какие приняты без проверки, какие — аксиоматизированы?
• Запускается ли верификация автоматически при каждом изменении кода?

Как рекомендует PQShield, «формальная верификация будет играть важную роль в гарантии того, что в дополнение к снижению рисков от потенциального прорыва в квантовых вычислениях, модификации IT-инфраструктуры не внесут новых уязвимостей».

2. Применяйте эшелонированную защиту

Не полагайтесь на один уровень защиты. При переходе на постквантовую криптографию эксперты рекомендуют гибридный подход: использовать ML-KEM вместе с существующими алгоритмами вроде ECDH или RSA. Аналогично для подписей — ML-DSA вместе с ECDSA или RSA.

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

3. Используйте только библиотеки с CSPRNG и валидированными модулями

Ключи должны генерироваться с использованием криптографически стойкого генератора псевдослучайных чисел (CSPRNG), идеально — внутри валидированного криптографического модуля, такого как библиотека или устройство с сертификацией FIPS 140-2/3.

4. Независимый аудит и bug bounty

Используйте библиотеки, которые проходят независимый аудит и имеют программы вознаграждения за найденные уязвимости (bug bounty). История с GuuJiang и Filippo Valsorda показывает ценность независимых исследователей.

5. Следите за практиками раскрытия уязвимостей

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

6. Проверяйте зависимости

Как показал случай с libcrux, используемой в Signal, проблема может быть в зависимости зависимости. Анализируйте всю цепочку поставок.

7. Понимайте ограничения верификации

Формальная верификация — мощный инструмент, но не панацея. Как отмечают исследователи, даже полностью верифицированный TLS 1.3 в Rust покрывает только определённые свойства на определённых уровнях абстракции. Граница верификации всегда существует.

Вывод

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

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

Проблема не в самой верификации. Проблема в разрыве между тем, что заявляется, и тем, что реально доставляется. Проблема в том, что когда сборочная система по умолчанию не проверяет доказательства, когда базовые предположения молча принимаются на веру, когда документация говорит «yes», а реальность отвечает «no» — разрыв между заявлениями и действительностью охватывает верифицированное ядро кода.

Как заключает Кобейсси:

«Эти находки не умаляют ценности формальной верификации как техники. Машинно-проверенные доказательства функциональной корректности, защиты памяти и независимости от секретных данных — это подлинные вклады в программную безопасность. То, что наши находки ставят под вопрос — это практика представления частичной верификации как всеобъемлющей гарантии».

Мы должны требовать от сообщества формальной верификации:

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

В мире, где Signal — символ защищённых коммуникаций — столкнулся с багами в «верифицированной» криптобиблиотеке, где Cryspen заблокировала GitHub-аккаунты исследователей, сообщивших о проблемах, критическое мышление становится не роскошью, а необходимостью.

Доверяй, но проверяй. И требуй прозрачности. Только так мы можем строить по-настоящему защищённые системы.

Источники

1. Verification Theatre: False Assurance in Formally Verified Cryptographic Libraries — Nadim Kobeissi, 2026. Ключевая научная работа, описывающая 13 уязвимостей в libcrux, hpke-rs и концепцию «верификационного театра». Содержит таксономию из 5 типов провалов верификации и детальный анализ того, как баги проскальзывают через формальную верификацию.
2. On the Promises of ‘High-Assurance’ Cryptography — Symbolic Software, февраль 2026. Критический анализ практик верификации Cryspen с позиции разработчиков криптографического ПО. Ставит вопрос о том, развило ли сообщество формальной верификации «привычку обещать больше, чем доставлять».
3. Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust — 2025. Описание первого результата верификации безопасности для протокольной реализации, написанной на Rust, включая первую верифицированную постквантовую библиотеку TLS 1.3.
4. Reflections on Trusting Trust — Ken Thompson, 1984. Классическая лекция при получении премии Тьюринга о том, как можно внедрить бэкдор в компилятор, который будет воспроизводить сам себя. Основополагающая работа о проблемах доверия в программных системах.
5. Formal Verification – Why It Matters — PQShield. Объяснение роли формальной верификации в постквантовой криптографии и контексте перехода на новые стандарты.
6. A Few Thoughts on Cryptographic Engineering — Matthew Green. Блог известного криптографа из Johns Hopkins University, содержащий анализ практических аспектов криптографической инженерии, trust models и проблем верификации.
7. Schneier on Security — Bruce Schneier. Блог одного из ведущих мировых экспертов по безопасности, регулярно обсуждающего проблемы доверия к криптографическим системам и важность peer review.
8. AWS LibCrypto Verification — Amazon Web Services, 2024. Репозиторий с артефактами формальной верификации частей AWS libcrypto, демонстрирующий прозрачный подход к документированию границ верификации с подробными caveats для каждого алгоритма.
9. Encryption Best Practices 2025: Complete Guide to Data Protection Standards and Implementation — Training Camp, 2025. Современное руководство по практикам защиты данных, включающее статистику о том, что более 70% уязвимостей происходит из ошибок реализации.
10. A Survey of Post-Quantum Cryptography Support in Cryptographic Libraries — 2025. Исследование состояния поддержки постквантовой криптографии в различных библиотеках, показывающее разнородность готовности к переходу.
11. Post-Quantum Cryptography Comes to Windows Insiders and Linux — Microsoft Security Blog, 2025. Объяснение гибридного подхода к постквантовой криптографии с использованием ML-KEM и ML-DSA вместе с традиционными алгоритмами для эшелонированной защиты.
12. libcrux GitHub Repository — Cryspen. Официальный репозиторий «формально верифицированной криптобиблиотеки для Rust», включающий issue reports от GuuJiang и других исследователей об обнаруженных уязвимостях.
13. Comprehensive Guide to Cryptographic Failures (OWASP Top 10 A02) — Authgear. Руководство по криптографическим провалам из OWASP Top 10 с акцентом на принцип эшелонированной защиты.
14. Revisiting Ken Thompson’s Reflection on Trusting Trust — Cesar Soto Valero, современный анализ классической работы Томпсона в контексте supply chain security.
15. Best Practices for Key Wrapping, Storage, and Management — Ubiq Security. Практические рекомендации по управлению криптографическими ключами с использованием CSPRNG и FIPS-сертифицированных модулей.