Microsoft формально верифицировала Rust-криптографию SymCrypt с помощью Lean и ИИ-агентов
Microsoft опубликовала на своём исследовательском блоге отчёт о новой методологии формальной верификации криптографического кода в SymCrypt, криптографической библиотеке, которая используется в Windows и Azure Linux. Ещё в июне прошлого года компания объявила, что новые криптоалгоритмы будут писаться на безопасном Rust, а затем доказываться в системе формальных доказательств Lean с помощью тулчейна Aeneas. Логика в том, что тестирование и аудит проверяют код лишь на конкретных примерах, а криптографические реализации намеренно низкоуровневые, с побитовыми операциями, SIMD-инструкциями (интринсиками) под конкретный процессор и слоями переносимости под разные платформы; одна ошибка в них может свести на нет всю безопасность системы. Формальная верификация вместо выборочных тестов доказывает математическую теорему: реализация ведёт себя как положено для ВСЕХ допустимых входных данных, а не только для проверенных вручную случаев.
Первый релиз включает полные доказательства для Rust-реализаций SHA-3 и постквантового алгоритма шифрования ключей ML-KEM, этот код уже работает в инсайдерских сборках Windows. Ветка SymCrypt с формальными спецификациями и доказательствами выложена в открытый доступ, чтобы показать методологию на реальном продакшен-коде, а не на исследовательском прототипе. Дальше в работе, верификация Rust-реализаций AES-GCM, FrodoKEM и ML-DSA.
Методология работает так: сначала стандарт (спецификация NIST, IETF RFC и т.п.) вручную переводится в исполняемую модель на языке Lean, максимально близко повторяющую структуру оригинала, построчно, чтобы криптографы могли сверить стандарт и Lean-модель бок о бок; эту модель можно прогонять на официальных тестовых векторах, чтобы отловить ошибки транскрипции. Затем инструмент Aeneas автоматически переводит написанный инженерами продакшен-код на Rust в чистую функциональную модель на Lean, благодаря дисциплине владения и заимствования (ownership/borrowing) в Rust это делается без дорогостоящего анализа указателей и мутации памяти, характерного для верификации C-кода. После этого доказывается теорема: Rust-функция при соблюдении входных ограничений возвращает тот же результат, что и Lean-спецификация, выведенная из стандарта. Разработчики продолжают писать обычный производительный Rust, а верификаторы отдельно доказывают теоремы о сгенерированных Lean-моделях, код не подстраивается под нужды доказательства.
Отдельная сложность, аппаратная специфика: SymCrypt должна работать от встроенных и ядерных сред до облака и использовать платформенные SIMD-инструкции, когда они доступны (например, SSE2 на x86-64 и Neon на aarch64) с динамическим выбором нужной реализации на лету. Тулчейн компилирует код отдельно под каждую целевую платформу верификации и затем сливает получившиеся модели, превращая статический выбор реализации в Rust-коде (через атрибуты cfg) в диспетчеризацию внутри Lean-модели. Низкоуровневые обёртки, которые напрямую работают с указателями или аппаратными инструкциями, описываются вручную проверенными небольшими Lean-спецификациями, это узкое доверенное ядро, вокруг которого верифицируется остальной безопасный Rust-код.
Чтобы разработчики понимали, что именно доказано, без необходимости разбираться в Lean, команда генерирует дашборды: они на понятном инженерам языке показывают предусловия, постусловия, покрытые функции, доверенные модели и оставшиеся допущения, с прямыми ссылками на определения в Rust и Lean. В пункте «на заметку» в начале материала Microsoft также упоминает, что ИИ-агенты помогают масштабировать доказательства, самостоятельно составляя доказательства, которые затем можно независимо проверить, но подробностей о том, как именно агенты встроены в процесс, в доступном тексте статьи нет.
Ключевые факты
- Microsoft открыла ветку SymCrypt с формальными спецификациями и доказательствами для Rust-реализаций SHA-3 и постквантового ML-KEM, код уже используется в инсайдерских сборках Windows
- Метод: код на Rust инструмент Aeneas переводит в модель на языке доказательств Lean, где доказывается теорема о соответствии реализации спецификации, выведенной из стандарта NIST/IETF
- Двойная защита: сам Rust исключает целые классы ошибок работы с памятью, а доказательства в Lean подтверждают функциональную корректность алгоритма для всех допустимых входов
- Верифицируются не только эталонные версии алгоритмов, но и низкоуровневые SIMD-варианты под x86-64 (SSE2) и aarch64 (Neon) вместе с логикой выбора нужной реализации
- В планах, расширение верификации на AES-GCM, FrodoKEM и ML-DSA; Microsoft также заявляет, что ИИ-агенты помогают писать независимо проверяемые доказательства и ускоряют масштабирование
Почему это важно
Криптографический код лежит в основе операционных систем, облаков, прошивок и мессенджеров, и одна арифметическая ошибка или пропущенная проверка границ может подорвать безопасность всей системы. Тестирование и аудит проверяют лишь отдельные случаи, а продакшен-реализации криптографии специально низкоуровневые и оптимизированные, с побитовыми операциями и SIMD-инструкциями под конкретный процессор, из-за чего код почти не похож на чистый алгоритм из стандарта. Формальная верификация закрывает этот разрыв: вместо выборочных тестов она доказывает математическую теорему о том, что реализация ведёт себя корректно для всех допустимых входных данных. Публикация Microsoft, не просто анонс методологии, а первый релиз с завершёнными доказательствами для кода, который уже работает в реальных сборках Windows.
Кому это важно
В первую очередь, самой Microsoft и командам, которые поддерживают Windows и Azure Linux, где SymCrypt служит центральной криптобиблиотекой. Материал также адресован разработчикам постквантовой криптографии (ML-KEM, будущие FrodoKEM и ML-DSA), где сложность алгоритмов делает ручной аудит особенно ненадёжным, а также инженерам по формальным методам и Rust-разработчикам низкоуровневых систем, которым интересен пример верификации, не требующей переписывания продакшен-кода на специальный язык доказательств.
Как это применить
Практический рецепт из статьи: сначала спецификацию из стандарта (NIST, IETF RFC) вручную и максимально буквально переносят в исполняемую Lean-модель, которую можно прогнать на официальных тестовых векторах и сверить со стандартом построчно. Затем инструмент Aeneas автоматически переводит написанный инженерами Rust-код в чистую функциональную Lean-модель, используя гарантии владения и заимствования Rust, чтобы избежать дорогого анализа указателей. Дальше доказывается теорема о соответствии Rust-реализации и Lean-спецификации, а результаты, какие функции покрыты, какие условия доказаны, что осталось как допущение, выводятся на понятный разработчикам дашборд без необходимости открывать Lean.
Можно ли доверять
SymCrypt, не исследовательский прототип, а реальная открытая криптобиблиотека Microsoft, которая уже работает в Windows и Azure Linux; ветка с формальными спецификациями и доказательствами выложена в открытый доступ, и любой может свериться с кодом и доказательствами. В то же время это отчёт самой Microsoft о собственной технологии, без независимой сторонней оценки в тексте статьи, а сами доказательства опираются на доверенные (не доказанные, а вручную проверенные) модели низкоуровневых аппаратных обёрток.
Риски и подводные камни
Пока полностью доказаны только два алгоритма, SHA-3 и ML-KEM, остальные (AES-GCM, FrodoKEM, ML-DSA) ещё в процессе. Верификация опирается на небольшой, но всё же вручную проверяемый доверенный слой: низкоуровневые обёртки над указателями и аппаратными инструкциями описываются Lean-спецификациями, которые не доказаны формально, а лишь тщательно проверены людьми, ошибка в этом слое не будет поймана доказательствами выше. Наконец, заявление о роли ИИ-агентов в написании доказательств в доступном тексте не раскрыто подробно, так что судить о масштабе и надёжности их вклада по одной этой статье нельзя.