Une équipe de cinq personnes et l'IA ont prouvé le code de Signal en quatre semaines

Quatre semaines. C'est le temps qu'il a fallu à une équipe de cinq personnes de Google DeepMind, travaillant avec des agents d'IA, pour produire des preuves vérifiées par machine des propriétés de sécurité essentielles du code compilé de la bibliothèque de messagerie principale de Signal. Ces preuves représentent environ 6,5 millions de lignes de code. Des travaux similaires menés précédemment sur d'autres systèmes avaient nécessité des années de travail de spécialistes et, généralement, l'écriture du code à prouver.

L’article de recherche, daté du 10 novembre 2026, expose la méthode et ses limites. Le document technique qui accompagne ce document présente ces chiffres plus en détail. Ce travail ne constitue pas une preuve de l'application Signal dans son ensemble, ni d'autres applications utilisant une conception similaire. Il s'agit d'une preuve de propriétés spécifiques de libsignal, la bibliothèque de référence, pour les sessions individuelles, traduites en code machine compilé exécuté.

Ce qui a été prouvé

libsignal est la bibliothèque qui implémente le système de chiffrement Signal. En clair, ce système vise à garantir la confidentialité d'un message même en cas de vol ultérieur de la clé, et à permettre sa récupération après une brève compromission du système. Ces deux concepts sont généralement appelés confidentialité persistante et sécurité post-compromission.

L'équipe a compilé la bibliothèque originale (version 0.105.4, ainsi que la crate SPQR associée en version 1.6.0) avec le compilateur Rust standard, pour obtenir un petit outil en ligne de commande fonctionnant sous Linux ARM 64 bits. Les preuves portent sur cet exécutable, et non sur une réécriture optimisée. La bibliothèque vérifiée pèse environ 560 Ko, soit environ 140 000 instructions machine.

Ils couvrent l'établissement d'une session PQXDH, qui permet à deux personnes d'initier une session privée, incluant une étape post-quantique conçue pour résister aux attaques d'un futur ordinateur quantique, ainsi que le mécanisme Triple Ratchet, qui génère une nouvelle clé pour chaque message. Dans le modèle « symbolique », qui considère la cryptographie sous-jacente comme idéale, l'article affirme également la confidentialité de l'établissement de la session face à une attaque ultérieure utilisant un ordinateur quantique. Les discussions de groupe, l'expéditeur scellé (sealed sender) et le protocole côté serveur sont laissés pour des travaux futurs.

Comment le travail a été effectué

La vérification formelle consiste à formuler un énoncé mathématique précis du comportement attendu du code, puis à prouver que ce dernier s'y conforme. Une seule hypothèse erronée peut invalider le résultat ; il est donc indispensable de définir ce qu'il faut prouver et de valider cet énoncé.

L'article est clair quant à la répartition des tâches. Les humains ont sélectionné les propriétés, levé les ambiguïtés et validé le cahier des charges. Des agents ont ensuite rédigé les preuves. Ces preuves ne sont acceptées que si Lean, un système de vérification de preuves, les confirme. La fiabilité du résultat, expliquent les auteurs, ne dépend pas de la fiabilité des agents de preuve, car le noyau de Lean vérifie la logique.

L'article de recherche indique que les agents de preuve étaient basés sur Gemini Carbon. Le travail de preuve lui-même a été réalisé par cinq chercheurs en quatre semaines, chacun exécutant des agents sur son propre poste de travail. Il s'agit d'une campagne courte pour le domaine. L'article note que le micro-noyau seL4, une vérification antérieure bien connue, a nécessité vingt années-personnes, et le compilateur C CompCert, six. Ces deux bases de code ont été conçues en tenant compte de la preuve. Ce n'était pas le cas de libsignal.

Vous voulez que l'IA vous fasse gagner des heures par semaine ? Notre guide gratuit vous explique comment.Téléchargez le guide gratuit →

Les preuves elles-mêmes peuvent être longues car elles traitent du code machine. Environ 6,5 millions de lignes sont des preuves : 5,3 millions concernant le binaire, auxquelles s’ajoutent des fichiers distincts pour les deux modèles de sécurité. Un lecteur souhaitant se fier aux affirmations principales doit néanmoins consulter les parties fiables : environ 18 000 lignes de spécification dans le dépôt, ainsi qu’environ 8 000 lignes du modèle de code machine Arm et des noms de symboles associés à l’exécutable. Les routines cryptographiques de bas niveau, deux fonctions de sortie et quelques appels de bibliothèque sont implicites, non démontrés.

Une vérification des anciens bogues

Pour vérifier la robustesse des affirmations, l'équipe a réintroduit deux bogues précédemment découverts par des chercheurs dans libsignal et depuis corrigés. Dans les deux cas, ils ont démontré que le théorème de sécurité symbolique ne s'applique pas au binaire défectueux. Ce test est utile : une spécification qui “ réussit ” encore sur du code connu pour être défectueux serait trop faible.

L'une de ces failles stockait l'état d'une nouvelle session, y compris une copie d'un secret, alors qu'un message de pré-clé n'avait été déchiffré que dans le cadre d'une session antérieure. L'autre acceptait une négociation dont la clé de base avait été altérée, créant ainsi une seconde session avec le même secret partagé.

Ce que le résultat ne dit pas

Les auteurs sont rigoureux et les limites sont importantes. Les preuves ne couvrent pas l'intégralité du système Signal, toutes les attaques possibles, ni même les primitives cryptographiques elles-mêmes. Les attaques par canaux auxiliaires sont exclues du champ d'application. La preuve computationnelle, qui tente de limiter les chances de succès d'un attaquant réel, n'offre aucune garantie contre un adversaire quantique, et sa limite devient inapplicable pour de multiples sessions longues comportant de nombreux tours.

Des variantes du même protocole sont utilisées dans WhatsApp, Messenger de Meta et Google Messages, précise l'article. Ces applications n'étaient pas l'objet de la démonstration. Une démonstration concernant libsignal ne s'applique pas automatiquement à tous les produits utilisant un langage similaire.

Ehren Kret, directeur technique de Signal, est cité dans l'article de recherche comme disant que la vérification rigoureuse de la mise en œuvre du protocole « nous donne une confiance encore plus grande dans les garanties de confidentialité de notre code ».

Les preuves et les spécifications sont publiées dans un dépôt ouvert.

Pourquoi c'est important

La plupart des personnes qui envoient un message privé n'ont jamais accès à la bibliothèque qui le chiffre. Une méthode permettant de vérifier le code compilé de cette bibliothèque en quelques semaines plutôt qu'en plusieurs années-personnes représente une avancée majeure dans l'audit de ce type de logiciel. Il ne s'agit pas d'une certification attestant que Signal, ou toute autre application de messagerie instantanée, est exempte de failles. C'est un argument, vérifié automatiquement, concernant des propriétés spécifiques d'une bibliothèque essentielle, produit suffisamment rapidement pour permettre l'audit d'autres parties critiques du code par la suite.

La plupart des applications de messagerie instantanée courantes ne disposent toujours pas d'une telle preuve, et certains outils populaires ne chiffrent même pas les messages de bout en bout. Un précédent rapport portait sur un outil de messagerie instantanée destiné aux consommateurs, qui envoie des SMS sans cette protection.