Microsoft Usa Agentes de IA para Probar Matemáticamente que Su Código de Cifrado No Tiene Defectos

Puntos clave

• La biblioteca SymCrypt de Microsoft, el motor criptográfico utilizado en Windows y Azure, se está verificando formalmente usando una cadena de herramientas que combina 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 únicas de datos, y ML-KEM, un esquema de cifrado post-cuántico diseñado para resistir ataques de futuros ordenadores cuánticos.
• Los agentes de IA, software que puede llevar a cabo tareas multietapas de forma autónoma, escriben pasos de pruebas matemáticas que los ingenieros humanos revisan y verifican de forma independiente.
• Microsoft abrió el código verificado, las especificaciones y las pruebas en una rama pública de SymCrypt, permitiendo que el trabajo esté disponible para revisión externa.
• Los algoritmos futuros programados para el mismo tratamiento incluyen AES-GCM, FrodoKEM y ML-DSA, todos los cuales protegen datos en Windows y Linux actualmente.

El código criptográfico, el software que cifra y protege datos en todas las aplicaciones, navegadores y sistemas operativos, es notoriamente implacable. Una comprobación de límites omitida, es decir, una falta de confirmación de que un número se mantiene dentro de un rango seguro, puede resquebrajar la seguridad que parece sólida en la superficie. Las pruebas detectan muchos errores. No detectan todos ellos.

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

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 ahora están escribiendo nuevos algoritmos criptográficos en Rust, un lenguaje de programación que elimina familias completas de errores de seguridad de memoria por diseño. Luego ejecutan esos programas Rust a través de una herramienta llamada Aeneas, que traduce el código a una forma que un asistente de pruebas llamado Lean puede analizar.

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

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

El primer lanzamiento público cubre SHA-3, un algoritmo estándar para crear una huella digital única de cualquier dato, y ML-KEM, un esquema de intercambio de claves post-cuántico. Criptografía post-cuántica significa algoritmos construidos para mantenerse seguros incluso contra ordenadores cuánticos, máquinas que podrían romper muchos de los métodos de cifrado actuales.

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

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

Los agentes manejan los pasos repetitivos intermedios, redactando fragmentos de pruebas que conectan resultados intermedios. Los ingenieros humanos se concentran en las partes que requieren un verdadero juicio: verificar que la especificación formal realmente 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, lo que significa que la máquina acepta la prueba o la rechaza. No hay espacio para que el agente blufee.

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

Para las personas que usan Windows, Azure o cualquier servicio que dependa de la pila de seguridad de Microsoft, el significado práctico es directo. El cifrado que protege tus archivos, tus datos en la nube y tus inicios de sesión se está manteniendo a un estándar superior al que solo las pruebas pueden proporcionar. Si las pruebas pasan, el código hace exactamente lo que requiere el estándar.

La rama de código abierto permite que investigadores externos inspeccionen tanto el código Rust como las pruebas lado a lado, por lo que las afirmaciones no son solo la palabra de Microsoft.

Atento a: anuncios de compilaciones formalmente verificadas llegando a lanzamientos estables de Windows, y si otras bibliotecas de criptografía adoptan flujos de trabajo de pruebas similares asistidos por IA. Eso marcaría un cambio real en cómo la industria piensa sobre la corrección del software.