6,5 millones de líneas de pruebas formales para 560 KB de código: Google puso a prueba la seguridad de Signa

En cuatro semanas Google DeepMind confirmó matemáticamente garantías clave del cifrado de Signal a nivel de código máquina. El sistema AlphaProof Code verificó la implementación del protocolo, y no solo su esquema teórico. Variantes del Signal Protocol protegen la mensajería en Signal, WhatsApp, Google Messages y Messenger, pero las pruebas no se extienden automáticamente a todas las aplicaciones.

El 10 de noviembre informó Google DeepMind. Cinco especialistas supervisaron agentes de inteligencia artificial que crearon alrededor de 6,5 millones de líneas de demostraciones matemáticas en el lenguaje Lean. El verificador Lean evaluó las deducciones de forma independiente de las redes neuronales. El trabajo abarcó unos 560 KB de código, equivalentes a 140 000 instrucciones máquina de la arquitectura AArch64.

Se verificó libsignal versión 0.105.4 en una compilación de prueba de libsignal-cli. Las pruebas cubren el establecimiento de conexión segura PQXDH y el mecanismo Triple Ratchet, que actualiza las claves de forma periódica. Los autores confirmaron la confidencialidad y autenticidad de los mensajes, la protección de la conversación anterior tras el robo de claves y la recuperación de la confidencialidad bajo ciertas condiciones.

Personas formularon los requisitos de seguridad y aprobaron las especificaciones matemáticas, y la inteligencia artificial construyó las demostraciones. En la preparación de los requisitos participaron Gemini 4 Carbon y Claude Opus 5.5, mientras que las demostraciones las generaron agentes Gemini. Los desarrolladores divulgaron los detalles de la verificación y publicaron los resultados en acceso abierto.

Para poner a prueba AlphaProof Code, los autores volvieron a introducir en la compilación de prueba dos errores previamente corregidos. El primero llevaba al mantenimiento de un estado de sesión inseguro y el segundo rompía la comprobación de la clave pública al reconectarse. En ambos casos la IA demostró la violación de las garantías. Además, el equipo encontró 15 lagunas y errores en un análisis científico anterior del Double Ratchet, aunque no en el código del Signal en funcionamiento.

La verificación no abarcó los chats grupales, varios dispositivos, canales laterales de filtración ni todo el código de la aplicación móvil Signal. Parte de las pruebas contempla a un adversario cuántico, pero no hay una confirmación completa de seguridad postcuántica. El resultado se aplica a una compilación específica de AArch64 y se basa en supuestos sobre primitivas criptográficas, por lo que no garantiza la seguridad en todas las plataformas y versiones.

El alcance está limitado también en otros mensajeros. Un estudio científico independiente de 2026 detectó diferencias entre la libsignal original y la implementación de WhatsApp Web. Y la protección frente a la suplantación de interlocutor requiere un mecanismo separado: en agosto Signal añadió la verificación automática de claves. AlphaProof Code no evaluó el funcionamiento de esa función en la aplicación final.

El cifrado fuerte no excluye el robo de conversaciones por otros medios. Por ejemplo, ya se ha descrito la vinculación de un dispositivo ajeno a un chat protegido sin romper la criptografía. Google DeepMind no reveló el coste del experimento ni anunció un lanzamiento comercial de AlphaProof Code. La posibilidad de verificar con la misma rapidez otros programas grandes sigue siendo una cuestión abierta.