El código de Signal, verificado por la IA de DeepMind en un mes

¿Qué es la verificación formal?

Consiste en usar matemáticas, en lugar de pruebas, para demostrar que un programa se comporta como se pretende. Se considera la garantía de seguridad más sólida, pero ha sido lenta y laboriosa. La mayoría de las verificaciones de protocolos criptográficos se quedan en la fase de diseño. DeepMind afirma que ha comprobado la implementación real, donde a menudo se esconden los errores del mundo real. Dice que es la primera vez que se verifica formalmente la implementación de un protocolo tan extendido, con o sin IA.

¿Cómo funciona AlphaProof Code?

Es un marco que combina varios modelos de IA con expertos humanos. Investigadores y modelos tradujeron los objetivos de seguridad de Signal en especificaciones formales, y personas revisaron cada una. Los agentes, impulsados por Gemini Carbon, escribieron las pruebas: más de seis millones de líneas de Lean, un lenguaje que permite a un ordenador comprobarlas automáticamente. Después auditaron su propio trabajo y señalaron cerca del 1 % del código para una segunda revisión humana.

Las pruebas cubren propiedades como mantener los mensajes protegidos antes y después de que un dispositivo quede comprometido temporalmente.

¿Encontró errores?

No halló nuevas vulnerabilidades en las partes analizadas. Para ver si el sistema distingue el código bueno del malo, el equipo reintrodujo dos errores reales ya corregidos en una versión aislada. En ambos casos, dice DeepMind, el sistema generó una prueba verificada por máquina de que esa versión no era segura.

Hay límites. No se verificó toda la app móvil de Signal, y DeepMind partía de un trabajo previo de la Signal Foundation. Ehren Kret, director de tecnología de Signal, dijo que ese trabajo se centró en porciones más pequeñas, mientras que el enfoque de DeepMind permite una expansión significativa.

El investigador Swarat Chaudhuri no quiere que la IA escriba tanto los objetivos como las pruebas, o sea, que se ponga nota a sí misma. Por eso los humanos revisaron las especificaciones y las secciones marcadas.

Queda sin aclarar si esto escala y a qué coste. DeepMind hizo el análisis gratis, como proyecto de investigación, y no ha dicho cuánto costó ni si habrá un producto comercial. Abre el código de sus artefactos de verificación y sugiere que el método podría llegar al firmware de dispositivos médicos o al software de la red eléctrica.