AlphaProof Code de Google DeepMind vérifie formellement le protocole cryptographique de Signal

Google DeepMind affirme avoir franchi une étape majeure en matière de sécurité logicielle, longtemps considérée comme un défi de taille : ses chercheurs ont guidé des agents IA pour prouver mathématiquement des propriétés de sécurité clés du code réel underlying le protocole Signal, la technologie qui protège des milliards de conversations privées dans des applications telles que Signal et Google Messages en chiffrant les messages de bout en bout, de sorte que seuls l'expéditeur et le destinataire prévu peuvent les lire. L'annonce a été publiée sur le blog Google DeepMind par Pushmeet Kohli et Swarat Chaudhuri.

Le résultat a été obtenu avec AlphaProof Code, un nouveau framework agentique de vérification formelle à une profondeur inédite, combinant l'expertise humaine et des agents IA. La vérification formelle — la preuve mathématique qu'un code s'exécute correctement sans défaut — constitue le plus haut standard d'assurance de sécurité, mais elle est difficile et souvent laborieuse. Les tests conventionnels échantillonnent le comportement d'un programme ; une preuve formelle exclut les défauts sur toutes les exécutions possibles — un niveau d'assurance si coûteux à produire qu'il a rarement atteint les logiciels largement déployés.

Selon l'entreprise, ce travail marque la première fois que l'IA est utilisée pour vérifier formellement un protocole cryptographique largement déployé à cette profondeur. C'est également la première fois que l'implémentation d'un protocole largement déployé de ce type est vérifiée formellement par quelque méthode que ce soit, avec ou sans IA.

Comment Google DeepMind a vérifié Signal

AlphaProof Code est un framework agentique multi-LLM qui répartit le travail de vérification formelle comme le ferait une équipe de recherche : des experts humains travaillent avec l'IA pour décider ce qu'il faut prouver, et un groupe d'agents IA exécute les preuves.

Dans un premier temps, les chercheurs de Google DeepMind ont collaboré avec un ensemble de modèles pour traduire les objectifs de sécurité de Signal en spécifications mathématiques formelles, chaque spécification étant examinée par des experts humains. Des agents propulsés par Gemini Carbon ont ensuite réalisé les preuves, générant plus de six millions de lignes de Lean, un langage informatique qui prouve mathématiquement l'exactitude du code.

Les agents ont ensuite audité la preuve et signalé les zones nécessitant un second regard humain — soit un pour cent seulement de la base de code, ce que l'entreprise décrit comme un gain de temps considérable. Comme Lean vérifie automatiquement le reste, les experts ont pu concentrer leur revue là où le jugement humain compte le plus.

Prouver la sécurité jusqu'au code en exécution

Les protocoles cryptographiques sous-tendent presque toutes les communications numériques, de la banque en ligne à la navigation web, et un seul défaut peut exposer des millions de personnes à la fois. C'est pourquoi les experts les analysent formellement depuis des décennies, même si la plupart des vérifications de protocoles s'arrêtaient au niveau de la conception.

Les agents de Google DeepMind sont allés plus loin, prouvant que le code compilé satisfait les propriétés de sécurité clés — comme le maintien de la protection des messages avant et après la compromission temporaire d'un appareil, des garanties que les cryptographes connaissent sous les noms de confidentialité durable (forward secrecy) et sécurité après compromission (post-compromise security) — jusqu'au code exact exécuté sur les appareils. Les vulnérabilités du monde réel se cachent souvent dans l'écart entre la conception et l'implémentation, et combler cet écart rend ces preuves considérablement plus complexes.

Malgré ce niveau de complexité, le processus de vérification n'a pris que quatre semaines — une tâche qui exigeait historiquement des années aux équipes d'experts, selon l'entreprise — établissant que le code cryptographique central de Signal offre les protections de sécurité spécifiées par les chercheurs.

Pour confirmer qu'AlphaProof Code peut distinguer un code correct d'un code défectueux, l'équipe a réintroduit deux bugs réels, précédemment corrigés, dans une version isolée du code de Signal. Dans les deux cas, le système a produit une preuve vérifiée par machine établissant que la version défectueuse n'était pas sûre — un contrôle essentiel, car un vérificateur incapable de signaler un code défaillant fournirait une fausse assurance.

Dans AlphaProof Code, les agents IA aident les utilisateurs à rédiger une spécification, puis prouvent de manière autonome que l'implémentation y répond. Chaque preuve est vérifiée par Lean pour contrôler le travail des agents.

La réponse de Signal

« Alors que la vérification formelle précédente se concentrait sur des portions plus restreintes du code, l'approche de Google DeepMind permet une extension significative », a déclaré Ehren Kret, directeur technique de Signal. « L'utilisation d'agents IA pour traduire du code réel en théorèmes Lean valides est une avancée majeure. À mesure que les menaces de sécurité pilotées par l'IA augmentent, la vérification rigoureuse de l'implémentation du protocole Signal nous donne une confiance encore plus grande dans les garanties de confidentialité de notre code. »

L'avenir de la sécurité

Google DeepMind estime que relever ce défi de longue date démontre comment l'IA peut apporter une assurance de sécurité de haut niveau aux entreprises, aux gouvernements et aux infrastructures critiques, contribuant à se défendre contre les cybermenaces pilotées par des agents. La vérification de la cryptographie centrale de Signal, selon l'entreprise, pose les bases pour sécuriser d'autres systèmes essentiels, du firmware des dispositifs médicaux aux logiciels des réseaux électriques.

Le déploiement à grande échelle de ces techniques nécessite des recherches continues. Associée à des agents de défense automatisés tels que CodeMender, la vérification formelle peut aider à contrer la vitesse et l'échelle des cybermenaces modernes et à créer des logiciels dotés d'une preuve mathématique que leurs protections fonctionnent.

Google DeepMind publie en open source ses artefacts de vérification formelle pour la communauté, hébergés sur google-deepmind.github.io/code-verification. Le document technique complet est disponible en PDF. Pour la communauté de la recherche en sécurité, cette publication offre un moyen d'inspecter directement les preuves vérifiées par machine et la méthodologie — et l'ampleur de la diffusion de la vérification à cette profondeur au-delà de Signal, vers les systèmes médicaux, industriels et d'infrastructure cités par l'entreprise, constitue la prochaine évolution à suivre.

Remerciements

La recherche a été développée par Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton et Pushmeet Kohli.

L'équipe a remercié Eric Wieser pour son aide à la publication open source du code, Owen Jones pour son soutien en gestion de programme, ainsi que Martín Abadi, Christopher Henson, Katerina Hristova, Henryk Michalewski, Jonathan Protzenko et George Tsoukalas pour leurs discussions fructueuses. Les chercheurs ont également remercié Rolfe Schmidt, Michael Rosenberg et Ehren Kret de Signal pour leurs retours sur la méthodologie, ainsi que Tulsee Doshi, Four Flynn, Kate Olszewska, Alicia Huang, Andy Liu, Benoit Schillings, Raluca Ada Popa, Melvin Johnson, Koray Kavukcuoglu, Demis Hassabis et Sundar Pichai pour leur soutien au projet.