AlphaProof Code : l’IA de DeepMind prouve mathématiquement la sécurité du chiffrement de Signal

Dire qu’un logiciel est sûr est une chose ; le démontrer mathématiquement en est une autre, bien plus exigeante. C’est ce que vient de réaliser Google DeepMind sur l’un des logiciels de chiffrement les plus utilisés au monde. Le laboratoire a présenté le 10 novembre 2026 AlphaProof Code, un système qui combine expertise humaine et agents d’IA, et l’a appliqué au cœur cryptographique de Signal, la messagerie chiffrée de bout en bout. Résultat : des propriétés de sécurité clés prouvées en quatre semaines, un travail qui, selon DeepMind, prend historiquement des années à des équipes d’experts.

Qu’est-ce que la vérification formelle ?

La plupart des logiciels sont testés : on les fait tourner sur de nombreux cas et on vérifie qu’ils se comportent bien. Mais un test ne couvre que les situations envisagées. La vérification formelle va plus loin : elle consiste à démontrer, comme un théorème de mathématiques, qu’un programme respecte une propriété dans tous les cas possibles, selon un modèle d’attaquant défini à l’avance.

Cette méthode est réputée pour sa fiabilité, mais aussi pour son coût. Écrire ces preuves à la main est si long qu’on la réserve d’ordinaire à des systèmes critiques, comme l’aéronautique. C’est précisément ce goulet d’étranglement que DeepMind veut faire sauter avec l’IA.

Une répartition des rôles entre humains et IA

AlphaProof Code est décrit par DeepMind comme un cadre réunissant plusieurs modèles de langage dans un système d’agents. Le partage du travail est clair :

Selon DeepMind, les agents n’ont signalé qu'environ 1 % du code pour un examen humain. Les preuves produites dépassent six millions de lignes, un volume qu’aucune équipe humaine ne pourrait écrire en quelques semaines.

Ce qui a été prouvé sur Signal

La cible est libsignal, la bibliothèque de référence qui met en œuvre le protocole de chiffrement de Signal. Fait notable, la vérification ne porte pas sur une description abstraite du protocole, mais sur le code machine compilé, c’est-à-dire les instructions effectivement exécutées par un processeur Arm 64 bits, celui des smartphones modernes. DeepMind a pour cela modélisé dans Lean le processeur qui exécute ce code.

Les propriétés démontrées concernent notamment le fait de garder les messages protégés avant et après la compromission temporaire d’un appareil. Selon le site spécialisé CyberInsider, les preuves couvrent la phase d’établissement de la connexion entre deux appareils et le mécanisme qui renouvelle en permanence les clés de chiffrement, y compris dans un scénario où un futur ordinateur quantique casserait une partie de la cryptographie classique.

Pour tester la méthode, les chercheurs ont réintroduit deux véritables bogues, corrigés depuis, dans une copie isolée du code de Signal. Dans les deux cas, le système a produit une preuve vérifiée par machine que la version modifiée n’était pas sûre. Aucune nouvelle faille n’a été signalée dans les parties examinées.

Pourquoi vérifier le code machine plutôt que le code source ?

Les développeurs écrivent leurs programmes dans un langage lisible par les humains, ici le Rust. Un logiciel appelé compilateur traduit ensuite ce code source en instructions pour le processeur. Or cette traduction n’est pas neutre : optimisations, choix du compilateur ou subtilités du langage peuvent produire un comportement légèrement différent de celui que l’on croit avoir écrit. Prouver la sécurité du code source laisse donc une zone d’ombre entre ce qui est écrit et ce qui s’exécute réellement.

En travaillant directement sur le code machine, DeepMind réduit cet écart : la preuve porte sur les instructions que le processeur exécute vraiment. C’est l’un des points qui distinguent ces travaux des vérifications menées jusqu’ici sur des modèles abstraits du protocole.

Ce que la preuve ne garantit pas

Une preuve formelle n’est valable que dans le cadre défini au départ. Plusieurs limites sont précisées par DeepMind et dans les fichiers publiés :

• la vérification porte sur la bibliothèque libsignal compilée dans un environnement de test en ligne de commande, et non sur les applications Signal telles qu’elles sont distribuées ;
• les primitives cryptographiques de base, comme les algorithmes de chiffrement eux-mêmes, sont modélisées et considérées comme fiables, sans être vérifiées à leur tour ;
• les attaques par canaux auxiliaires, qui exploitent par exemple le temps de calcul ou la consommation électrique, ne sont pas couvertes, selon CyberInsider ;
• les garanties dépendent des modèles d’attaquant retenus : un modèle dit symbolique et un modèle calculatoire, plus proche de la cryptographie réelle.

Autrement dit, la preuve ne rend pas Signal invulnérable : elle établit que, dans ce cadre précis, le code se comporte comme prévu.

Des résultats vérifiables par tous

DeepMind a publié l’ensemble des preuves en open source sous licence Apache 2.0, sur sa plateforme GitHub. N’importe qui disposant de Lean peut les revérifier, à condition d’avoir de la patience et une machine puissante : la compilation et la vérification prennent plusieurs heures et mobilisent jusqu’à plusieurs dizaines de gigaoctets de mémoire. En revanche, le cadre AlphaProof Code lui-même n’a pas été annoncé comme disponible pour le public.

Signal a été associé à la démarche. Trois de ses ingénieurs sont remerciés pour leurs retours sur la méthode, et son directeur technique, Ehren Kret, cité par DeepMind, salue « une avancée majeure » : utiliser des agents d’IA pour traduire du code en production en théorèmes Lean valides. Selon lui, une vérification aussi rigoureuse donne une confiance encore plus grande dans les garanties de confidentialité du code.

Quand l’IA sert à prouver plutôt qu’à deviner

Ce travail s’inscrit dans une tendance de fond : utiliser l’IA non seulement pour produire du contenu, mais pour démontrer des résultats vérifiables par machine. Les mathématiques en ont déjà bénéficié, comme avec la conjecture KLS résolue avec l’aide de l’IA en octobre. En cybersécurité, l’IA est aussi utilisée pour trouver des failles, à l’image des 948 vulnérabilités du noyau Linux exploitées par des agents d’OpenAI. La vérification formelle prend le problème par l’autre bout : prouver l’absence de certaines failles plutôt que d’en chercher.

DeepMind estime que ces travaux posent les bases d’une vérification à grande échelle de logiciels critiques, comme les micrologiciels d’appareils médicaux ou les logiciels qui pilotent les réseaux électriques. Si la méthode se généralise, la question ne sera plus seulement de savoir si un logiciel a été bien testé, mais s’il a été prouvé. Reste à démontrer qu’elle s’applique avec la même efficacité à des systèmes moins bien documentés que Signal, dont le protocole est étudié par les cryptographes depuis des années.