Des agents IA de Google ont vérifié le cœur du chiffrement de Signal en quatre semaines

Pour éprouver leur système, les chercheurs de Google DeepMind ont saboté une copie isolée du code de Signal. Ils y ont réintroduit deux failles réelles, corrigées en 2025. La première amenait la bibliothèque à enregistrer à tort un état de session contenant une clé secrète. La seconde, un bug dit de petit sous-groupe, venait d'un contrôle manquant sur les clés X25519 reçues, le mécanisme utilisé pour l'échange de clés. Dans les deux cas, la machine a produit une preuve, contrôlée automatiquement, que la version piégée violait les garanties attendues.

Google DeepMind a présenté cet outil, AlphaProof Code, le 10 novembre. Le partage des rôles est simple : des experts humains décident de ce qu'il faut prouver, et des agents d'IA, animés par le modèle Gemini Carbon de Google, rédigent les preuves. Celles-ci sont écrites pour Lean, un « assistant de preuve » qui accepte ou rejette mécaniquement chaque étape. Première cible : libsignal, la bibliothèque de référence du protocole Signal. Ce protocole protège la messagerie du même nom et, selon DeepMind, Google Messages.

Une preuve faite sur le programme qui tourne réellement

Le travail porte sur les conversations à deux. Il couvre l'échange de clés initial, baptisé PQXDH, qui intègre une protection contre les ordinateurs quantiques. Il couvre aussi le « triple cliquet » (Triple Ratchet), qui renouvelle les clés au fil des messages. Parmi les propriétés démontrées :

• la confidentialité persistante : une clé volée ne permet pas de relire les anciens messages ;
• la sécurité après compromission : la protection se rétablit après un piratage passager ;
• l'authentification des interlocuteurs ;
• dans le modèle dit symbolique, la résistance à la stratégie « collecter maintenant, déchiffrer plus tard ».

La nouveauté tient au niveau de la preuve. Elle ne porte pas sur le code source, mais sur le programme compilé pour processeur ARM 64 bits à partir des versions publiques, non modifiées, de libsignal (0.105.4) et de son module post-quantique SPQR (1.6.0). Inutile, donc, de faire confiance au compilateur. Selon l'article technique, les agents ont produit environ 6,5 millions de lignes de preuve. Elles reposent sur quelque 26 000 lignes de spécifications et de description du processeur.

Le chantier a pris quatre semaines à une équipe de cinq personnes, selon The Register. Le site rapporte que l'article de recherche compare ce délai aux 20 années-personnes qu'avait demandées la vérification du micronoyau seL4. « Utiliser des agents d'IA pour traduire du code en production en théorèmes Lean valides est une avancée majeure », estime Ehren Kret, directeur technique de Signal, cité par DeepMind.

Ce que la preuve laisse de côté

Les auteurs listent eux-mêmes ce qui n'est pas couvert :

• les attaques par canaux auxiliaires, qui observent par exemple le temps de calcul, et les autres secrets présents en mémoire ;
• les conversations de groupe, l'usage sur plusieurs appareils et les applications Android et iOS elles-mêmes ;
• la génération des clés et le code des briques cryptographiques (ML-KEM, Kyber, opérations sur les courbes X25519 et Edwards, HMAC du module SPQR), remplacées par des « contrats » supposés respectés ;
• l'attaquant quantique dans la preuve dite calculatoire, ainsi que le rétablissement post-quantique propre à SPQR.

Autrement dit, la logique de l'échange post-quantique est vérifiée, mais la solidité des algorithmes eux-mêmes reste une hypothèse : le modèle symbolique suppose une cryptographie parfaite. Swarat Chaudhuri, chercheur chez DeepMind, admet auprès de The Register que l'approche n'est pas « le dernier mot ». Selon lui, la difficulté se déplace vers les spécifications, c'est-à-dire décider quoi prouver. Selon DeepMind, les agents ont d'ailleurs signalé environ 1 % du code pour un second regard humain.

Ce que cela change pour vous

Les utilisateurs de Signal n'ont rien à faire. Pour les entreprises, la vérification formelle, longtemps réservée à quelques projets très coûteux, pourrait devenir envisageable pour du code cryptographique critique. Là où OpenAI et Anthropic financent, avec la Simons Foundation, un programme pour aider les mathématiciens à vérifier les résultats obtenus avec l'IA, les preuves de DeepMind sont contrôlées par une machine. Les preuves sont publiées sur GitHub. DeepMind n'a en revanche ni chiffré le coût de l'opération ni annoncé de service commercial. Reste à savoir si la méthode suivra le rythme des mises à jour de Signal, et si elle s'appliquera à des logiciels bien plus gros.