De años a cuatro semanas: la IA de DeepMind verifica por primera vez el código real del protocolo Signal

Google DeepMind ha conseguido algo que la industria llevaba años persiguiendo: demostrar matemáticamente que el código real del protocolo Signal cumple sus propiedades de seguridad clave, no sobre el papel del diseño, sino hasta el código compilado que se ejecuta en los dispositivos. El protocolo Signal protege las conversaciones privadas de miles de millones de personas en aplicaciones como Signal y Google Messages, y es la primera vez que se verifica formalmente la implementación de un protocolo criptográfico tan desplegado, con cualquier método. La hazaña la han logrado agentes de inteligencia artificial en cuatro semanas, un trabajo que según la compañía ha llevado históricamente años a equipos de expertos.

El sistema se llama AlphaProof Code y funciona como lo haría un equipo de investigación. Primero, los investigadores de DeepMind tradujeron los objetivos de seguridad de Signal a especificaciones matemáticas formales, trabajando con varios modelos y revisando los humanos cada especificación una a una. A partir de ahí, agentes impulsados por Gemini Carbon generaron más de seis millones de líneas en Lean, un lenguaje que permite comprobar mecánicamente que una demostración es correcta. Los propios agentes auditaron después la prueba y marcaron las zonas que necesitaban una segunda mirada humana: apenas el uno por ciento del código. El resto lo valida Lean de forma automática, así que los expertos pudieron concentrarse donde el juicio humano importa.

La diferencia entre el diseño y el código que corre en tu móvil

La mayoría de las verificaciones formales de protocolos se quedan en el nivel del diseño. Los investigadores de DeepMind fueron más allá y demostraron que el código compilado cumple propiedades como mantener los mensajes protegidos antes y después de que un dispositivo se vea comprometido temporalmente. Es un matiz decisivo: las vulnerabilidades reales suelen esconderse en la distancia entre lo que el protocolo promete en su diseño y lo que la implementación hace de verdad, y cerrar esa brecha es lo que hace estas pruebas mucho más complejas.

Para comprobar que el sistema distingue código correcto de código con fallos, el equipo reintrodujo dos errores reales ya corregidos en una versión aislada del código de Signal. En ambos casos, AlphaProof Code produjo una prueba verificada por máquina de que la versión con el fallo era insegura. Es la prueba de fuego de cualquier herramienta de este tipo: no basta con que apruebe lo correcto, tiene que suspender lo que no lo es.

Desde Signal han recibido el trabajo con entusiasmo contenido. «Aunque los trabajos previos de verificación formal se centraban en porciones más pequeñas del código, el enfoque de Google DeepMind permite una expansión significativa», ha declarado Ehren Kret, su director de tecnología. «Usar agentes de IA para traducir código en producción a teoremas Lean válidos es un gran avance. A medida que crecen las amenazas de seguridad impulsadas por IA, verificar rigurosamente la implementación del protocolo Signal nos da aún más confianza en las garantías de privacidad de nuestro código».

Conviene ser precisos con lo que se ha demostrado. La verificación certifica que el código cumple las propiedades de seguridad que los expertos especificaron, y la especificación la escriben humanos: lo que queda fuera de ella queda fuera de la prueba. Dicho esto, el precedente es potente. La verificación formal ha sido durante décadas el estándar más exigente de garantía de seguridad y, a la vez, un lujo reservado a proyectos con años de plazo. Si los agentes de IA lo convierten en un proceso de semanas, auditar software crítico deja de ser una excepción. DeepMind ya apunta al siguiente paso: abrir los artefactos de verificación a la comunidad y combinar estas técnicas con agentes de defensa automatizados como CodeMender, en un momento en el que los agentes de IA ofensivos ya han empezado a actuar contra servicios gubernamentales.

Para los cientos de millones de personas que usan a diario aplicaciones protegidas por este protocolo, también en España, la noticia no exige hacer nada: exige saber que el cifrado en el que confían ha pasado, por primera vez, el examen más duro que existe. La pregunta de siempre, si Signal es seguro, tiene desde hoy una respuesta con demostración matemática incluida. Queda por ver cuánto tardan otros protocolos y otros fabricantes en someterse al mismo examen, y si la verificación con IA se convierte en un requisito y no en una primicia.

Más información | el anuncio de Google DeepMind sobre AlphaProof Code