Signal prouvé sûr par l’IA : Google lâche jusqu’à 80 agents et 6,5 millions de lignes de preuves sur son chiffrement

Google DeepMind affirme avoir démontré mathématiquement que le code de chiffrement de Signal tient ses promesses. Présenté mardi 10 novembre, le système AlphaProof Code a fait travailler des équipes d’agents IA pendant quatre semaines sur libsignal, la bibliothèque de référence du protocole, jusqu’au niveau du code machine exécuté par le processeur.

Le protocole Signal ne protège pas seulement l’application du même nom. Des variantes équipent WhatsApp, Messenger et Google Messages, soit des milliards de conversations. Son design a déjà été passé au crible par des cryptographes, à plusieurs reprises. La nouveauté revendiquée par DeepMind est ailleurs : la preuve ne porte plus sur une description théorique du protocole, mais sur le programme réellement compilé. « C’est la première fois que l’implémentation d’un protocole aussi largement déployé est vérifiée formellement, par quelque méthode que ce soit, avec ou sans IA », écrivent Pushmeet Kohli et Swarat Chaudhuri dans le billet d’annonce.

6,5 millions de lignes de Lean, aucune écrite à la main

Les chercheurs ont pris le code Rust de libsignal-protocol (version 0.105.4) sans le modifier, l’ont emballé dans un petit outil en ligne de commande et l’ont compilé avec rustc pour des processeurs ARM 64 bits (AArch64) sous Linux. Les théorèmes portent sur ce binaire, décrit grâce à un modèle formel du processeur écrit en Lean, un langage dont le noyau vérifie automatiquement chaque étape d’une démonstration.

Le travail se fait en deux temps. D’abord la spécification : des humains, épaulés par des agents tournant sur Gemini 4 Carbon et Claude Opus 5.5, traduisent en énoncés mathématiques les garanties attendues du protocole. Chaque énoncé est relu et validé par un expert. Ensuite la preuve, confiée entièrement aux agents. Selon l’article technique, une campagne mobilisait typiquement 40 à 80 agents sur une seule machine pendant 24 à 72 heures, et « aucun des auteurs n’a écrit de code de preuve ». Les agents n’ont pas le droit de toucher à la spécification. Une démonstration n’est acceptée que si le noyau de Lean la valide.

Résultat : environ 6,5 millions de lignes de preuves vérifiées par la machine, qui reposent sur quelque 26 000 lignes de spécifications et de sémantique AArch64 jugées de confiance. Cinq chercheurs ont mené le projet en quatre semaines, un travail qui aurait demandé des années avec les outils précédents, selon DeepMind. Les preuves couvrent la poignée de main post-quantique PQXDH et le Triple Ratchet, qui renouvelle les clés à chaque échange. Elles établissent quatre propriétés : la confidentialité persistante (un voleur de clés ne peut pas relire les anciens messages), l’authentification, la sécurité après compromission (la conversation redevient sûre une fois de nouvelles clés échangées) et le secret de la poignée de main.

Deux anciennes failles réinjectées pour tester l’outil

Une preuve n’a de valeur que si la spécification est assez stricte pour attraper un vrai défaut. Pour le vérifier, l’équipe a réintroduit dans libsignal deux bugs découverts par d’autres chercheurs et corrigés depuis, en annulant les correctifs correspondants avant de recompiler. L’un d’eux poussait la bibliothèque à conserver l’état d’une nouvelle session, avec une copie d’une clé secrète, quand un message ne se déchiffrait qu’avec une session archivée. Dans les deux cas, AlphaProof Code a produit une preuve vérifiée que la version bugguée violait les garanties de sécurité. Aucune nouvelle faille n’a en revanche été trouvée dans le code actuel.

Signal a suivi la démarche. « Utiliser des agents 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 Google. L’opération s’inscrit dans le défi « Signal Shot », lancé en avril 2026 par la Beneficial AI Foundation, Signal et la Lean FRO pour vérifier formellement le protocole et l’application.

Les limites sont documentées noir sur blanc dans l’article. Seules les conversations à deux sont couvertes, pas les groupes. Les primitives cryptographiques de base (X25519, AES, HMAC, Kyber1024) sont supposées fonctionner parfaitement et ne sont pas prouvées. Le modèle computationnel n’offre aucune garantie face à un attaquant quantique, et il restreint certaines capacités de l’adversaire. Enfin, la cible est un binaire de test sous Linux ARM, pas les applications Android et iOS que les utilisateurs installent.

Google publie les spécifications et les preuves en open source sur GitHub (dépôt google-deepmind/code-verification), avec l’article technique. L’entreprise voit dans ces travaux une méthode applicable demain aux firmwares d’appareils médicaux ou aux logiciels des réseaux électriques, en complément de son agent de correction de failles CodeMender.

Sources : Google DeepMind, article technique AlphaProof Code, dépôt GitHub, Wired.

Ajouter Geek Actu à mes sources préférées sur Google