Google DeepMind presentó el 10 de noviembre AlphaProof Code, un sistema en el que expertos humanos deciden qué hay que demostrar y un equipo de agentes de IA escribe la demostración. Su primera prueba de fuego fue libsignal, el código que cifra los chats de Signal: en cuatro semanas, cinco personas con decenas de agentes demostraron matemáticamente que el programa compilado cumple las garantías de seguridad centrales del protocolo. No aparecieron fallas nuevas.
El protocolo de Signal es la base del cifrado de extremo a extremo de Signal y de Google Messages, entre otras apps; DeepMind dice que protege «miles de millones de conversaciones privadas». Su diseño ya se había revisado con métodos formales: Karthikeyan Bhargavan y otros criptógrafos analizaron el saludo inicial PQXDH con las herramientas ProVerif y CryptoVerif, y la empresa Cryspen probó que el componente SPQR no se cae por errores de ejecución. Pero esas revisiones miraban el diseño o partes sueltas. Entre el papel y el programa que corre en el teléfono queda un hueco, y ahí se esconden muchas vulnerabilidades: un estado que se guarda cuando no debía, una validación que falta.
Lo nuevo es que DeepMind cerró ese hueco. Sus teoremas no hablan del código fuente en Rust sino del binario: libsignal 0.105.4 compilado con el rustc de siempre a código máquina para procesadores Arm de 64 bits (AArch64). Así no hace falta confiar ni en el compilador. Las pruebas, unos 6.5 millones de líneas en el asistente de pruebas Lean, las revisa el núcleo de Lean, un programa pequeño que acepta una demostración solo si cada paso es correcto. Si un agente de IA se equivoca, la prueba simplemente no pasa.
Claves de la verificación
- Humanos deciden, agentes prueban. Investigadores y varios modelos de IA tradujeron las metas de seguridad de Signal a especificaciones en Lean, y una persona revisó cada una. Después, agentes que funcionan con Gemini Carbon escribieron las pruebas: equipos de 40 a 80 agentes trabajando de 24 a 72 horas por campaña, en una sola computadora. Según DeepMind, los expertos solo tuvieron que revisar a mano alrededor del 1 % del código.
- Qué quedó demostrado. Para las sesiones uno a uno con el saludo PQXDH y el Triple Ratchet (el Double Ratchet clásico más SPQR, su parte poscuántica): forward secrecy, es decir, que los mensajes viejos siguen a salvo si hoy roban las claves; seguridad tras un compromiso, que la sesión se recupere después de un robo; autenticación, y que el saludo inicial resista a quien guarde tráfico hoy para descifrarlo cuando existan computadoras cuánticas.
- Se confía en poco. Todo descansa en unas 26,000 líneas que sí hay que creerse: 18,000 de especificaciones y 8,000 que describen cómo se comporta cada instrucción AArch64. Los 6.5 millones de líneas escritas por la IA no necesitan revisión humana.
- Una prueba que también detecta fallas. Para comprobar que las especificaciones sirven, el equipo reintrodujo en una copia aislada dos errores reales que otros investigadores habían encontrado y que ya estaban corregidos. Uno hacía que libsignal guardara el estado de una sesión nueva, con una copia de un secreto de la clave, al recibir cierto mensaje. El sistema demostró que esa versión era insegura.
- Todo es público. Las especificaciones y las pruebas están en GitHub con licencia Apache 2.0, y cualquiera puede volver a comprobarlas con
lake build, aunque tarda horas y pide entre 15 y 34 GiB de RAM. Lo que DeepMind no publicó es AlphaProof Code: no dijo si lo venderá ni cuánto costó el trabajo. - Signal lo celebra. «Usar agentes de IA para traducir código vivo en teoremas válidos de Lean es un avance importante», dijo Ehren Kret, CTO de Signal, que añadió que las revisiones formales anteriores cubrían porciones más chicas del código.
Lo que una prueba así garantiza, y lo que no
Para quien usa Signal, el resultado no cambia nada en el teléfono, pero sube el nivel de confianza en la pieza más delicada de la app. Conviene leerlo con su letra chica, que el propio paper detalla. La prueba cubre las conversaciones uno a uno, no los chats de grupo ni el uso en varios dispositivos. Las rutinas criptográficas de bajo nivel, como AES, SHA o Kyber, se dan por correctas sin revisar su código; la parte poscuántica de SPQR que «cura» una sesión tampoco quedó demostrada. Y la app completa, con su interfaz, sus servidores y el propio teléfono, está fuera. Algunos medios titularon que DeepMind «demostró» que Signal y WhatsApp son seguros, pero WhatsApp usa el protocolo con su propia implementación, que no se revisó.
La lectura de fondo va más allá de Signal. Verificar formalmente un programa real era tan caro que solo se hacía con piezas críticas y por equipos expertos durante años. Si la IA puede escribir la mayor parte de la demostración, lo difícil pasa a ser decidir qué propiedad se quiere demostrar y escribirla bien, una tarea que sigue en manos de personas. Es la misma tendencia que mostraron este año los agentes de DeepMind que encontraron debilidades en el RSA de 1024 bits y el trabajo en que Claude escribió pruebas de seguridad para 123 bibliotecas: la IA ya ataca y defiende el software con matemáticas. DeepMind dice que su siguiente meta son sistemas como el firmware de equipos médicos y el software de la red eléctrica.
Fuente: Google DeepMind, «Introducing AlphaProof Code»; paper «Verifying Signal’s security at the machine-code level»; especificaciones y pruebas en GitHub. Imagen de portada: Google DeepMind.