Google DeepMind ha anunciado que sus agentes de inteligencia artificial han comprobado matemáticamente la efectividad de partes críticas del código del protocolo de cifrado utilizado en aplicaciones como Signal, Google Messages y WhatsApp. Este avance promete reforzar la seguridad de las comunicaciones privadas, un aspecto cada vez más relevante en la era digital. La compañía considera que esta verificación formal de un protocolo tan adoptado representa un avance significativo, aunque aclara que se trata de un paso dentro de un proceso más amplio de mejora de seguridad.
La verificación formal implica el uso de matemáticas para demostrar que el software funciona según lo previsto, ofreciendo un nivel de seguridad superior al de las pruebas convencionales. Este tipo de validación ha sido históricamente un proceso laborioso y costoso, que generalmente se detenía en la fase de diseño. Sin embargo, DeepMind sostiene que su nuevo sistema, AlphaProof Code, ha llegado más allá al auditar la implementación real, donde frecuentemente surgen errores en el código.
AlphaProof Code combina modelos de inteligencia artificial y la revisión de expertos humanos para establecer especificaciones formales de seguridad. Durante el proceso, los agentes de inteligencia artificial, como Gemini, generaron más de seis millones de líneas de código en Lean, un lenguaje que permite la verificación automática de pruebas. Este análisis, que normalmente tomaría años, se completó en cuatro semanas, detectando un 1% del código que necesitaba revisión humana.
Cabe destacar que no se encontraron nuevas vulnerabilidades en el análisis de Signal. Se realizaron pruebas al reintroducir errores previamente corregidos en una versión aislada del código, y en ambos casos, el sistema demostró que dichas versiones no eran seguras. Aunque el estudio no abarcó la totalidad de la aplicación Signal, expertos enfatizan que el trabajo previo de la Signal Foundation facilitó el éxito del análisis.
DeepMind ha declarado que está comprometida a evitar que la inteligencia artificial asuma tanto la formulación de objetivos como la creación de pruebas. La participación humana en la revisión de especificaciones es fundamental para mantener un equilibrio en el proceso. No se ha especificado el costo del análisis ni si se desarrollará un producto comercial basado en esta tecnología.
A futuro, DeepMind planea abrir el código fuente de sus artefactos de verificación formal, lo que podría permitir su aplicación en otras áreas, como firmware de dispositivos médicos o software crítico para infraestructura energética. Este enfoque abre nuevas oportunidades para mejorar la seguridad del software en un entorno cada vez más amenazante y conectado.