AlphaProof Code demostró el cifrado de Signal con una prueba matemática completa, y el trabajo entero tomó cuatro semanas. Google DeepMind presentó el sistema el 10 de noviembre: sus agentes generaron más de seis millones de líneas de demostración en Lean, el lenguaje que permite a una computadora comprobar cada paso de un razonamiento sin margen de error.
El objetivo no era menor. El protocolo de Signal protege miles de millones de conversaciones privadas en la propia aplicación de Signal y en Google Messages.
DeepMind afirma que es la primera vez que una inteligencia artificial verifica formalmente un protocolo criptográfico de uso masivo a esta profundidad. También es la primera vez que la implementación real de un protocolo así queda verificada por cualquier método, con agentes o sin ellos.
Verificar formalmente no es probar un programa muchas veces a ver si falla. Es demostrar, con lógica matemática, que el código cumple unas propiedades concretas en cualquier situación. Ese es el estándar más alto de seguridad que existe en software, y su precio explica por qué casi nadie lo paga: un equipo de especialistas puede tardar años en cerrar una verificación de este tamaño.
El código compilado, no el dibujo del protocolo
Los análisis formales anteriores del protocolo de Signal se quedaban en el diseño, en el plano teórico. AlphaProof Code bajó un piso más: demostró que el código compilado, las instrucciones exactas que se ejecutan en los aparatos, cumple las propiedades clave.
La diferencia pesa. Las fallas reales suelen esconderse justo en ese tramo entre el diseño y el programa, como pasó con la falla de Signal que dejaba el micrófono activo tras colgar una llamada.
Entre las propiedades demostradas está la que más valoran los usuarios de mensajería cifrada: los mensajes quedan protegidos antes y después de que un dispositivo sufra un compromiso temporal. El artículo técnico del equipo detalla que el trabajo cubre el intercambio inicial de claves conocido como PQXDH y el mecanismo Triple Ratchet de las sesiones individuales, el engranaje que renueva la protección mensaje a mensaje.
El reparto de tareas copió el de un equipo de investigación. Expertos humanos trabajaron con varios modelos para traducir las metas de seguridad de Signal a especificaciones formales, y revisaron cada una de esas especificaciones.
Con esa base, agentes impulsados por Gemini Carbon escribieron las demostraciones en Lean. El sistema marcó además los puntos que pedían una segunda mirada humana: cerca del 1 % del código, con el resto comprobado de forma automática por el propio Lean.
Dos fallos viejos sirvieron de examen
Una prueba que aprueba todo no prueba nada. Para comprobar que AlphaProof Code distingue el código correcto del defectuoso, los investigadores reintrodujeron dos fallos reales, ya corregidos por Signal en su momento, dentro de una versión aislada del programa. En ambos casos el sistema produjo una demostración, verificada por computadora, de que esa versión era insegura. DeepMind no detalló cuáles eran esos dos fallos.
Ehren Kret, director de tecnología de Signal, valoró el resultado con una frase corta: da a su equipo «una confianza aún mayor en las garantías de privacidad del código». El equipo de Signal aportó comentarios sobre la metodología durante el trabajo. DeepMind publicó el artículo técnico completo y liberó los artefactos de la verificación como código abierto, de modo que cualquier especialista puede repetir las comprobaciones por su cuenta.
La letra pequeña también está en la propia página de DeepMind, y conviene leerla. El cuerpo del anuncio habla de más de seis millones de líneas de prueba; el resumen de esa misma página cita más de tres millones.
Quedan así dos versiones de la misma casa para una sola cifra. El dato firme es el orden de magnitud: millones de líneas generadas en cuatro semanas para un núcleo concreto, no para la aplicación entera de Signal ni para el teléfono completo de cada usuario.
Ese límite define lo que la verificación significa. Demuestra que el núcleo del cifrado de Signal cumple las propiedades que los expertos especificaron; no convierte a la aplicación en inatacable ni cubre fallos del sistema operativo, de la pantalla o de un aparato ya intervenido por completo.
La revisión humana de las especificaciones sigue siendo la pieza que sostiene todo el edificio: una propiedad mal definida se demuestra igual de bien, y protege igual de mal.
DeepMind apunta el método hacia terrenos donde un fallo sale mucho más caro que un mensaje leído: el programa interno de dispositivos médicos y el software de las redes eléctricas aparecen nombrados como campos de trabajo.
La combinación que plantea la casa suma agentes de reparación automática como CodeMender a esta verificación formal, para responder a ataques que ya se mueven a velocidad de máquina. Los artefactos abiertos de Signal son, desde el 10 de noviembre, el primer banco de pruebas público de esa apuesta.
Fuente: Google DeepMind
