DeepMind : une IA prouve mathématiquement la sécurité du chiffrement de Signal

Une intelligence artificielle vient de démontrer, preuve mathématique à l’appui, que le cœur du chiffrement de Signal tient ses promesses. Le 10 novembre 2026, Google DeepMind a présenté AlphaProof Code, un système qui associe experts humains et agents d’IA pour vérifier formellement du code. Sa première démonstration porte sur libsignal, la bibliothèque qui assure le chiffrement de bout en bout de la messagerie.

Le résultat a de quoi impressionner : environ 6,5 millions de lignes de preuve, produites en quatre semaines par une équipe de cinq personnes, et vérifiées jusqu’au code machine qui s’exécute réellement sur les téléphones. Aucune nouvelle faille n’a été découverte. L’exercice ne couvre toutefois qu’une partie de l’application et repose sur plusieurs hypothèses.

AlphaProof Code et Signal en chiffres

Annonce	10 novembre 2026, par Google DeepMind
Code vérifié	libsignal 0.105.4, compilé pour processeurs Arm 64 bits
Composants	PQXDH (établissement de la session, résistant au quantique) et Triple Ratchet (renouvellement des clés)
Taille de la preuve	Environ 6,5 millions de lignes en Lean
Durée	4 semaines, pour une équipe de 5 personnes
Relecture humaine	Toutes les spécifications, plus environ 1 % du code signalé par les agents
Nouvelles failles	Aucune

AlphaProof Code, un duo entre humains et agents d’IA

La vérification formelle consiste à prouver mathématiquement qu’un programme respecte des propriétés précises, plutôt que de se contenter de le tester. La méthode est réputée fiable mais extrêmement coûteuse : il faut écrire des preuves d’une longueur considérable, ligne à ligne.

AlphaProof Code répartit le travail. Les humains décident de ce qu’il faut prouver : les chercheurs ont traduit les objectifs de sécurité de Signal en spécifications formelles, avec l’aide de plusieurs modèles d’IA, et des experts ont relu chacune d’entre elles. Des agents propulsés par Gemini Carbon, le modèle de Google, rédigent ensuite les preuves dans Lean, un assistant de preuve dont le noyau vérifie chaque étape du raisonnement. Une passe d’audit, elle aussi confiée aux agents, a signalé environ 1 % du code pour un second examen humain.

Selon l’article technique publié par DeepMind, aucun des auteurs n’a écrit lui-même de code de preuve. « C’est un système fondamentalement conçu pour la collaboration entre humains et IA », résume Swarat Chaudhuri, chercheur chez Google DeepMind et professeur à l’université du Texas à Austin, interrogé par The Register. Le nom du système fait écho à AlphaProof, l’IA de DeepMind qui avait atteint en 2024 le niveau d’une médaille d’argent aux Olympiades internationales de mathématiques.

Jusqu’au code machine qui tourne sur les téléphones

L’originalité du travail tient à sa profondeur. DeepMind n’a pas vérifié le code source en Rust de libsignal, mais l’exécutable compilé pour les processeurs Arm 64 bits, ceux de la quasi-totalité des smartphones. L’équipe a modélisé dans Lean le comportement des instructions machine, puis prouvé les propriétés de sécurité sur ce modèle. Une erreur introduite lors de la compilation entre donc, elle aussi, dans le champ de la preuve.

Deux briques du protocole ont été passées au crible. PQXDH est la poignée de main qui établit un secret partagé au début d’une conversation, conçue pour résister aux futurs ordinateurs quantiques. Le Triple Ratchet renouvelle en permanence les clés de chiffrement au fil des messages.

Les propriétés prouvées couvrent la confidentialité et l’authenticité des messages, la confidentialité persistante (les anciens messages restent protégés si les clés actuelles sont volées), la récupération de la sécurité après la compromission temporaire d’un appareil, et le secret de la poignée de main même si un attaquant parvenait plus tard à casser le Diffie-Hellman classique, un scénario qui simule la menace quantique.

Quatre semaines au lieu de plusieurs années

Pour mesurer le gain, The Register rappelle deux références du domaine : la vérification formelle du micronoyau seL4 avait demandé environ 20 années-personnes, et le développement du compilateur C vérifié CompCert s’était étalé sur six ans. Ici, cinq personnes ont bouclé le travail en quatre semaines, en consommant selon les chercheurs « pas mal de tokens ». Google n’a pas communiqué le coût de l’opération.

L’essentiel de l’effort humain s’est déplacé. D’après l’article technique, la majorité du travail n’a pas porté sur les preuves mais sur les spécifications, soit environ 26 000 lignes de définitions et de sémantique machine sur lesquelles repose l’ensemble. « Nous pensons vraiment que la prochaine frontière ne sera pas la preuve, mais la spécification », estime Swarat Chaudhuri.

Côté Signal, l’accueil est enthousiaste. « Utiliser des agents d’IA pour traduire du code en production en théorèmes Lean valides est une avancée majeure », salue Ehren Kret, directeur technique de Signal, cité par DeepMind. Les travaux s’inscrivent dans un défi lancé en avril par la Beneficial AI Foundation, qui visait à vérifier formellement le protocole et l’application Signal avec Lean.

Deux anciens bugs réintroduits pour tester la méthode

Une preuve n’a de valeur que si elle sait aussi détecter un code défaillant. Pour s’en assurer, l’équipe a réintroduit dans des copies isolées de libsignal deux bugs réels, corrigés depuis. Dans les deux cas, le système a produit une preuve vérifiée par la machine que la version modifiée violait bien une propriété de sécurité.

Ce test répond à une critique classique : une vérification trop permissive pourrait valider n’importe quel code. Ici, la méthode a correctement repéré les versions vulnérables.

Ce que la preuve ne couvre pas

DeepMind présente ce travail comme une démonstration, pas comme une chasse aux failles. Plusieurs limites encadrent le résultat :

• les preuves supposent que les primitives cryptographiques sous-jacentes sont parfaites ;
• les attaques par canaux auxiliaires, qui exploitent par exemple le temps de calcul ou la consommation électrique, sont exclues ;
• seul le cœur du protocole est vérifié : l’interface de l’application, les sauvegardes et le reste du code de Signal sont hors champ ;
• les garanties dépendent des modèles d’attaquant retenus et de la justesse des spécifications, qui ne peuvent pas être vérifiées automatiquement.

Les chercheurs le reconnaissent eux-mêmes : l’IA peut réduire le coût de l’écriture des spécifications et de l’assurance logicielle, mais pas remplacer entièrement le jugement et la relecture humaine.

Ce que cela change pour les utilisateurs

Pour les utilisateurs de Signal, rien ne change dans l’application, mais la confiance dans son chiffrement gagne un appui mathématique. Le protocole Signal sert aussi de base au chiffrement d’autres messageries, comme WhatsApp ou Google Messages. Attention cependant : c’est l’implémentation de référence libsignal qui a été vérifiée, pas le code propre à ces applications.

À plus long terme, DeepMind voit dans cette approche un moyen de sécuriser des logiciels critiques, comme le micrologiciel d’appareils médicaux ou les logiciels de pilotage des réseaux électriques. Les éléments de vérification ont été publiés en open source sur GitHub, afin que la communauté puisse les examiner et les réutiliser.