Investigadores de Google DeepMind lograron demostrar formalmente que el protocolo de cifrado de Signal —el mismo que protege los mensajes de millones de personas en Signal, Google Messages y WhatsApp— funciona exactamente como fue diseñado. El logro, alcanzado con ayuda de inteligencia artificial, marca un hito en la verificación de software.
El equipo, formado por criptógrafos humanos acompañados por agentes de IA, completó la prueba de concepto en apenas cuatro semanas, un proceso que tradicionalmente tomaba años de trabajo manual. Para lograrlo crearon AlphaProof Code, una herramienta que construyó el modelo de seguridad directamente a partir de la descripción escrita del protocolo y lo perfeccionó con la ayuda de los investigadores.
«Lo que demostramos aquí es que la IA puede hacer el trabajo difícil de las pruebas formales», señaló Swarat Chaudhuri, científico investigador de DeepMind. Las pruebas formales son demostraciones matemáticas de que un sistema hace exactamente lo que se supone que debe hacer, y en el caso de Signal, la herramienta demostró las propiedades de seguridad que se creían ciertas, pero sin un sistema de verificación que las avalara.
Lo más relevante es que el trabajo no encontró vulnerabilidades nuevas en las partes del protocolo examinadas. Y para comprobar que el método funciona, los investigadores también pusieron a prueba su herramienta con versiones antiguas del protocolo con fallos conocidos y ya corregidos: AlphaProof Code los identificó correctamente, lo que da confianza en el resultado.
Ehren Kret, director de tecnología de Signal, señaló que la compañía se siente alentada de que, gracias a la investigación de DeepMind, «ahora podemos decir con certeza que las garantías de seguridad de Signal son sólidas». Por su parte, Pushmeet Kohli, científico en jefe de Google Cloud y vicepresidente de investigación de DeepMind, destacó que las propiedades que se demostraron eran las más críticas del protocolo y que el equipo pudo probar «lo que realmente se propuso probar».
DeepMind publicó tanto la especificación como la prueba del protocolo para que otros investigadores y la comunidad puedan apoyarse en este trabajo. La empresa, sin embargo, declinó compartir el costo del proceso y no comentó sobre planes para convertirlo en un producto comercial.
El objetivo a largo plazo es mucho más ambicioso: según Chaudhuri, la meta es que algún día cada programa del mundo cuente con una prueba de sus afirmaciones de seguridad. De momento, este trabajo confirma con una demostración matemática que el cifrado en el que confían millones de personas todos los días hace exactamente lo que promete.
Para más noticias de tecnología, cultura geek, gadgets y entretenimiento, visita: GeekAndLife.com.mx. Descubre más contenido en nuestras redes: Instagram | YouTube | TikTok
Fuente: WIRED