Google verifica con IA protecciones clave del cifrado de Signal

Google DeepMind presentó AlphaProof Code, un sistema de inteligencia artificial que permitió comprobar matemáticamente propiedades esenciales de seguridad del código utilizado por el protocolo de cifrado Signal, una tecnología que ayuda a proteger conversaciones privadas en aplicaciones de mensajería.

La investigación, publicada el 10 de noviembre, representa un avance en la verificación de programas informáticos: en lugar de limitarse a buscar errores, los investigadores utilizaron herramientas matemáticas para demostrar que determinadas protecciones funcionan conforme a las condiciones establecidas.

El trabajo se realizó durante cuatro semanas y combinó la participación de especialistas humanos con agentes de inteligencia artificial capaces de generar y revisar pruebas matemáticas.

Aunque el resultado fortalece la confianza en componentes fundamentales del protocolo, no significa que toda la aplicación Signal esté libre de vulnerabilidades.

¿Qué comprobó la inteligencia artificial de Google?

AlphaProof Code analizó propiedades de seguridad de libsignal, la implementación de referencia del protocolo criptográfico utilizado por Signal.

Entre los aspectos estudiados se encuentran la confidencialidad de las conversaciones, la autenticidad de los mensajes y determinados mecanismos destinados a proteger la información incluso cuando un dispositivo o sus claves de seguridad se ven comprometidos temporalmente.

La característica más importante de la investigación es que las comprobaciones no se quedaron únicamente en el diseño teórico del sistema.

Los investigadores avanzaron hasta el código de máquina, es decir, las instrucciones que ejecuta directamente un procesador.

Esto permitió relacionar las garantías matemáticas del protocolo con una implementación concreta del software.

El protocolo Signal, o variantes de él, también se utiliza para proteger comunicaciones en servicios como WhatsApp y Google Messages.

Sin embargo, el estudio no constituye una certificación de seguridad de esas aplicaciones completas ni de todas sus funciones.

Seis millones y medio de líneas de pruebas matemáticas

Para realizar la investigación, DeepMind desarrolló un procedimiento en el que especialistas humanos establecieron qué propiedades de seguridad debían demostrarse.

Después, agentes de inteligencia artificial basados en Gemini Carbon elaboraron las pruebas utilizando Lean, un sistema informático que permite verificar razonamientos matemáticos.

El proyecto generó aproximadamente 6.5 millones de líneas de pruebas revisadas por computadora.

La diferencia es importante: la inteligencia artificial propuso las demostraciones, pero un sistema de verificación independiente comprobó que cumplieran las reglas matemáticas definidas.

Los especialistas humanos conservaron la responsabilidad de revisar y aprobar las condiciones sobre las cuales se construyeron las pruebas.

De acuerdo con Google, el procedimiento permitió completar en cuatro semanas una tarea que, mediante métodos tradicionales, podría requerir años de trabajo especializado.

La herramienta también reconoció errores antiguos

Los investigadores realizaron una prueba adicional para comprobar si AlphaProof Code podía distinguir entre una implementación segura y otra que contenía fallas.

Para ello, reintrodujeron dos errores reales que ya habían sido corregidos en versiones anteriores del código de Signal.

El sistema logró demostrar matemáticamente que esas versiones modificadas incumplían las propiedades de seguridad evaluadas.

Esta prueba ayudó a comprobar que el método no se limitaba a aprobar cualquier versión del programa.

Durante el análisis de los componentes examinados no se identificaron nuevas vulnerabilidades, según la investigación presentada por DeepMind.

No obstante, ese resultado no descarta la existencia de errores en otras partes de la aplicación.

Signal reconoce el avance, pero quedan límites

Ehren Kret, director de Tecnología de Signal, consideró que el trabajo representa un avance importante para ampliar la verificación formal del código criptográfico.

La verificación formal consiste en establecer mediante matemáticas que un programa cumple determinadas propiedades previamente definidas.

A diferencia de las pruebas convencionales, que examinan el funcionamiento del software en situaciones específicas, este método busca demostrar que ciertas garantías se mantienen bajo todas las condiciones contempladas por el modelo utilizado.

Sin embargo, una comprobación matemática solo cubre aquello que fue incluido en sus especificaciones y supuestos.

El estudio no abarcó toda la aplicación móvil Signal, todos los escenarios de funcionamiento ni todas las posibles amenazas.

Tampoco demostró de manera integral la seguridad frente a futuros ataques con computadoras cuánticas.

Por eso, sería incorrecto concluir que Signal se ha convertido en una plataforma imposible de vulnerar.

¿Podría utilizarse en bancos y servicios públicos?

La importancia de AlphaProof Code va más allá de las aplicaciones de mensajería.

Los bancos, hospitales, empresas y gobiernos utilizan sistemas informáticos que almacenan o procesan información sensible.

Errores en estos programas pueden comprometer datos personales, operaciones financieras y servicios esenciales.

Google considera que la verificación matemática asistida por inteligencia artificial podría facilitar la revisión de componentes críticos de ese tipo de plataformas.

Para México, la investigación resulta relevante por sus posibles aplicaciones futuras en sistemas bancarios, servicios digitales gubernamentales y herramientas de protección de información.

Sin embargo, DeepMind no anunció que AlphaProof Code ya se esté utilizando para certificar plataformas mexicanas.

La compañía tampoco confirmó un lanzamiento comercial de la herramienta ni detalló el costo total del trabajo realizado.

¿Por qué importa?

La inteligencia artificial suele utilizarse en ciberseguridad para detectar errores, identificar amenazas o ayudar a corregir vulnerabilidades.

Esta investigación muestra una posibilidad distinta: emplearla para construir pruebas matemáticas de que ciertas protecciones del software se cumplen realmente.

Si el método puede aplicarse a más sistemas, podría facilitar revisiones de seguridad que actualmente requieren grandes equipos de especialistas y periodos prolongados.

El avance también demuestra que la supervisión humana sigue siendo necesaria, especialmente al definir qué propiedades deben comprobarse y bajo qué condiciones.

¿Qué observar?

Uno de los principales puntos será conocer si otros equipos de investigadores pueden reproducir y ampliar los resultados publicados por Google DeepMind.

La compañía anunció que pondrá a disposición de la comunidad técnica los materiales de verificación para facilitar nuevas revisiones.

También será importante determinar si el procedimiento puede aplicarse a sistemas más grandes, con múltiples componentes y mayores niveles de complejidad.

Otro aspecto será comprobar si estas herramientas permiten reducir costos sin perder rigor técnico.

Por ahora, AlphaProof Code representa un avance en la seguridad informática: permitió demostrar matemáticamente determinadas protecciones del código criptográfico de Signal, pero todavía no ofrece una garantía absoluta sobre la seguridad de todas las aplicaciones que utilizan ese protocolo.