Le système a été baptisé AlphaProof Code.
Pendant quatre semaines, des équipes comptant jusqu’à 80 agents d’IA ont travaillé sans interruption sur les machines de cinq chercheurs de Google DeepMind, avec une mission précise, démontrer mathématiquement que le code qui chiffre les conversations Signal tient ses promesses de sécurité.
Google a dévoilé le résultat le 10 novembre 2026. Le travail porte sur libsignal, la bibliothèque qui met en œuvre le protocole de chiffrement de bout en bout de Signal, dont des variantes équipent aussi WhatsApp, Messenger et Google Messages.
Prouver plutôt que tester
D’ordinaire, on évalue la sécurité d’un logiciel en le testant, en l’auditant ou en y cherchant des failles, ce qui permet d’affirmer qu’aucun problème n’a été trouvé, sans garantir qu’il n’en existe aucun.
Mais il existe une autre approche, la vérification formelle.
Reposant sur des méthodes mathématiques, elle consiste à démontrer, comme on le ferait pour un théorème, que le code ne peut pas enfreindre certaines propriétés. Problème, la méthode est réputée extrêmement coûteuse. La vérification de seL4, un noyau de système d’exploitation dont des chercheurs australiens ont démontré formellement le bon fonctionnement en 2009, a par exemple demandé l’équivalent de vingt ans de travail pour une seule personne.
Et c’est à cela que s’est attaqué Google DeepMind avec AlphaProof Code.
Dans ce système, explique Google, « des experts humains travaillent avec l’IA pour décider de ce qu’il faut prouver, et un groupe d’agents IA s’en charge ».
Les chercheurs ont donc d’abord défini les propriétés à vérifier, en s’appuyant sur les travaux académiques consacrés à Signal. Les agents, fonctionnant eux avec le modèle Gemini 4 Carbon, ont ensuite rédigé environ 6,5 millions de lignes de démonstration dans le langage Lean, dont le vérificateur contrôle automatiquement chaque étape.
Aucun des chercheurs n’a écrit lui-même une ligne de preuve. « Nous avons décidé du périmètre et de l’ordre du travail, choisi les modèles de référence, guidé et approuvé les énoncés », résument-ils dans leur article technique.
Ce que Google a démontré
L’objectif principal était de prouver que le programme compilé de libsignal applique bel et bien le « ratchet », le mécanisme du protocole Signal qui renouvelle en permanence les clés de chiffrement au fil de la conversation, et qu’il en offre réellement les protections.
Ainsi, selon l’article technique, les preuves établissent qu’un attaquant parvenant à voler les clés stockées sur un téléphone ne pourrait pas pour autant lire les messages échangés auparavant, puisque chaque message est chiffré avec une clé dérivée de la précédente, puis effacée. Elles montrent aussi que la conversation redevient sûre dès que les deux interlocuteurs ont échangé de nouveaux messages, ceux-ci générant des clés neuves que l’attaquant ne connaît pas, et que personne ne peut se faire passer pour l’un des deux.
Pour vérifier que la méthode fonctionne, les chercheurs ont réintroduit deux anciens bugs de libsignal, corrigés depuis, et le système a démontré que ces versions n’offraient plus les garanties attendues.
Signal a réagi par la voix de son directeur technique Ehren Kret, qui a salué « une avancée majeure ».
Les équipes de Google ont tout de même tenu à mentionner les limites de ce travail de recherche. La preuve couvre uniquement les conversations à deux, et elle suppose que les briques cryptographiques de base fonctionnent parfaitement, sans les vérifier elles-mêmes. Elle porte aussi sur une version de test tournant sous Linux, et non sur les applications mobiles.
« Maintenant que les preuves deviennent bon marché, la question difficile devient de savoir quoi prouver » concluent les auteurs, qui en font la principale leçon de leur expérience.
Vous avez lu 0 articles sur Numerama ce mois-ci
Tout le monde n'a pas les moyens de payer pour l'information.
C'est pourquoi nous maintenons notre journalisme ouvert à tous.
Mais si vous le pouvez,
voici trois bonnes raisons de soutenir notre travail :
- 1 Numerama+ contribue à offrir une expérience gratuite à tous les lecteurs de Numerama.
- 2 Vous profiterez d'une lecture sans publicité, de nombreuses fonctions avancées de lecture et des contenus exclusifs.
- 3 Aider Numerama dans sa mission : comprendre le présent pour anticiper l'avenir.
Si vous croyez en un web gratuit et à une information de qualité accessible au plus grand nombre, rejoignez Numerama+.
Toute l'actu tech en un clin d'œil
Ajoutez Numerama à votre écran d'accueil et restez connectés au futur !
Tous nos articles sont aussi sur notre profil Google : suivez-nous pour ne rien manquer !