Microsoft выпустила проверенный код ML-KEM и SHA-3 в SymCrypt с использованием Lean и Aeneas

Microsoft открыла исходный код ветки своей криптографической библиотеки SymCrypt, содержащей формальные спецификации и доказательства для реализаций ML-KEM и SHA-3 на Rust. Этот релиз демонстрирует методологию, при которой производственные алгоритмы пишутся на безопасном Rust и проверяются против моделей Lean, полученных из стандартов, с использованием инструментария Aeneas.

• Подход использует Aeneas для перевода среднего уровня представления Rust в чистые модели Lean, используя правила владения Rust для упрощения рассуждений о безопасности памяти.
• Формальные спецификации разработаны так, чтобы максимально соответствовать публичным стандартам, таким как NIST или IETF RFC, что позволяет проводить исполняемое тестирование против официальных векторов и построчный человеческий обзор.
• Открытая ветка включает полные доказательства для кода ML-KEM и SHA-3, который в настоящее время используется во внутренних сборках Windows, с планами расширения этого рабочего процесса на AES-GCM, FrodoKEM и ML-DSA.

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