Microsoft формально верифицирует крипто-код на Rust с помощью Lean и AI-агентов
Microsoft внедряет формальную верификацию криптографических алгоритмов в SymCrypt: код пишут на Rust, доказывают корректность в Lean через инструмент Aeneas, а AI-агенты помогают масштабировать процесс написания доказательств. Уже верифицированы SHA-3 и ML-KEM для постквантовой криптографии, код используется в Windows.
Это первая масштабируемая методология верификации production-криптографии: математически доказанная корректность плюс безопасность памяти, без жертв в производительности. Особенно критично для постквантовой криптографии, которая защитит данные от квантовых компьютеров.
Зачем доказывать код математически
Криптографический код — фундамент безопасности в Windows, Azure, прошивках и сетевых протоколах. Одна ошибка в арифметике или проверке границ может сломать всю защиту. Тестирование важно, но недостаточно: реальный крипто-код — это не чистые алгоритмы из учебников, а оптимизированные низкоуровневые операции с битами, SIMD-инструкциями и защитой от timing-атак.
Формальная верификация решает эту проблему через машинно-проверяемые математические доказательства. Вместо "код обычно работает правильно" получаем "доказано, что работает для всех входов".
Как это работает в SymCrypt
Microsoft применяет новую методологию в SymCrypt — открытой криптобиблиотеке, которая используется в Windows и Azure Linux:
- Пишут алгоритмы на Rust — это отсекает целые классы ошибок с памятью
- Формализуют спецификации в Lean — переводят стандарты NIST/IETF в исполняемые математические модели, максимально близкие к оригиналу (можно сверять строка в строку)
- Доказывают через Aeneas — инструмент переводит Rust-код в Lean и автоматизирует большую часть доказательств
- AI-агенты пишут промежуточные леммы — масштабируют процесс, генерируя проверяемые доказательства
Что уже сделано
Опубликован открытый бранч SymCrypt с полными доказательствами для: - SHA-3 — криптографическая хеш-функция - ML-KEM — постквантовая криптография (защита от квантовых компьютеров)
Этот верифицированный код уже используется в инсайдерских сборках Windows. В работе — AES-GCM, FrodoKEM, ML-DSA.
Почему это меняет игру
Раньше формальная верификация была слишком дорогой для production-кода. Новый подход: - Верифицирует код как есть — не нужно переписывать под доказательства - Сохраняет производительность — все оптимизации остаются - Масштабируется через AI — агенты пишут рутинные доказательства, люди проверяют ключевые свойства
Постквантовая криптография особенно нуждается в этом: алгоритмы сложные, реализации быстрые и критичные для безопасности. Теперь можно доказать, что код точно реализует стандарт — не "вероятно правильно", а математически строго.
Ключевые выводы
- Microsoft верифицирует production-крипто через связку Rust (безопасность памяти) + Lean (математические доказательства корректности)
- Спецификации в Lean максимально близки к оригинальным стандартам NIST/IETF — можно сверять синтаксически строка в строку
- AI-агенты пишут промежуточные доказательства (леммы), люди фокусируются на проверке ключевых свойств и формализации стандартов
- Уже верифицированы SHA-3 и постквантовый ML-KEM, код используется в реальных сборках Windows
- Методология масштабируется: можно верифицировать код по мере разработки без потери производительности
Автор: Елена Верещагина · Источник: microsoft.com
**Это важнее, чем кажется.** Криптография — единственное место в софте, где "обычно работает" недостаточно: одна ошибка в арифметике ломает всю защиту. Microsoft впервые делает формальную верификацию масштабируемой для production: пишут на Rust (отсекает баги с памятью), доказывают в Lean (математическая корректность), а AI-агенты пишут рутинные леммы. Спецификации держат максимально близко к оригинальным стандартам — можно сверять глазами, плюс они исполняемые (прогоняют тест-векторы).
**На практике это значит:** верифицированный SHA-3 и постквантовый ML-KEM уже в инсайдерских сборках Windows, открытый код с доказательствами на GitHub. Раньше формальная верификация была академической роскошью, теперь — часть обычного dev-процесса. Для постквантовой крипты это особенно критично: алгоритмы сложные, ошибки дорогие, а тестированием не покрыть все углы. Тут либо доказано, либо нет — середины нет.
Комментарии