Google DeepMind utilise des agents d’IA pour vérifier le code machine central de Signal

Google DeepMind a présenté AlphaProof Code le 10 novembre 2026, en faisant appel à des équipes d’agents d’IA pour produire des preuves Lean vérifiées mécaniquement concernant des propriétés de sécurité spécifiées du code compilé de libsignal, le protocole de Signal. L’équipe de recherche, composée de cinq personnes, a réalisé ces travaux de preuve en quatre semaines et a publié ses spécifications et ses éléments de vérification afin qu’ils puissent être examinés par des tiers.

Les travaux sont allés au-delà d’un modèle abstrait de la conception du protocole de Signal pour porter sur son implémentation compilée. Les chercheurs ont intégré les crates libsignal v0.105.4 et SPQR v1.6.0, laissées intactes, dans un petit outil en ligne de commande, puis ont utilisé rustc standard pour créer un exécutable Linux AArch64 lié statiquement. L’article technique présente ce résultat comme les premières preuves de sécurité au niveau du protocole portant sur le code non modifié d’une implémentation de protocole cryptographique largement déployée.

Comment AlphaProof Code a réparti le travail

Cinq chercheurs ont consacré quatre semaines aux travaux de preuve, en faisant fonctionner les agents en continu sur leurs postes de travail tout en menant de front des preuves symboliques et computationnelles. Selon l’article, les agents ont généré environ 6,5 millions de lignes de code de preuve Lean vérifié mécaniquement, reposant sur quelque 26 000 lignes de spécifications fiables et de sémantique AArch64.

Les humains ont choisi les propriétés, levé les ambiguïtés et tranché les compromis en matière de sécurité, examiné les spécifications et conservé le pouvoir d’approbation final. Des agents s’appuyant sur Gemini 4 Carbon et Claude Opus 5.5 ont rédigé et examiné ces spécifications, y compris dans le cadre d’un examen mené par une autre famille de modèles. Des équipes d’agents Gemini 4 Carbon ont ensuite généré l’intégralité du code de preuve ; aucun des auteurs n’a écrit de code de preuve. Les campagnes habituelles mobilisaient de 40 à 80 agents sur une même machine pendant 24 à 72 heures. Un orchestrateur et des responsables d’équipe coordonnaient les agents chargés des preuves, tandis que des personnes assumant les rôles d’architecte et d’intégrateur entretenaient la base de preuves partagée.

Un mécanisme de contrôle n’acceptait une preuve qu’après vérification par le noyau de Lean et confirmation, par un comparateur, de sa conformité à la spécification mise de côté et approuvée par un humain, y compris à chacune de ses définitions transitives, en n’utilisant que les axiomes standard de Lean. Les agents pouvaient proposer de petites modifications lorsque les preuves révélaient des problèmes dans les spécifications, mais toute modification des hypothèses de confiance exigeait l’approbation d’un humain ou le respect d’une règle définie par l’utilisateur, et devait être consignée avec sa justification. Ce contrôle répond à un risque documenté des preuves générées par des agents : une spécification peut être affaiblie indirectement par l’intermédiaire de l’une de ses définitions.

Couverture de la sécurité et tests sur des bogues historiques

La cible vérifiée était le code des sessions individuelles, couvrant la poignée de main PQXDH et la messagerie Triple Ratchet. Les chercheurs font état de deux démonstrations indépendantes : dix théorèmes symboliques reposant sur des hypothèses cryptographiques idéalisées et une preuve computationnelle qui borne l’avantage d’un attaquant à l’aide d’hypothèses cryptographiques et de termes statistiques. Les propriétés couvertes comprennent la confidentialité persistante, qui protège les messages antérieurs en cas de vol de l’état actuel ; l’authentification ; la sécurité après compromission, qui concerne le rétablissement de la sécurité après une compromission ; et la confidentialité de la poignée de main. La démonstration symbolique couvre également la confidentialité de la poignée de main après une future rupture de Diffie–Hellman.

Pour vérifier si ces spécifications pouvaient détecter des erreurs réelles, l’équipe a annulé les correctifs de deux bogues de libsignal précédemment corrigés, connus sous les noms d’« état faible » et de « petit sous-groupe », puis a recompilé les binaires ainsi modifiés. Dans les deux cas, elle a produit des preuves Lean montrant que le théorème de sécurité symbolique était faux. Le dépôt public de vérification distingue les éléments computationnels, symboliques, binaires communs et relatifs à la sémantique AArch64, et explique comment reconstruire les preuves et les vérifier de manière indépendante.

Ehren Kret, directeur de la technologie chez Signal, a déclaré que ce travail « nous donne encore plus confiance dans les garanties de confidentialité de notre code ».

Limites et prochaines étapes

Ces garanties sont loin de certifier l’ensemble des applications de Signal. Elles portent sur la version de libsignal-cli des chercheurs, exécutée dans un processus neuf ; la génération des clés n’a pas été vérifiée, la messagerie de groupe a été laissée aux travaux futurs, et les canaux auxiliaires ainsi que l’état multiappareil ne sont pas couverts par le scénario. Les primitives cryptographiques de bas niveau et certaines routines de sortie et de bibliothèque sont représentées par des contrats de confiance. Le résultat dépend donc également de ces contrats, des spécifications approuvées, du noyau de Lean, de la sémantique AArch64 et des hypothèses relatives aux primitives.

L’article précise qu’aucune des deux démonstrations ne prouve le rétablissement post-quantique que SPQR est conçu pour apporter : le théorème computationnel couvre les attaquants classiques, tandis que les théorèmes symboliques sur le ratchet autorisent l’attaquant à choisir les clés SPQR. Le modèle computationnel restreint également plusieurs actions de l’attaquant et devient trivial lorsque le nombre de messages et de sessions atteint une échelle suffisamment grande. Ces limites définissent ce en quoi un examinateur externe doit avoir confiance avant de considérer les preuves vérifiées mécaniquement comme une garantie de sécurité pour un déploiement donné.

Les prochaines étapes annoncées par les chercheurs consistent à renforcer les théorèmes, à réduire la base de confiance en vérifiant davantage de routines raccordées et en reliant les contrats cryptographiques à des implémentations vérifiées, ainsi qu’à étendre la couverture à la messagerie de groupe, à l’expéditeur scellé et aux protocoles côté serveur. Leur objectif de vérifier les nouvelles versions de libsignal avant leur livraison relève de la recherche ; aucun déploiement n’a été annoncé.

Le résultat met immédiatement en évidence la répartition des tâches : les agents se sont chargés de construire les preuves, tandis que la garantie repose toujours sur des spécifications examinées par des humains et des hypothèses explicites. La publication des preuves et des procédures de vérification permet à des évaluateurs externes de mettre ces fondements à l’épreuve, tandis que les chercheurs s’emploient à intégrer ce processus au développement continu de libsignal.