La IA escribió una prueba de 6.5 millones de líneas y Signal la pasó

El código de encriptación de Signal ahora cuenta con algo que casi ningún software de uso extendido puede afirmar: una prueba matemática de que cumple lo que promete. Un equipo de agentes de IA analizó libsignal, la biblioteca que hace funcionar el protocolo de Signal, y demostró que sus chats individuales permanecen en secreto, permiten confirmar quién está del otro lado y vuelven a dejar fuera a un atacante después del robo de una clave. No encontraron fallas nuevas.

Esto importa mucho más allá de los propios usuarios de Signal. El protocolo es el estándar global para la mensajería con cifrado de extremo a extremo, y sus variantes protegen las conversaciones en WhatsApp, Messenger y Google Messages. Revisar código real, ya implementado, con este nivel de profundidad solía ser tan lento que casi nadie lo intentaba: uno de los mayores logros del campo, la verificación de un núcleo de sistema operativo, tomó veinte años de trabajo de una persona. Este proyecto tomó cuatro semanas.

La herramienta, desarrollada por Google DeepMind, se llama AlphaProof Code. Primero, expertos humanos y modelos de IA tradujeron los objetivos de seguridad de Signal en enunciados formales en Lean, un lenguaje de programación diseñado para pruebas matemáticas; una persona revisó cada uno. Después, equipos de entre 40 y 80 agentes, impulsados por Gemini Carbon, escribieron las pruebas y trabajaron durante periodos de entre 24 y 72 horas en una sola máquina. El resultado suma cerca de 6.5 millones de líneas de Lean.

No es necesario confiar en esas millones de líneas. El núcleo de Lean comprueba cada paso y descarta cualquier prueba que no sea válida, así que da lo mismo qué modelo la haya escrito o cuántas veces se haya equivocado durante el proceso. Lo que sí hay que confiar es mucho más acotado: unas 26,000 líneas de especificaciones y un modelo de cómo un procesador ARM ejecuta el código.

Las pruebas abarcan las partes de Signal que protegen una conversación: el intercambio de claves PQXDH, que establece un chat, y el Triple Ratchet, que cambia la clave con cada mensaje, incluida la capa poscuántica, diseñada para resistir a futuras computadoras cuánticas. En la práctica, esto significa que robar las claves actuales de un teléfono no permite desbloquear mensajes antiguos, y que el ladrón vuelve a perder el acceso cuando ambas partes intercambian claves nuevas.

Para demostrar que el sistema distingue el código correcto del defectuoso, los investigadores volvieron a introducir dos errores antiguos de libsignal que ya se habían corregido. Uno hacía que la biblioteca conservara una copia de una clave secreta que debía haber descartado. En ambos casos, AlphaProof Code generó una prueba verificada por máquina de que la versión con errores era insegura.

Las limitaciones son reales. La prueba abarca únicamente las sesiones individuales, y DeepMind señala que la mensajería grupal queda para trabajos futuros. Se aplica a libsignal versión 0.105.4, compilada con el compilador estándar de Rust para ARM Linux dentro de un pequeño programa de prueba, no a las aplicaciones completas de Signal para iPhone, Android o computadoras de escritorio. Se da por sentado que los componentes criptográficos de bajo nivel son seguros; no se demuestra. Un error en las especificaciones aprobadas por humanos debilitaría la garantía, y WhatsApp y las demás aplicaciones usan sus propias versiones del protocolo, así que el resultado no se aplica automáticamente a ellas. Google también se negó a decirle a Wired cuánto costó el análisis o si planea ofrecerlo como servicio.

Signal recibió con agrado el resultado. «A medida que crecen las amenazas de seguridad impulsadas por la IA, verificar rigurosamente la implementación del protocolo de Signal nos da aún más confianza en las garantías de privacidad de nuestro código», dijo en un comunicado Ehren Kret, director de Tecnología de Signal. Swarat Chaudhuri, investigador científico de DeepMind, se mostró más cauto y le dijo a Wired que «todavía falta mucho» para que el método pueda aplicarse «a todo el software del mundo».

Quienes usan Signal no tienen que instalar nada ni cambiar ninguna configuración. La prueba se refiere al código que ya está en la aplicación.

DeepMind publicó el trabajo el 10 de noviembre, junto con un artículo técnico, y liberó las especificaciones y las pruebas como código abierto en GitHub. Describe el proyecto de Signal como un hito hacia un gran desafío de verificación formal planteado en abril, y menciona el firmware de dispositivos médicos y el software de las redes eléctricas como los tipos de sistemas que quiere revisar a continuación.

Chaudhuri también marcó un límite respecto de cuánto trabajo deberían hacer las máquinas. «No queremos un mundo de este tipo, donde la IA genere los objetivos y también las pruebas», le dijo a Wired. Los humanos siguen decidiendo qué se considera seguro; la IA solo lo demuestra.

Etiquetas: ciberseguridad, Google DeepMind, AlphaProof Code, cifrado de extremo a extremo, libsignal, Signal