Google DeepMind a annoncé le 10 novembre 2026 qu’un groupe d’agents d’intelligence artificielle avait vérifié des propriétés de sécurité du code de libsignal, la bibliothèque qui met en œuvre le protocole de chiffrement de Signal. Numerama rapporte que jusqu’à 80 agents ont travaillé pendant quatre semaines sur des machines utilisées par cinq chercheurs. Google baptise son système AlphaProof Code.
Le travail associe chercheurs et agents : les humains choisissent les garanties à démontrer et formulent les spécifications, puis les agents produisent les preuves. Google DeepMind indique que celles-ci représentent plus de six millions de lignes dans Lean, un langage dont le vérificateur contrôle automatiquement les étapes mathématiques. Les agents ont aussi signalé des passages à examiner par des humains, environ 1 % du code selon Google.
Quelles garanties ont été vérifiées ?
L’équipe a relié des propriétés du protocole au code compilé de libsignal. Les preuves portent notamment sur la confidentialité des anciens messages si les clés d’un téléphone sont volées, le retour à une communication protégée après l’échange de nouveaux messages, et l’authentification des interlocuteurs. The Register précise que le travail couvre le protocole PQXDH et le Triple Ratchet.
Pour éprouver la méthode, les chercheurs ont réintroduit deux bugs anciens, déjà corrigés dans libsignal. Dans les deux cas, le système a produit une preuve vérifiée par machine que la version modifiée ne respectait plus les garanties attendues. Google DeepMind dit avoir ouvert les éléments de vérification à la communauté.
Une preuve utile, mais limitée
Ce résultat ne constitue pas un audit de toutes les applications qui utilisent le protocole. Numerama souligne que la vérification porte sur une version de test sous Linux et sur les conversations entre deux personnes, pas sur les applications mobiles elles-mêmes. Elle suppose aussi que les briques cryptographiques de base fonctionnent correctement, sans les vérifier.
La méthode s’attaque à une difficulté ancienne : vérifier mathématiquement un logiciel demande souvent beaucoup de travail. The Register rappelle que la vérification formelle du noyau seL4 a demandé l’équivalent de vingt années de travail individuel. Les chercheurs estiment que l’IA peut réduire le coût des preuves ; reste à déterminer quelles propriétés formuler et vérifier, une étape qui dépend encore du jugement humain.
Pourquoi c'est important
Pour les utilisateurs de Signal, cette vérification apporte une assurance mathématique sur certaines propriétés du code de chiffrement, plutôt qu’un simple résultat de tests. Elle ne prouve toutefois pas que chaque version de l’application mobile est exempte de failles.
