DeepMind verifica formalmente el protocolo Signal con una IA

Investigadores de Google DeepMind usaron un marco de IA agéntica llamado AlphaProof Code para demostrar matemáticamente varias garantías criptográficas clave del protocolo Signal, según Wired. El trabajo, una prueba de concepto realizada en cuatro semanas, es un ejercicio de verificación formal: un método que usa las matemáticas para comprobar que un software hace lo que debe, en lugar de probar una muestra de casos.

El protocolo Signal es el esquema de cifrado de la aplicación Signal y, como señala Wired, también protege las comunicaciones de Google Messages y WhatsApp. El análisis se presenta, por tanto, como una validación independiente adicional de una criptografía que protege un volumen enorme de mensajes. Wired lo describe como un hito para la criptografía y para la propia IA, aunque subraya que su alcance es limitado.

¿Qué demostró exactamente DeepMind?

El equipo demostró “varias” de las garantías clave del protocolo, no todas. Wired aclara que el análisis no verificó formalmente toda la aplicación móvil de Signal, y los investigadores presentan su resultado como un hito dentro de un proceso más amplio. “Estamos muy entusiasmados con este resultado, pero queda un largo camino antes de poder escalarlo a todo el software del mundo, y queremos hacerlo”, dijo a Wired Swarat Chaudhuri, científico investigador de DeepMind.

Según el mismo artículo, el análisis no encontró ninguna vulnerabilidad nueva en las partes del protocolo examinadas. Los investigadores también aplicaron AlphaProof Code a versiones antiguas de Signal con vulnerabilidades conocidas y corregidas hace tiempo: la herramienta las identificó correctamente y demostró que esas versiones no podían verificarse formalmente. Esa prueba importa porque muestra que el método puede fallar cuando existe un defecto, y no solo tener éxito cuando no lo hay.

• Herramienta: AlphaProof Code, un nuevo marco de IA agéntica de Google DeepMind.
• Duración: cuatro semanas, como proyecto de prueba de concepto.
• Resultado: garantías criptográficas clave demostradas; ninguna vulnerabilidad nueva en las partes analizadas.
• Versiones antiguas: fallos conocidos y corregidos detectados, y protocolo declarado no verificable.
• Publicación: se difunden la especificación y la prueba para ayudar a otros trabajos de verificación formal.
• Coste: no divulgado; el análisis se hizo gratis, como proyecto de investigación.

¿Cómo se repartieron el trabajo la IA y las personas?

Antes de la era de la IA, había que describir las propiedades que se querían demostrar, convertirlas en fórmulas y luego desarrollar la prueba. Wired explica que la IA agéntica puede reducir mucho el tiempo de este último paso, lo que hizo posible la evaluación de Signal en cuatro semanas. Los investigadores de DeepMind añaden que partieron con ventaja, porque la Signal Foundation ya había hecho trabajo de verificación formal sobre partes más pequeñas del código.

Ehren Kret, director de tecnología de Signal, dijo en un comunicado citado por Wired: “Mientras que la verificación formal previa se centraba en partes más pequeñas del código, el enfoque de Google DeepMind permite una ampliación significativa”. Añadió que verificar rigurosamente la implementación aumenta la confianza de Signal en las garantías de privacidad de su código, a medida que crecen las amenazas de seguridad impulsadas por la IA.

DeepMind sitúa su principal avance en un “proceso de colaboración humano-IA”: los agentes contribuyen y se autocorrigen en casi todas las fases, mientras que las personas revisan en los momentos clave. “No queremos un mundo en el que la IA genere los objetivos y genere las pruebas”, dijo Chaudhuri. Una prueba formal solo garantiza las propiedades que se escribieron, por eso la revisión humana de la especificación sigue siendo central.

Un esfuerzo paralelo en torno a Signal

El trabajo de DeepMind no es el único intento de demostrar la criptografía de Signal. La Beneficial AI Foundation, con Rolfe Schmidt de Signal y el Lean FRO, lanzó “Signal Shot”, un proyecto público para verificar el protocolo y su implementación en Rust con el asistente de pruebas Lean. Prevé traducir el código Rust de Signal a Lean con la herramienta Aeneas, y enumera componentes por verificar, como el intercambio de claves poscuántico PQXDH, el Double Ratchet y el SPQR/Triple Ratchet. Wired no vincula esta iniciativa con la de DeepMind: son dos esfuerzos distintos.

¿Qué sigue siendo incierto?

La pregunta abierta, señala Wired, es si la verificación formal automatizada con IA puede escalar a un coste viable. Google se negó a revelar el coste del análisis de Signal y a decir si planea un producto o servicio comercial de verificación formal. Pushmeet Kohli, científico jefe de Google Cloud y vicepresidente de investigación de DeepMind, imagina que bancos y otras empresas preocupadas por los errores podrían afirmar que pueden demostrar ciertas propiedades de su software. Es una visión, no una oferta anunciada.

Qué cambia para las empresas

Para una empresa que elige una herramienta de mensajería o construye sobre el protocolo Signal, el resultado es una señal tranquilizadora sobre el diseño del protocolo, no un certificado para cada aplicación que lo usa: la aplicación Signal completa no se verificó, y el despliegue, los servidores y la configuración de un producto quedan fuera de la prueba. La especificación y la prueba publicadas dan a los equipos de seguridad material para estudiar y reutilizar. Como el coste y cualquier oferta comercial son desconocidos, aún no conviene contar con este enfoque para verificar formalmente el código propio, pero ya se puede preguntar a los proveedores de software crítico qué propiedades están especificadas y demostradas.