Verificar el código de Signal era un reto que llevaba años de trabajo de expertos. DeepMind dice que su IA lo ha hecho en un mes

Google DeepMind dice que sus agentes de IA han demostrado 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, tal y como comparten en Wired. La compañía lo describe como un hito en la seguridad del software, aunque los propios investigadores recalcan que es un paso en un proceso más largo.

Comprobado, el protocolo funciona. La verificación formal significa usar matemáticas, en lugar de pruebas, 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. La mayor parte de la verificación de protocolos criptográficos se detiene en la fase de diseño. DeepMind afirma que su sistema ha ido más allá, comprobando la implementación real, que es precisamente donde a menudo se esconden los errores del mundo real.

La compañía dice que 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.

Esquema de cómo se ha realizado la verificación formal del código de Signal. Imagen: Google

Cómo funciona. El sistema se llama AlphaProof Code, un marco que combina varios modelos de IA con expertos humanos. Para ello, 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, generando más de seis millones de líneas de Lean, un lenguaje que permite a un ordenador comprobar las pruebas automáticamente.

Tras ello, 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 tales como mantener los mensajes protegidos antes y después de que un dispositivo se vea comprometido temporalmente.

¿Detecta realmente errores? El análisis no encontró nuevas vulnerabilidades en las partes de Signal, según comparten desde Wired. 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.

Entre líneas. 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. Ehren Kret, director de tecnología de Signal, dijo en un comunicado que el trabajo anterior "se centró en porciones más pequeñas del código", mientras que el enfoque de DeepMind "permite una expansión significativa". Añade además 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.

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", declaraba a Wired Swarat Chaudhuri, científico investigador de DeepMind. "Hay un término medio". Por ello mismo la parte humana se ha encargado de revisar las especificaciones y las secciones marcadas.

Las preguntas abiertas. 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", contaba 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.

Imagen de portada | Adem AY

En Xataka | Anthropic ha descubierto lo que mi madre ya sabía: la IA cuida mejor las cosas cuando cree que son suyas