AlphaProof Code de Google DeepMind verifica formalmente el protocolo criptográfico de Signal

Google DeepMind afirma haber alcanzado un hito en seguridad de software considerado durante mucho tiempo un gran desafío: sus investigadores guiaron a agentes de IA para demostrar matemáticamente propiedades de seguridad clave del código real que sustenta el protocolo de Signal, la tecnología que protege miles de millones de conversaciones privadas en aplicaciones como Signal y Google Messages al cifrar los mensajes de extremo a extremo, de modo que solo el remitente y el destinatario previsto puedan leerlos. El anuncio fue publicado en el blog de Google DeepMind por Pushmeet Kohli y Swarat Chaudhuri.

El resultado se logró con AlphaProof Code, un novedoso framework agéntico para la verificación formal a una profundidad sin precedentes que combina la experiencia humana con agentes de IA. La verificación formal —demostrar matemáticamente que el código funciona correctamente sin fallas— es el estándar más alto de garantía de seguridad, pero es difícil y a menudo requiere mucho trabajo. Las pruebas convencionales muestrean el comportamiento de un programa; una demostración formal descarta fallas en todas las ejecuciones posibles, un nivel de garantía tan costoso de producir que rara vez ha llegado al software ampliamente desplegado.

Según la empresa, este trabajo marca la primera vez que se utiliza la IA para verificar formalmente un protocolo criptográfico ampliamente desplegado a esta profundidad. También es la primera vez que la implementación de un protocolo de este tipo es verificada formalmente por cualquier método, con o sin IA.

Cómo Google DeepMind verificó Signal

AlphaProof Code es un framework agéntico multi-LLM que divide el trabajo de verificación formal como lo haría un equipo de investigación: los expertos humanos trabajan con la IA para decidir qué demostrar, y un grupo de agentes de IA ejecuta las demostraciones.

Primero, los investigadores de Google DeepMind colaboraron con una combinación de modelos para traducir los objetivos de seguridad de Signal a especificaciones matemáticas formales, con expertos humanos revisando cada una. Luego, agentes impulsados por Gemini Carbon realizaron las demostraciones, generando más de seis millones de líneas de Lean, un lenguaje informático que demuestra matemáticamente la exactitud del código.

A continuación, los agentes auditaron la demostración y señalaron las áreas que necesitaban una segunda revisión humana: apenas el uno por ciento del código base, lo que la empresa describe como un ahorro de tiempo enorme. Como Lean verifica automáticamente el resto, los expertos pudieron centrar su revisión donde el juicio humano importa más.

Demostrar la seguridad hasta el código en ejecución

Los protocolos criptográficos sustentan casi toda la comunicación digital, desde la banca en línea hasta la navegación web, y una sola falla puede exponer a millones de personas a la vez. Por eso los expertos llevan décadas analizándolos formalmente, aunque la mayoría de las verificaciones de protocolos se detiene a nivel de diseño.

Los agentes de Google DeepMind fueron más allá y demostraron que el código compilado cumple las propiedades de seguridad clave —como mantener los mensajes protegidos antes y después de que un dispositivo sea temporalmente comprometido, garantías que los criptógrafos conocen como secreto hacia adelante y seguridad posterior al compromiso— hasta el código exacto que se ejecuta en los dispositivos. Las vulnerabilidades del mundo real a menudo se esconden en la brecha entre el diseño y la implementación, y cerrar esa brecha hace que estas demostraciones sean muchísimo más complejas.

Incluso con este nivel de complejidad, el proceso de verificación tomó solo cuatro semanas, una tarea que históricamente toma años a los equipos de expertos, según la empresa, y estableció que el código criptográfico central de Signal ofrece las protecciones de seguridad especificadas por los investigadores.

Para confirmar que AlphaProof Code puede distinguir el código correcto del código con errores, el equipo reintrodujo dos errores reales, ya corregidos previamente, en una versión aislada del código de Signal. En ambos casos, el sistema produjo una demostración verificada por máquina de que la versión con errores era insegura, una comprobación importante, ya que un verificador incapaz de señalar código defectuoso ofrecería una falsa garantía.

En AlphaProof Code, los agentes de IA ayudan a los usuarios a escribir una especificación y luego demuestran de forma autónoma que la implementación la cumple. Cada demostración es verificada por Lean para validar el trabajo de los agentes.

La respuesta de Signal

"Mientras que la verificación formal previa se enfocaba en porciones más pequeñas del código, el enfoque de Google DeepMind permite una expansión significativa", dijo Ehren Kret, director de tecnología de Signal. "Usar agentes de IA para traducir código vivo en teoremas de 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 de Signal nos da aún más confianza en las garantías de privacidad de nuestro código".

El futuro de la seguridad

Google DeepMind sostiene que superar este desafío de larga data demuestra cómo la IA puede llevar una garantía de seguridad de élite a empresas, gobiernos e infraestructura crítica, ayudando a defenderse contra ciberamenazas impulsadas por agentes. Verificar la criptografía central de Signal, dice la empresa, sienta las bases para asegurar otros sistemas vitales, desde el firmware de dispositivos médicos hasta el software de redes eléctricas.

Escalar estas técnicas requiere investigación continua. Combinada con agentes de defensa automatizados como CodeMender, la verificación formal puede ayudar a contrarrestar la velocidad y la escala de las ciberamenazas modernas y crear software con prueba matemática de que sus protecciones funcionan.

Google DeepMind está publicando como código abierto sus artefactos de verificación formal para uso de la comunidad, disponibles en google-deepmind.github.io/code-verification. El artículo técnico completo está disponible como PDF. Para la comunidad de investigación en seguridad, esa publicación ofrece una forma de inspeccionar directamente las demostraciones verificadas por máquina y la metodología, y hasta dónde se extiende la verificación a esta profundidad más allá de Signal, hacia los sistemas médicos, industriales y de infraestructura que la empresa menciona, es el desarrollo a seguir de cerca.

Agradecimientos

La investigación fue desarrollada por Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton y Pushmeet Kohli.

El equipo agradeció a Eric Wieser su ayuda con la publicación del código como abierto, a Owen Jones su apoyo en gestión de programa, y a Martín Abadi, Christopher Henson, Katerina Hristova, Henryk Michalewski, Jonathan Protzenko y George Tsoukalas las discusiones valiosas. Los investigadores también agradecieron a Rolfe Schmidt, Michael Rosenberg y Ehren Kret de Signal sus comentarios sobre la metodología, así como a Tulsee Doshi, Four Flynn, Kate Olszewska, Alicia Huang, Andy Liu, Benoit Schillings, Raluca Ada Popa, Melvin Johnson, Koray Kavukcuoglu, Demis Hassabis y Sundar Pichai su apoyo al proyecto.