Google DeepMind ha anunciado que sus agentes de inteligencia artificial han logrado verificar matemáticamente partes cruciales del protocolo de cifrado de Signal, que protege comunicaciones en Signal, Google Messages y WhatsApp. Este logro, descrito como un hito en la seguridad del software, implica el uso de matemáticas para demostrar el comportamiento intencionado del código, un proceso tradicionalmente largo y complejo. La compañía destaca que es la primera vez que la implementación real de un protocolo tan extendido es verificada formalmente con o sin IA, abriendo nuevas posibilidades para la seguridad digital.
Google DeepMind ha anunciado que sus agentes de inteligencia artificial han demostrado matemáticamente que componentes clave del código que sustenta el protocolo de cifrado de Signal funcionan como se espera. Este protocolo es fundamental para la seguridad de las conversaciones privadas en Signal y Google Messages, y también es la base del cifrado de WhatsApp.
La empresa describe este logro como un hito significativo en la seguridad del software, aunque los propios investigadores enfatizan que es un paso inicial en un proceso de mayor alcance. La verificación formal, en este contexto, implica el uso de métodos matemáticos, en lugar de pruebas tradicionales, para confirmar que el software se comporta según lo previsto. Este enfoque se considera la garantía de seguridad más robusta disponible, pero históricamente ha sido un proceso lento y laborioso. Generalmente, 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á, verificando la implementación real del código, que es precisamente donde suelen residir los errores en el mundo real. La compañía sostiene que es la primera vez que la implementación de un protocolo tan ampliamente utilizado ha sido verificada formalmente mediante cualquier método, sea con o sin inteligencia artificial.
El sistema empleado se denomina AlphaProof Code, un marco que integra diversos modelos de IA con la intervención de expertos humanos. Para llevar a cabo esta tarea, investigadores de DeepMind y varios modelos de IA tradujeron los objetivos de seguridad de Signal en especificaciones formales, que luego fueron revisadas por expertos humanos. Los agentes de IA, impulsados por Gemini Carbon, se encargaron de escribir las pruebas, generando más de seis millones de líneas en Lean, un lenguaje que permite a una computadora verificar automáticamente las pruebas.
Posteriormente, los agentes de IA auditaron su propio trabajo e identificaron aproximadamente el 1% de la base de código que requería una segunda revisión por parte de un humano. DeepMind indica que este trabajo se completó en cuatro semanas, una tarea que, históricamente, llevaría años a equipos de expertos. Las pruebas realizadas cubren propiedades esenciales, como la protección de los mensajes antes y después de que un dispositivo haya sido comprometido temporalmente.
El análisis no reveló nuevas vulnerabilidades en las partes de Signal examinadas. Para evaluar la capacidad del sistema para diferenciar entre código correcto e incorrecto, el equipo reintrodujo dos errores reales previamente corregidos en una versión aislada del código de Signal. En ambos casos, según DeepMind, el sistema produjo una prueba verificada por máquina que confirmaba la inseguridad de la versión con errores.
Es importante señalar que el proyecto no verificó la totalidad de la aplicación móvil de Signal. Se destaca que DeepMind contó con una ventaja gracias a un trabajo previo de verificación formal realizado por la Signal Foundation. Ehren Kret, director de tecnología de Signal, comentó 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ñadió que, a medida que aumentan las amenazas a la seguridad impulsadas por la IA, esta verificación otorga a Signal “aún mayor confianza” en sus garantías de privacidad.
Los investigadores también expresan su deseo de evitar una situación en la que la IA sea responsable tanto de definir los objetivos como de escribir las pruebas. Swarat Chaudhuri, científico investigador de DeepMind, declaró: “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. Hay un término medio”. Por esta razón, la revisión de las especificaciones y de las secciones marcadas ha sido responsabilidad humana.
Aún quedan preguntas sobre la escalabilidad de este método y los costos asociados. DeepMind realizó el análisis de Signal de forma gratuita como parte de un proyecto de investigación, pero no ha revelado el costo de la operación ni si planean desarrollar un producto de verificación comercial. Chaudhuri comentó: “Hay un largo trecho por recorrer antes de que podamos escalar esto a todo el software del mundo, y queremos hacerlo”. DeepMind ha anunciado que pondrá a disposición de la comunidad el código fuente de sus artefactos de verificación formal y sugiere que este enfoque podría aplicarse eventualmente a sistemas críticos como el firmware de dispositivos médicos y el software de la red eléctrica.
