Google DeepMind a annoncé le 10 novembre avoir vérifié formellement, grâce à des agents d’intelligence artificielle, des propriétés de sécurité essentielles du protocole de chiffrement de Signal, le même qui protège WhatsApp et Google Messages. Le travail, mené par cinq personnes en quatre semaines avec un outil baptisé AlphaProof Code, aurait demandé des années à des experts humains. Mais il ne garantit pas que l’application Signal soit sans faille, et son coût reste inconnu.
Ce que DeepMind a démontré
La vérification formelle ne consiste pas à tester un logiciel sur des milliers de cas : elle établit, par une démonstration mathématique contrôlée par une machine, qu’une propriété est vraie dans toutes les situations prévues par le modèle. D’après The Register, l’équipe a porté son effort sur deux briques du protocole : PQXDH, la poignée de main conçue pour résister aux futurs ordinateurs quantiques, et le Triple Ratchet, qui renouvelle les clés au fil des messages.
Les propriétés prouvées touchent au cœur de la promesse de Signal : la confidentialité persistante (un message ancien reste protégé même si une clé fuit plus tard), l’authentification des interlocuteurs, la récupération après la compromission temporaire d’un appareil et le secret de l’échange initial. Les chercheurs revendiquent une première : une IA aurait aidé à construire une preuve qui relie ces garanties théoriques à une implémentation cryptographique réellement utilisée, au niveau du code machine.
Comment fonctionne AlphaProof Code
L’outil est un système multi-agents. Des experts en cryptographie définissent ce qu’il faut prouver ; plusieurs modèles traduisent ces objectifs en une spécification que les experts relisent, puis des agents fondés sur Gemini Carbon, le modèle de Google, rédigent les preuves dans Lean, un assistant de preuve dont le noyau vérifie chaque étape. The Register évoque environ 6,5 millions de lignes de Lean générées, puis un audit automatique désignant les passages à faire relire par un humain. Selon le blog de DeepMind, qui parle de plus de six millions de lignes, cette relecture humaine n’a concerné qu’environ 1 % du code.
Pour s’assurer que l’outil ne valide pas n’importe quoi, l’équipe a fait un test à rebours. D’après 9to5Mac, des versions anciennes de Signal, porteuses de vulnérabilités connues, ont bien été signalées comme échouant à la vérification. DeepMind précise que deux bugs réels, corrigés depuis, ont été réintroduits dans une copie isolée du code : dans les deux cas, le système a produit une preuve vérifiée par la machine que la version fautive n’était pas sûre.
Le chercheur Swarat Chaudhuri, de DeepMind et de l’université du Texas à Austin, insiste sur le rôle des humains. Cité par The Register, il estime que la prochaine difficulté ne sera plus la preuve mais la spécification, c’est-à-dire la définition exacte de ce que le logiciel doit garantir. Du côté de Signal, son directeur technique Ehren Kret, cité par DeepMind, qualifie de « major breakthrough » le fait que des agents traduisent du code en production en théorèmes Lean valides, les vérifications formelles antérieures s’étant concentrées sur des portions plus réduites du code.
Ce que ce travail ne prouve pas
Le titre de 9to5Mac, qui parle d’un chiffrement « prouvé sûr », va plus loin que le contenu. La démonstration porte sur le protocole et certaines de ses garanties, pas sur l’application Signal entière, ni sur la manière dont WhatsApp ou Google Messages l’ont intégré. The Register rappelle aussi que le résultat suppose une cryptographie parfaite : il ne dit rien de la solidité mathématique des algorithmes eux-mêmes.
Reste la question de l’échelle. Ni le coût de calcul ni le volume exact de ressources consommées n’ont été publiés. Swarat Chaudhuri reconnaît lui-même, selon 9to5Mac, qu’il reste « a long distance to go » avant d’appliquer la méthode à l’ensemble des logiciels. DeepMind annonce en revanche publier en accès libre ses artefacts de vérification, accompagnés d’un article technique. Selon The Register, ce travail rapproche aussi d’un défi lancé en avril par la Beneficial AI Foundation : vérifier formellement en Lean le protocole et l’application Signal.
Pourquoi c’est important
Des projets de vérification célèbres ont mobilisé des années de travail : The Register cite le micronoyau seL4, qui a demandé une vingtaine d’années-personnes. Si des agents peuvent réduire ce délai à quelques semaines, la vérification formelle pourrait sortir des laboratoires pour couvrir des briques critiques comme les bibliothèques de chiffrement, les protocoles de messagerie ou les systèmes embarqués. Pour les entreprises, la leçon immédiate est plus modeste : une preuve vaut ce que vaut sa spécification, et l’expertise humaine reste le maillon décisif.
Questions fréquentes
Signal est-il désormais impossible à pirater ?
Non. Le travail de DeepMind prouve des propriétés précises du protocole, sous l’hypothèse d’une cryptographie parfaite. L’application, le téléphone et les erreurs d’utilisation restent des points d’attaque possibles.
WhatsApp est-il concerné ?
WhatsApp et Google Messages utilisent le protocole Signal, donc les garanties démontrées sur le protocole les concernent. Leur propre implémentation n’a en revanche pas été vérifiée dans ce travail.
Qu’est-ce que Lean ?
Lean est un assistant de preuve : un logiciel qui vérifie mécaniquement chaque étape d’une démonstration. Une preuve acceptée par son noyau ne dépend pas de la confiance accordée à l’IA qui l’a rédigée.
Sources
- Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques — The Register, 2026-11-10
- Google DeepMind analysis proves Signal and WhatsApp encryption is secure — 9to5Mac, 2026-11-10
- Introducing AlphaProof Code — Google DeepMind (blog officiel), 2026-11-10