Microsoft ha liberado como código abierto una rama de su biblioteca criptográfica SymCrypt que contiene especificaciones formales y pruebas para las implementaciones de Rust de ML-KEM y SHA-3. Este lanzamiento demuestra una metodología donde los algoritmos de producción se escriben en Rust seguro y se verifican contra modelos Lean derivados de estándares utilizando la cadena de herramientas Aeneas.
- El enfoque utiliza Aeneas para traducir la representación de nivel medio de Rust en modelos Lean puros, aprovechando las reglas de propiedad de Rust para simplificar el razonamiento sobre la seguridad de la memoria.
- Las especificaciones formales están diseñadas para reflejar estrechamente los estándares públicos como NIST o RFCs de IETF, permitiendo pruebas ejecutables contra vectores oficiales y revisión humana línea por línea.
- La rama liberada incluye pruebas completas para el código de ML-KEM y SHA-3 actualmente utilizado en compilaciones insider de Windows, con planes para extender este flujo de trabajo a AES-GCM, FrodoKEM y ML-DSA.
Esta metodología proporciona dos capas de garantía al combinar las garantías de seguridad de memoria de Rust con pruebas Lean de corrección funcional, con el objetivo de escalar la verificación formal para algoritmos criptográficos de producción.