Google DeepMind dice que la IA verificó partes clave del protocolo Signal
🎧 Escucha esta noticia
Investigadores de Google DeepMind dicen que utilizaron agentes de IA y AlphaProof Code para verificar formalmente garantías criptográficas importantes de la implementación del protocolo Signal. El protocolo protege conversaciones en Signal y Google Messages y sustenta el cifrado de WhatsApp. Según Xataka, los agentes generaron más de seis millones de líneas en Lean, mientras expertos humanos revisaron las especificaciones y cerca del 1% del código marcado para un análisis adicional; el trabajo tomó cuatro semanas.
El análisis no encontró nuevas vulnerabilidades en las partes examinadas. Cuando el equipo reintrodujo dos fallas reales ya corregidas en una versión aislada del código, el sistema identificó que las versiones vulnerables no eran seguras, afirma Google DeepMind. El proyecto no verificó toda la aplicación móvil de Signal, y sigue abierta la cuestión de si el enfoque puede ampliarse a un costo viable. Signal Foundation ya había realizado trabajos previos de verificación en partes más pequeñas del código, según Wired y Xataka.
Por qué importa · interpretación editorial
El trabajo sugiere que los agentes de IA pueden ampliar la verificación formal de software criptográfico, pero la revisión humana siguió siendo necesaria y aún está abierta la cuestión de si el método puede escalar con un costo práctico. Como el análisis cubrió solo partes del código, no equivale a verificar por completo la aplicación Signal.
Fuentes
InvestigaciónSeguridadCódigo