DeepMind verifica en un mes código de Signal, tarea que llevaba años a expertos
Google DeepMind ha aconseguit una fita en la seguretat del programari en verificar matemàticament parts clau del codi darrere del protocol de xifratge de Signal en tan sols un mes, una tasca que tradicionalment portava anys a equips d'experts. Aquest protocol és fonamental per protegir les converses privades en aplicacions com Signal, Google Messages i WhatsApp. Segons Wired, la companyia descriu aquest assoliment com un avenç significatiu, encara que els investigadors adverteixen que és només un pas en un procés més extens.
La verificació formal, que utilitza matemàtiques en lloc de proves, es considera la garantia de seguretat més sòlida disponible. No obstant això, ha estat històricament lenta i laboriosa, aturant-se sovint en la fase de disseny. DeepMind ha anat més enllà en verificar la implementació real, on solen amagar-se els errors del món real. Aquest assoliment marca la primera vegada que un protocol àmpliament desplegat ha estat verificat formalment per qualsevol mètode, amb o sense IA.
El sistema utilitzat, anomenat AlphaProof Code, combina models d'IA amb experts humans. Els investigadors van traduir els objectius de seguretat de Signal en especificacions formals, que van ser revisades per experts humans. Els agents d'IA, impulsats per Gemini Carbon, van escriure les proves, generant més de sis milions de línies de Lean, un llenguatge que permet la verificació automàtica per ordinador. Aproximadament l'1% del codi auditat va requerir una segona revisió humana.
L'anàlisi no va trobar noves vulnerabilitats en Signal. Per comprovar l'eficàcia del sistema, es van reintroduir dos errors prèviament corregits en una versió aïllada del codi, i el sistema va demostrar que la versió amb errors no era segura. Encara que el projecte no va verificar tota l'aplicació de Signal, DeepMind tenia avantatge gràcies a un treball previ de verificació formal per la Signal Foundation.
Ehren Kret, director de tecnologia de Signal, va destacar que l'enfocament de DeepMind permet una expansió significativa de les garanties de privacitat, crucial en un context de creixents amenaces de seguretat impulsades per la IA. No obstant això, encara queda per veure si aquest enfocament pot escalar-se a tot el programari global i a quin cost, ja que l'anàlisi de Signal va ser realitzat de forma gratuïta com un projecte de recerca.
DeepMind ha decidit obrir el codi font dels seus artefactes de verificació formal, suggerint que l'enfocament podria aplicar-se eventualment a sistemes crítics com el firmware de dispositius mèdics i el programari de la xarxa elèctrica.
Google DeepMind ha logrado un hito en la seguridad del software al verificar matemáticamente partes clave del código detrás del protocolo de cifrado de Signal en tan solo un mes, una tarea que tradicionalmente llevaba años a equipos de expertos. Este protocolo es fundamental para proteger las conversaciones privadas en aplicaciones como Signal, Google Messages y WhatsApp. Según Wired, la compañía describe este logro como un avance significativo, aunque los investigadores advierten que es solo un paso en un proceso más extenso.
La verificación formal, que utiliza matemáticas en lugar de pruebas, se considera la garantía de seguridad más sólida disponible. Sin embargo, ha sido históricamente lenta y laboriosa, deteniéndose a menudo en la fase de diseño. DeepMind ha ido más allá al verificar la implementación real, donde suelen esconderse los errores del mundo real. Este logro marca la primera vez que un protocolo ampliamente desplegado ha sido verificado formalmente por cualquier método, con o sin IA.
El sistema utilizado, denominado AlphaProof Code, combina modelos de IA con expertos humanos. Los investigadores tradujeron los objetivos de seguridad de Signal en especificaciones formales, que fueron revisadas por expertos humanos. Los agentes de IA, impulsados por Gemini Carbon, escribieron las pruebas, generando más de seis millones de líneas de Lean, un lenguaje que permite la verificación automática por ordenador. Aproximadamente el 1% del código auditado requirió una segunda revisión humana.
El análisis no encontró nuevas vulnerabilidades en Signal. Para comprobar la eficacia del sistema, se reintrodujeron dos errores previamente corregidos en una versión aislada del código, y el sistema demostró que la versión con errores no era segura. Aunque el proyecto no verificó toda la aplicación de Signal, DeepMind tenía ventaja gracias a un trabajo previo de verificación formal por la Signal Foundation.
Ehren Kret, director de tecnología de Signal, destacó que el enfoque de DeepMind permite una expansión significativa de las garantías de privacidad, crucial en un contexto de crecientes amenazas de seguridad impulsadas por la IA. Sin embargo, aún queda por ver si este enfoque puede escalarse a todo el software global y a qué coste, ya que el análisis de Signal fue realizado de forma gratuita como un proyecto de investigación.
DeepMind ha decidido abrir el código fuente de sus artefactos de verificación formal, sugiriendo que el enfoque podría aplicarse eventualmente a sistemas críticos como el firmware de dispositivos médicos y el software de la red eléctrica.
Google DeepMind has achieved a milestone in software security by mathematically verifying key parts of the code behind Signal's encryption protocol in just one month, a task that traditionally took years for expert teams. This protocol is essential for protecting private conversations in applications like Signal, Google Messages, and WhatsApp. According to Wired, the company describes this achievement as a significant breakthrough, although researchers caution that it is only a step in a more extensive process.
Formal verification, which uses mathematics instead of testing, is considered the strongest security guarantee available. However, it has historically been slow and laborious, often stalling at the design phase. DeepMind has gone further by verifying the actual implementation, where real-world errors typically hide. This achievement marks the first time a widely deployed protocol has been formally verified by any method, with or without AI.
The system used, called AlphaProof Code, combines AI models with human experts. Researchers translated Signal's security goals into formal specifications, which were reviewed by human experts. AI agents, powered by Gemini Carbon, wrote the proofs, generating over six million lines of Lean, a language that allows for automatic computer verification. Approximately 1% of the audited code required a second human review.
The analysis found no new vulnerabilities in Signal. To test the system's effectiveness, two previously fixed bugs were reintroduced into an isolated version of the code, and the system demonstrated that the buggy version was not secure. Although the project did not verify the entire Signal application, DeepMind had an advantage thanks to previous formal verification work by the Signal Foundation.
Ehren Kret, Signal's Chief Technology Officer, highlighted that DeepMind's approach allows for a significant expansion of privacy guarantees, crucial in a context of increasing AI-driven security threats. However, it remains to be seen whether this approach can scale to all global software and at what cost, as the Signal analysis was conducted for free as a research project.
DeepMind has decided to open source its formal verification artefacts, suggesting that the approach could eventually be applied to critical systems such as medical device firmware and power grid software.
¿Te ha interesado esta noticia?
Recibe cada mañana el resumen de IA y sociedad directo en tu email.
Suscríbete gratis →