IA en un minutoNoticiasSeguridad
Google DeepMind usa IA para demostrar matemáticamente garantías clave del cifrado de Signal en una prueba de concepto
Redacción de IA en un minuto · Editor: Jon Elgezabal
En 30 segundos
AlphaProof Code reparte la tarea entre personas que eligen qué probar, agentes de IA que redactan las pruebas y Lean, que las revisa sin ayuda. DeepMind lo tuvo cuatro semanas trabajando sobre el núcleo criptográfico de Signal, el mismo que usa Google Messages. Signal había corregido hace tiempo dos fallos que el equipo volvió a meter en una copia, y el sistema demostró que esa versión no era segura.
Google DeepMind ha presentado AlphaProof Code, un sistema de varios agentes de IA para la verificación formal, es decir, para demostrar con matemáticas que un programa cumple lo que se espera de él. El trabajo se reparte así: expertos humanos deciden qué hay que demostrar, los agentes de IA elaboran las demostraciones y Lean, un programa de comprobación, las verifica automáticamente.
La compañía lo ha aplicado al código criptográfico central de Signal, la tecnología que protege miles de millones de conversaciones privadas en apps como Signal y Google Messages. El objetivo era demostrar propiedades de seguridad como que los mensajes sigan protegidos antes y después de que un dispositivo se vea comprometido temporalmente, y hacerlo sobre el código que se ejecuta en los dispositivos, no solo sobre el diseño del protocolo. Según DeepMind, los agentes, basados en Gemini Carbon, generaron más de seis millones de líneas de Lean y marcaron para una segunda revisión humana apenas el 1 % del código. El proceso llevó cuatro semanas.
Para comprobar el sistema, el equipo volvió a introducir dos fallos reales y ya corregidos en una versión aislada del código, y en ambos casos AlphaProof Code generó una prueba verificada por máquina de que esa versión era insegura. Según Infobae, que cita a Wired, los investigadores lo describen como una prueba de concepto: no encontraron vulnerabilidades nuevas y el análisis cubrió ciertas garantías del protocolo, no toda la aplicación móvil de Signal. Google tampoco ha dicho cuánto costó el trabajo ni si prepara un producto comercial.
DeepMind publicará en código abierto los artefactos de la verificación formal.
Por qué importa · análisis y opinión
La verificación formal llevaba años reservada a piezas pequeñas y a equipos muy especializados, porque escribir cada demostración a mano era lentísimo. Si unos agentes hacen la parte pesada y dejan a las personas solo las decisiones y la revisión de lo dudoso, el coste puede bajar lo bastante como para pensar en otros programas críticos. Lo que aún no se sabe es justo lo que decidirá si sale del laboratorio: cuánto cuesta, si funciona igual con código peor documentado que el de Signal y quién lo ofrecerá como servicio. Quien dependa de software sensible no tiene nada que contratar hoy, pero sí un buen motivo para preguntar a sus proveedores qué partes de su código están demostradas y cuáles solo probadas.
Fuente oficial: Google DeepMind · Redactada con ayuda de IA: cómo hacemos las noticias
