Un equipo de cinco personas y la inteligencia artificial demostraron el código de Signal en cuatro semanas

Cuatro semanas. Ese fue el tiempo que tardó un equipo de cinco personas de Google DeepMind, trabajando con agentes de IA, en producir pruebas verificadas por máquina de propiedades de seguridad clave en el código compilado de la biblioteca de chat principal de Signal. Las pruebas abarcan aproximadamente 6,5 millones de líneas. Los esfuerzos anteriores de gran importancia en otros sistemas requirieron años de trabajo especializado y, por lo general, necesitaron que se escribiera código para poder realizar las pruebas.

La publicación de la investigación, con fecha del 10 de noviembre de 2026, describe el método y sus limitaciones. El documento técnico adjunto presenta las cifras con mayor detalle. Este trabajo no demuestra la eficacia de la aplicación Signal en su conjunto, ni de otras aplicaciones que utilizan un diseño similar. Se trata de una demostración de propiedades específicas de libsignal, la biblioteca de referencia, para sesiones individuales, llevada al código máquina compilado que se ejecuta en la práctica.

Lo que se demostró

libsignal es la biblioteca que implementa el diseño de cifrado de Signal. En términos sencillos, este diseño busca mantener la privacidad de un mensaje incluso si la clave es robada posteriormente, y recuperarse después de que un dispositivo haya sido comprometido brevemente. Estas dos ideas se conocen generalmente como confidencialidad directa y seguridad posterior al compromiso.

El equipo compiló la biblioteca original (versión 0.105.4, junto con el paquete SPQR correspondiente, versión 1.6.0) con el compilador Rust estándar, creando una pequeña herramienta de línea de comandos que se ejecuta en Linux Arm de 64 bits. Las pruebas se refieren a ese ejecutable, no a una reescritura optimizada. La biblioteca verificada tiene un tamaño aproximado de 560 KB, o unas 140 000 instrucciones de máquina.

El documento describe el protocolo de enlace PQXDH, que permite a dos personas iniciar una sesión privada, incluyendo un paso post-cuántico diseñado para resistir a una futura computadora cuántica, y el Triple Ratchet, que genera una clave nueva para cada mensaje. En el modelo “simbólico”, que considera la criptografía subyacente como ideal, el documento también afirma que el protocolo de enlace es secreto frente a un posible atacante con una computadora cuántica. Los chats grupales, el remitente sellado y el protocolo del servidor se dejan como trabajo futuro.

Cómo se realizó el trabajo

La verificación formal consiste en escribir una declaración matemática precisa sobre lo que el código debe hacer y luego demostrar que cumple con dicha declaración. Un solo supuesto erróneo puede debilitar el resultado, por lo que aún es necesario elegir qué demostrar y validar esa declaración.

El artículo deja claro que se trata de una división directa. Los humanos seleccionaron las propiedades, resolvieron las ambigüedades y aprobaron la especificación. Posteriormente, los agentes escribieron las demostraciones. Estas demostraciones solo se aceptan si Lean, un sistema de verificación de pruebas, las confirma. La fiabilidad del resultado, según los autores, no depende de la fiabilidad de los agentes que realizan las demostraciones, ya que el núcleo de Lean verifica la lógica.

Según la publicación de la investigación, los agentes de prueba funcionaron con Gemini Carbon. El trabajo de verificación en sí fue realizado por cinco investigadores durante cuatro semanas, cada uno ejecutando los agentes en su propia estación de trabajo. Se trata de una campaña breve para los estándares del sector. El artículo señala que el microkernel seL4, una verificación anterior muy conocida, requirió veinte años-persona, y que el compilador CompCert C requirió seis. Ambos códigos fuente se escribieron teniendo en cuenta la verificación. libsignal no.

¿Quieres que la IA te ahorre horas a la semana? Nuestra guía gratuita te muestra cómo.Obtén la guía gratuita →

Las pruebas en sí mismas pueden ser extensas porque tratan sobre código máquina. Aproximadamente 6,5 millones de líneas corresponden a las pruebas: 5,3 millones sobre el binario, además de archivos separados para los dos modelos de seguridad. Un lector que desee confiar en las afirmaciones principales aún debe leer las partes confiables: aproximadamente 18 000 líneas de especificación en el repositorio, más unas 8 000 líneas del modelo de código máquina Arm y los nombres de los símbolos asignados al ejecutable. Las rutinas criptográficas de bajo nivel, dos funciones de salida y algunas llamadas a bibliotecas se asumen por contrato, no se demuestran.

Una comprobación contra errores antiguos

Para comprobar si las afirmaciones eran lo suficientemente sólidas, el equipo reintrodujo dos errores que los investigadores habían encontrado previamente en libsignal y que ya se habían corregido. En ambos casos, demostraron que el teorema de seguridad simbólica no se cumple en el binario con el error. Esta es una comprobación útil: una especificación que aún se considere válida en código con errores conocidos sería demasiado débil.

Uno de esos errores almacenaba el estado de una nueva sesión, incluyendo una copia de un secreto, después de que un mensaje de preclave solo se hubiera descifrado en una sesión anterior. El otro aceptaba un protocolo de enlace cuya clave base había sido alterada, creando una segunda sesión con el mismo secreto compartido.

Lo que el resultado no dice

Los autores son meticulosos y las limitaciones son importantes. Las demostraciones no abarcan todas las partes de Signal, todos los posibles ataques ni las primitivas criptográficas en sí mismas. Los canales laterales quedan fuera del alcance. La demostración computacional, que intenta acotar la probabilidad de éxito de un atacante real, no ofrece ninguna garantía contra un adversario cuántico, y su límite se vuelve inútil para sesiones largas con muchas rondas.

El documento señala que se utilizan variantes del mismo protocolo en WhatsApp, Messenger de Meta y Google Messages. Sin embargo, estas aplicaciones no eran el objeto de la prueba. Una prueba sobre libsignal no se aplica automáticamente a todos los productos que utilizan un lenguaje similar.

Ehren Kret, director de tecnología de Signal, afirma en el artículo de investigación que verificar rigurosamente la implementación del protocolo “nos da aún mayor confianza en las garantías de privacidad de nuestro código”.

Las pruebas y especificaciones se publican en un repositorio abierto.

Por qué es importante

La mayoría de las personas que envían un mensaje privado nunca ven la biblioteca que lo cifra. Un método que permita verificar el código compilado de esa biblioteca en semanas, en lugar de años-persona, representa un cambio práctico en la forma en que se puede auditar este tipo de software. No es un certificado que garantice que Signal, o cualquier otra aplicación de chat, esté libre de fallos. Es un argumento verificado por máquina sobre propiedades específicas de una biblioteca central, generado con la suficiente rapidez como para que otros códigos críticos puedan ser los siguientes en ser analizados.

La mayoría de los productos de chat de uso diario aún no cuentan con dicha prueba, y algunas herramientas populares ni siquiera cifran los mensajes de extremo a extremo. Un informe anterior trataba sobre una herramienta de chat para consumidores que envía mensajes de texto sin esa protección.