Microsoft está usando agentes de IA para demostrar matemáticamente que su código de encriptación no tiene defectos

Puntos clave

• La biblioteca SymCrypt de Microsoft, el motor de criptografía utilizado en Windows y Azure, está siendo verificada formalmente usando Rust, Lean y Aeneas a partir de mediados de 2024.
• Los primeros algoritmos verificados lanzados son SHA-3, un estándar para crear huellas digitales matemáticas de datos, y ML-KEM, un esquema de encriptación poscuántica diseñado para resistir ataques de futuros ordenadores cuánticos.
• Los agentes de IA, software que ejecuta tareas de múltiples pasos de forma autónoma, escriben pasos de prueba matemática que los ingenieros humanos revisan independientemente.
• Microsoft ha hecho código abierto el código verificado y las pruebas en una rama pública de SymCrypt, permitiendo que investigadores externos inspeccionen todo lado a lado.
• Los algoritmos futuros planeados para el mismo tratamiento incluyen AES-GCM, FrodoKEM y ML-DSA.

El código criptográfico es notoriamente inflexible. Un único control de límites omitido, que significa un fallo en confirmar que un número se mantiene dentro de un rango seguro, puede abrir la seguridad que parece sólida en la superficie. Las pruebas detectan muchos errores. No detectan todos.

Microsoft Research ha estado trabajando en un enfoque diferente: demostrar que el código es correcto, matemáticamente, antes de que se lance.

El proyecto se centra en SymCrypt, la biblioteca criptográfica de código abierto de Microsoft que se ejecuta dentro de Windows y Azure Linux. Los ingenieros escriben nuevos algoritmos criptográficos en Rust, un lenguaje que elimina familias enteras de errores de seguridad de memoria por diseño. Luego ejecutan esos programas a través de una herramienta llamada Aeneas, que traduce el código a una forma que un asistente de prueba llamado Lean puede analizar.

Lean no es un chatbot. Es un marco de prueba formal, software que verifica argumentos matemáticos de la misma manera que una calculadora verifica aritmética, excepto que verifica pruebas y nunca comete errores aritméticos.

El objetivo es un teorema: para cada entrada válida, esta implementación devuelve exactamente el resultado que el estándar publicado dice que debe devolver. No usualmente. Siempre.

El código verificado ML-KEM y SHA-3 ya está funcionando en compilaciones de prueba de Windows, por lo que esto no es un prototipo de investigación sentado en un laboratorio.

¿Cómo encaja la IA en una prueba matemática?

Escribir pruebas formales es lento. Aquí es donde entran en juego los agentes de IA.

Los agentes manejan pasos intermedios repetitivos, redactando fragmentos de prueba que conectan resultados intermedios. Los ingenieros humanos se enfocan en las partes que requieren verdadero criterio: verificar que la especificación formal coincida con lo que dice el estándar publicado y revisar las propiedades de alto nivel que el código debe satisfacer. La verificación de pruebas en sí es completamente automatizada y determinista. La máquina acepta la prueba o la rechaza. No hay espacio para que el agente blufee.

Microsoft describe esto como una división clara: los agentes escriben, los humanos revisan, el verificador de pruebas decide.

Nuestra historia del 15 de julio sobre el récord de 570 parches de seguridad de Microsoft mostró a la empresa usando IA para encontrar errores a escala. Este proyecto corre en la otra dirección: usar IA para demostrar, antes del lanzamiento, que ciertos errores no pueden existir.

¿Deberías preocuparte por las brechas?

El primer lanzamiento cubre dos algoritmos. Windows y Azure se basan en muchos más, y la hoja de ruta para AES-GCM, FrodoKEM y ML-DSA no tiene fecha de finalización pública. La verificación formal también es tan confiable como la especificación contra la que demuestra que el código es correcto. Si la especificación malinterpreta el estándar, la prueba es hermética y aún así incorrecta. La metodología de Microsoft ejecuta la especificación de Lean contra vectores de prueba oficiales precisamente para detectar ese tipo de error, pero es un paso que los humanos deben hacer bien antes de que la máquina pueda ayudar.

Para cualquiera cuyos archivos, inicios de sesión o cargas de trabajo en la nube se encuentren en la infraestructura de Microsoft, el significado práctico es real: la encriptación subyacente se está manteniendo a un estándar más estricto del que solo las pruebas pueden proporcionar. La rama de código abierto permite que investigadores externos verifiquen esa afirmación en lugar de tomar la palabra de Microsoft.

Atento a: compilaciones verificadas formalmente que llegan a lanzamientos estables de Windows, y si otras bibliotecas de criptografía adoptan flujos de trabajo de prueba asistidos por IA similares.