Microsoft está fortaleciendo la seguridad de los nuevos algoritmos criptográficos escritos en Rust dentro del proveedor de criptografía SymCrypt, utilizado en productos como Windows y Azure, mediante verificación formal. Este enfoque va más allá de los métodos tradicionales de prueba y auditoría, buscando prevenir que incluso pequeños errores en el código criptográfico generen vulnerabilidades de seguridad críticas. Este método es especialmente crucial para algoritmos complejos como la criptografía post-cuántica.
El proceso de verificación comienza convirtiendo especificaciones públicas estandarizadas (NIST, IETF RFC) en especificaciones ejecutables dentro del marco de demostración formal Lean. Luego, la herramienta Aeneas traduce el código Rust en modelos Lean, permitiendo demostrar matemáticamente que el código Rust optimizado para rendimiento cumple con las especificaciones formales. De esta manera, se previenen errores de seguridad de memoria en Rust, mientras que las demostraciones en Lean garantizan la corrección funcional.
Esta metodología permite verificar el código de producción sin sacrificar su complejidad, incluyendo instrucciones SIMD y optimizaciones específicas de arquitectura. Además, los agentes de inteligencia artificial automatizan la creación y el mantenimiento de las demostraciones, aumentando la escalabilidad del proceso. Los desarrolladores pueden rastrear fácilmente funciones verificadas, precondiciones y supuestos mediante paneles generados automáticamente.
Este sistema proporciona demostraciones completas para implementaciones en Rust de algoritmos como SHA-3 y ML-KEM, permitiendo su uso en versiones de prueba de Windows. Microsoft planea extender este método a más algoritmos basados en Rust, como AES-GCM, FrodoKEM y ML-DSA, para integrarlos en las versiones de producción de Windows y Linux.