El cifrado de Signal supera una prueba de 6,5 millones de líneas hecha por IA

El código de cifrado de Signal cuenta ahora con algo que casi ningún programa de uso generalizado puede afirmar: una demostración matemática de que hace lo que promete. Un equipo de agentes de IA analizó libsignal, la biblioteca que implementa el protocolo de Signal, y demostró que sus conversaciones individuales siguen siendo secretas, confirman quién está al otro lado y vuelven a dejar fuera a un atacante después de que le roben una clave. No encontraron nuevas vulnerabilidades.

Esto importa mucho más allá de los propios usuarios de Signal. El protocolo es el estándar mundial para la mensajería cifrada de extremo a extremo, y algunas de sus variantes protegen las conversaciones de WhatsApp, Messenger y Google Messages. Revisar con este nivel de profundidad código real ya distribuido era hasta ahora tan lento que casi nadie lo intentaba: uno de los mayores logros del campo, la verificación de un núcleo de sistema operativo, llevó veinte años-persona. Este trabajo llevó cuatro semanas.

La herramienta, desarrollada por Google DeepMind, se llama AlphaProof Code. Primero, expertos humanos y modelos de IA tradujeron los objetivos de seguridad de Signal a enunciados formales en Lean, un lenguaje de programación creado para las demostraciones matemáticas, y una persona revisó cada uno. Después, equipos de entre 40 y 80 agentes, impulsados por Gemini Carbon, escribieron las demostraciones en sesiones de entre 24 y 72 horas en una sola máquina. El resultado suma unos 6,5 millones de líneas de Lean.

No hace falta confiar en esas millones de líneas. El núcleo de Lean comprueba cada paso y descarta cualquier demostración que no sea válida, así que da igual qué modelo la haya escrito o cuántas veces se haya equivocado por el camino. En lo que sí tienen que confiar las personas es en algo mucho más pequeño: unas 26.000 líneas de especificaciones y un modelo de cómo ejecuta el código un procesador ARM.

Las demostraciones cubren las partes de Signal que protegen una conversación: el protocolo de enlace PQXDH, que inicia un chat, y el Triple Ratchet, que cambia la clave con cada mensaje, incluida la capa poscuántica diseñada para resistir a los futuros ordenadores cuánticos. En la práctica, eso significa que robar las claves actuales de un teléfono no permite desbloquear mensajes antiguos, y que quien las robe vuelve a perder el acceso cuando ambas partes intercambian claves nuevas.

Para demostrar que el sistema distingue el código correcto del defectuoso, los investigadores reincorporaron dos errores antiguos de libsignal que ya se habían corregido. Uno hacía que la biblioteca conservara una copia de una clave secreta que debería haber descartado. En ambos casos, AlphaProof Code produjo una demostración verificada por máquina de que la versión con errores era insegura.

Las limitaciones son reales. La demostración solo cubre sesiones individuales, y DeepMind señala que la mensajería en grupo queda para trabajos futuros. Se aplica a la versión 0.105.4 de libsignal, compilada con el compilador estándar de Rust para ARM Linux dentro de un pequeño programa de prueba, no a las aplicaciones completas de Signal para iPhone, Android o escritorio. Se da por hecho que los componentes criptográficos básicos son seguros; no se demuestra. Un error en las especificaciones aprobadas por personas debilitaría la garantía, y WhatsApp y las demás aplicaciones utilizan sus propias versiones del protocolo, por lo que el resultado no se les aplica automáticamente. Google también se negó a decirle a Wired cuánto costó el análisis o si tiene previsto ofrecerlo como servicio.

Signal recibió con satisfacción el resultado. «A medida que crecen las amenazas a la seguridad impulsadas por la IA, verificar rigurosamente la implementación del protocolo de Signal nos da aún más confianza en las garantías de privacidad de nuestro código», declaró Ehren Kret, director de tecnología de Signal. Swarat Chaudhuri, investigador científico de DeepMind, se mostró más cauto y dijo a Wired que todavía queda «mucho camino por recorrer» antes de que el método pueda ampliarse «a todo el software del mundo».

Quienes usan Signal no tienen que instalar nada ni cambiar ningún ajuste. La demostración se refiere a código que ya está en la aplicación.

DeepMind publicó el trabajo el 10 de noviembre, junto con un artículo técnico, y ha puesto a disposición del público las especificaciones y las demostraciones como código abierto en GitHub. Presenta el proyecto de Signal como un hito hacia un gran desafío de verificación formal planteado en abril, y cita el firmware de dispositivos médicos y el software de las redes eléctricas como ejemplos de los sistemas que quiere comprobar a continuación.

Chaudhuri también trazó una línea sobre cuánto trabajo deberían asumir las máquinas. «No queremos un mundo de ese estilo en el que la IA genere los objetivos y la IA genere las demostraciones», dijo a Wired. Las personas siguen decidiendo qué se considera seguro; la IA solo lo demuestra.

Etiquetas: ciberseguridad, Google DeepMind, AlphaProof Code, cifrado de extremo a extremo, libsignal, Signal