La IA de Google DeepMind demuestra las garantías de cifrado de Signal

Investigadores de Google DeepMind, de Alphabet Inc. ↘ 0.21%, utilizaron un nuevo marco de IA llamado AlphaProof Code para demostrar matemáticamente varias de las principales garantías criptográficas del protocolo Signal. El proyecto de prueba de concepto de cuatro semanas no encontró nuevas vulnerabilidades en las partes del protocolo examinadas, informó WIRED el 10 de noviembrewired.com. El resultado es importante más allá de la aplicación Signal. El protocolo también protege los mensajes en Google Messages y WhatsApp de Meta Platforms, Inc. ↗ 0.22%, por lo que el análisis añade otra verificación independiente al cifrado que protege una gran parte de las comunicaciones mundiales, según WIRED. También demuestra que los agentes de IA pueden acelerar la verificación formal, una forma largamente buscada pero lenta de usar las matemáticas para demostrar que el software se comporta como se pretendewired.com. ## Lo que encontró el análisis Los investigadores probaron AlphaProof Code en versiones antiguas de Signal que contenían vulnerabilidades conocidas, todas corregidas hace mucho tiempo. La herramienta encontró correctamente esos fallos y demostró que esas versiones no podían ser verificadas formalmente, informó WIRED. DeepMind publicará la especificación y la prueba que creó para que otros esfuerzos de verificación puedan utilizarlaswired.com. El alcance fue limitado. El trabajo no verificó la aplicación móvil completa de Signal, y los investigadores lo describieron como un hito en un proceso más largo. "Estamos muy entusiasmados con este resultado, pero queda un largo camino por recorrer antes de que podamos escalar esto a todo el software del mundo, y queremos hacerlo", dijo a WIRED el científico investigador de DeepMind, Swarat Chaudhuriwired.com. El equipo señaló que el trabajo previo de verificación formal realizado por Signal les dio una ventaja. "Aunque la verificación formal anterior se centró en porciones más pequeñas del código, el enfoque de Google DeepMind permite una expansión significativa", dijo el director de tecnología de Signal, Ehren Kret, en un comunicado, añadiendo que la verificación le da a la empresa "una confianza aún mayor" a medida que crecen las amenazas de seguridad impulsadas por la IAwired.com. ## Un campo concurrido El trabajo de DeepMind llega mientras otros grupos persiguen objetivos similares. En abril de 2026, Signal, la Beneficial AI Foundation y Lean FRO lanzaron Signal Shot, un esfuerzo público para verificar el protocolo Signal y su implementación en Rust utilizando el asistente de pruebas Lean. El proyecto tiene como objetivo traducir el código real de Signal a Lean y demostrar que coincide con un modelo verificado del protocolo, según la fundación. El resultado de DeepMind es independiente de ese proyecto, señaló Startup Fortunebeneficialaifoundation.org+2. ## Preguntas abiertas sobre el costo Aún no está claro si la verificación automatizada por IA puede escalar a un costo viable. DeepMind realizó el análisis de Signal de forma gratuita como un proyecto de investigación. Google se negó a decir cuánto costó o si planea un producto de verificación comercial, informó WIREDwired.com. Chaudhuri dijo que un avance clave fue un proceso en el que los agentes de IA contribuyen y corrigen su propio trabajo mientras los humanos lo revisan en puntos clave. "No queremos este tipo de mundo donde la IA genera los objetivos y la IA genera las pruebas y básicamente toma exámenes que están autoescritos", dijo. "Hay un punto medio"wired.com.