Microsoft Research опубликовала исходный код формальных доказательств корректности для криптографической библиотеки SymCrypt. Первый публичный релиз охватывает реализации ML-KEM и SHA3 на Rust, прошедшие полную верификацию в доказательном фреймворке Lean с использованием инструментария Aeneas. Эти алгоритмы уже используются в инсайдерских сборках Windows.
SymCrypt — это основная криптографическая библиотека Microsoft, применяемая в Windows, Azure Linux, Xbox и других платформах. Ранее она была написана преимущественно на C и ассемблере. Переход на Rust и внедрение формальной верификации — часть более широкой стратегии Microsoft по повышению безопасности базового криптографического кода.
Что опубликовано и как это работает
Microsoft открыла ветку SymCrypt на GitHub, содержащую формальные спецификации и доказательства. В отличие от исследовательских прототипов, это production-код: верифицированные реализации ML-KEM и SHA3 уже интегрированы в инсайдерские сборки Windows.
Процесс верификации построен на связке трёх компонентов:
— Rust как язык реализации. Его система владения и заимствования позволяет статически исключить целые классы ошибок работы с памятью, которые характерны для C-кода.
— Aeneas — инструмент, разработанный Microsoft Azure Research совместно с французским институтом Inria. Он транслирует mid-level представление Rust в чистую функциональную модель на Lean. Благодаря дисциплине владения Rust, Aeneas безопасно элиминирует значительную часть рассуждений об алиасинге, времени жизни и мутации, что делает верификацию масштабируемой.
— Lean — доказательный фреймворк, в котором записываются формальные спецификации и проводятся доказательства. Спецификации пишутся так, чтобы максимально близко соответствовать тексту стандарта (NIST, IETF RFC). Это упрощает аудит: рецензент может сравнивать стандарт и Lean-модель построчно.
Например, для Number Theoretic Transform (NTT) из ML-KEM спецификация на Lean буквально повторяет структуру трёх вложенных циклов из стандарта NIST, но при этом остаётся исполняемой и математически типизированной. Её можно прогнать на официальных тестовых векторах и доказать высокоуровневые алгебраические свойства.
Что это даёт на практике
Формальная верификация в данном контексте — не абстрактное упражнение. Она доказывает функциональную корректность: для любого входа, удовлетворяющего предусловиям, реализация возвращает тот же математический результат, что и спецификация, выведенная из стандарта. Это идёт дальше тестирования — даже самым тщательным набором тестов невозможно покрыть все возможные состояния программы.
Особенно это критично для постквантовой криптографии. Алгоритмы вроде ML-KEM (Kyber) сложны по структуре, содержат интенсивные математические преобразования и оптимизации под конкретные архитектуры. Ошибка в такой реализации может свести на нет криптостойкость схемы.
Дополнительный уровень защиты даёт Rust: он исключает ошибки выхода за границы буфера, use-after-free и другие уязвимости, которые могут быть использованы для атак по сторонним каналам.
Планы и масштабирование
В Microsoft подчёркивают, что это только первый шаг. SymCrypt расширяет применение того же подхода (Rust + Lean + Aeneas) на другие алгоритмы. В разработке находятся верифицированные реализации AES-GCM, FrodoKEM и ML-DSA (Dilithium). Они будут интегрированы в production-версии для Windows и Linux.
Ключевой вызов — масштабирование верификации до темпов эволюции production-кода. Как отмечает Марк Руссинович, технический Fellow Microsoft, в комментариях на LinkedIn, для ускорения процесса уже используются AI-агенты, которые помогают писать доказательства и промежуточные леммы. Однако финальная ответственность за спецификации и доверительные решения остаётся за человеком.
Практический вывод для разработчиков и исследователей
Открытие исходного кода доказательств — это не только демонстрация возможностей, но и практический инструмент. Любая организация, использующая SymCrypt (или планирующая внедрение постквантовых алгоритмов), может изучить методологию, воспроизвести верификацию и адаптировать подход для собственных критических компонентов.
Для сообщества Rust и Lean это важный прецедент: production-криптография, проверенная формальными методами, перестала быть лабораторным экспериментом. Она работает в основной операционной системе Microsoft, и её исходный код открыт для аудита.
Ограничения, которые стоит учитывать
Верификация на данный момент охватывает функциональную корректность и свойства безопасности памяти. Это не означает автоматической защиты от всех атак по сторонним каналам (timing, power analysis). Microsoft отдельно упоминает, что анализирует скомпилированный код на предмет утечек по времени, но этот процесс остаётся дополнительным этапом, не включённым в текущий публичный релиз доказательств.
Кроме того, верифицированы пока только два алгоритма. Остальная часть SymCrypt (включая унаследованные C-реализации) ещё не прошла формальную проверку. Полный переход библиотеки на Rust и верификацию — это работа на годы, а не на один релиз.