Google DeepMind usó IA para probar la seguridad del cifrado de Signal
11 de noviembre de 2026
Probar un programa no es lo mismo que demostrar que funciona. Las pruebas habituales revisan muchos casos posibles, pero nunca todos. La verificación formal va más lejos: usa la lógica matemática para demostrar que un software cumple ciertas propiedades en cualquier situación. Es el estándar más alto de seguridad que existe, y también uno de los más caros, porque exige meses o años de trabajo de especialistas.
Google DeepMind asegura haber reducido ese tiempo de forma drástica. El 10 de noviembre presentó AlphaProof Code, un sistema de agentes de inteligencia artificial que, según la compañía, verificó formalmente el código criptográfico central de Signal, una de las aplicaciones de mensajería cifrada más usadas y respetadas por los expertos en seguridad, en unas cuatro semanas.
De las olimpiadas de matemáticas al código
El nombre no es casual. AlphaProof es el sistema de DeepMind que en 2024 resolvió problemas de la Olimpiada Internacional de Matemáticas con un nivel equivalente a una medalla de plata, generando demostraciones en Lean, un lenguaje en el que una computadora puede comprobar cada paso de un razonamiento matemático sin margen de error.
AlphaProof Code lleva esa idea al software. En lugar de demostrar teoremas sobre números, demuestra que un programa hace lo que debe hacer. El proceso tiene tres etapas. Primero, varios modelos de IA traducen los objetivos de seguridad de Signal a especificaciones formales, que luego revisan expertos humanos. Después, agentes basados en Gemini Carbon, un modelo de Google, generan las demostraciones. Por último, el sistema señala las partes que necesitan revisión humana, que según DeepMind fueron alrededor del 1 % del código, mientras Lean verifica automáticamente el resto.
Seguridad en el código que realmente se ejecuta
El protocolo de Signal ya había sido analizado formalmente en el pasado, pero esos estudios se centraban en el diseño teórico del protocolo. Lo que DeepMind afirma haber verificado es el código compilado, es decir, las instrucciones que efectivamente se ejecutan en los dispositivos. La diferencia importa: muchas vulnerabilidades reales no están en la idea del protocolo, sino en errores al convertirla en software.
Entre las propiedades demostradas figura que los mensajes sigan protegidos antes y después de que un dispositivo haya sido comprometido de forma temporal, una de las características más valoradas del sistema de cifrado de Signal. Ese mismo protocolo también se usa como base en otras aplicaciones de mensajería, como WhatsApp, aunque la verificación se hizo sobre el código de Signal.
«Usar agentes de IA para traducir código en funcionamiento a teoremas válidos de Lean es un avance importante», afirmó Ehren Kret, director de tecnología de Signal, cuyo equipo dio retroalimentación sobre la metodología.
Una prueba con errores reales
Para comprobar que el sistema no se limitaba a aprobar cualquier código, los investigadores reintrodujeron dos fallos reales que Signal había corregido en el pasado en una versión aislada del software. En ambos casos, AlphaProof Code generó una demostración verificada por computadora de que esa versión era insegura. DeepMind no detalló cuáles eran esos errores.
La compañía publicó un artículo técnico y liberó como código abierto los resultados de la verificación, lo que permitirá que otros expertos revisen el trabajo.
Lo que todavía falta saber
El anuncio deja varias preguntas abiertas. DeepMind no informó cuánto costó en capacidad de cómputo ni comparó su sistema con otras herramientas de verificación. Además, la propia página da cifras distintas sobre el tamaño del trabajo: en un lugar habla de más de tres millones de líneas de prueba y en otro de más de seis millones.
También conviene recordar el límite de cualquier verificación formal: demuestra que el software cumple las propiedades que se especificaron, no que sea invulnerable a todo. Si una amenaza no se incluyó en las especificaciones, la prueba no la cubre. Por eso, la revisión humana de esas especificaciones sigue siendo clave.
Aun así, si el método escala, podría cambiar la forma en que se protege el software crítico. DeepMind menciona como posibles aplicaciones futuras el firmware de dispositivos médicos y los sistemas de las redes eléctricas, aunque aclara que llevar estas técnicas más lejos todavía requiere investigación.