DeepMind afirma que su IA verificó en un mes el código de Signal

Google DeepMind afirmó que sus agentes de inteligencia artificial demostraron matemáticamente que partes clave del código que está detrás del protocolo de cifrado de Signal hacen lo que se supone que deben hacer. El protocolo protege las conversaciones privadas en Signal y Google Messages, y también sustenta el cifrado de WhatsApp, según comparten desde Wired.

La compañía describe el resultado como un hito en la seguridad del software, aunque los propios investigadores recalcan que se trata de un paso dentro de un proceso más largo. La verificación formal consiste en usar matemáticas, en lugar de pruebas convencionales, para demostrar que el software se comporta como se pretende. Se considera la garantía de seguridad más sólida disponible, pero tradicionalmente ha sido lenta y laboriosa.

Qué significa verificar formalmente un protocolo

La mayor parte de la verificación de protocolos criptográficos se detiene en la fase de diseño. DeepMind afirma que su sistema fue más allá y comprobó la implementación real, que es precisamente donde suelen esconderse los errores del mundo real.

Según la compañía, es la primera vez que la implementación de un protocolo ampliamente desplegado como este ha sido verificada formalmente por cualquier método, con o sin IA. El sistema se llama AlphaProof Code, un marco que combina varios modelos de IA con expertos humanos.

Investigadores de DeepMind y varios modelos de IA tradujeron los objetivos de seguridad de Signal en especificaciones formales, y expertos humanos revisaron cada una de ellas. Los agentes, impulsados por Gemini Carbon, escribieron las pruebas y generaron más de seis millones de líneas de Lean, un lenguaje que permite a un ordenador comprobar las pruebas automáticamente.

El papel humano y la revisión del propio trabajo

Tras la generación de pruebas, los agentes auditaron su propio trabajo y señalaron aproximadamente el 1% de la base de código que necesitaba una segunda revisión por parte de un humano. DeepMind dice que el trabajo llevó cuatro semanas, una tarea que históricamente lleva años a equipos de expertos.

Las pruebas cubren propiedades como mantener los mensajes protegidos antes y después de que un dispositivo se vea comprometido temporalmente. Para comprobar si el sistema puede distinguir el buen código del malo, el equipo reintrodujo dos errores reales previamente corregidos en una versión aislada del código de Signal. En ambos casos, dice DeepMind, el sistema produjo una prueba verificada por máquina de que la versión con errores no era segura.

El análisis no encontró nuevas vulnerabilidades en las partes de Signal, según Wired. Sin embargo, el proyecto no verificó toda la aplicación móvil de Signal, y Wired señala que DeepMind tenía ventaja gracias a un trabajo previo de verificación formal por parte de la Signal Foundation.

"Se centró en porciones más pequeñas del código", dijo Ehren Kret, director de tecnología de Signal, en un comunicado, mientras que el enfoque de DeepMind "permite una expansión significativa".

Kret añadió que, a medida que crecen las amenazas a la seguridad impulsadas por la IA, la verificación le da a Signal "aún mayor confianza" en sus garantías de privacidad.

Las preguntas abiertas sobre el método

Los investigadores también dicen que quieren evitar una configuración en la que la IA escriba tanto los objetivos como las pruebas. "No queremos este tipo de mundo de sensaciones en el que la IA genera los objetivos y la IA genera las pruebas y básicamente toma exámenes que están autoescritos", declaró a Wired Swarat Chaudhuri, científico investigador de DeepMind. "Hay un término medio", agregó. Por ello, la parte humana se encargó de revisar las especificaciones y las secciones marcadas.

Si esto puede escalar y a qué coste no está claro. Según Wired, DeepMind ejecutó el análisis de Signal de forma gratuita como un proyecto de investigación, pero no han compartido qué coste tuvo la operación ni si planean un producto de verificación comercial.

"Hay un largo trecho por recorrer antes de que podamos escalar esto a todo el software del mundo, y queremos hacerlo", contó Chaudhuri a Wired.

DeepMind dice que está abriendo el código fuente de sus artefactos de verificación formal para la comunidad, y sugiere que el enfoque podría extenderse eventualmente a sistemas como el firmware de dispositivos médicos y el software de la red eléctrica.