Signal : ce que l’IA a réellement prouvé sur son code

Google DeepMind affirme avoir utilisé AlphaProof Code pour prouver certaines propriétés du code compilé de libsignal. Le résultat éclaire le potentiel de l’IA, mais aussi les limites précises d’une preuve formelle.

Pour évaluer si un logiciel chiffre correctement les messages, il ne suffit pas de lancer des tests et d’observer son comportement dans quelques situations. Il faut aussi pouvoir établir, par un raisonnement vérifiable, que certaines propriétés tiennent dans toutes les exécutions couvertes par le modèle. Google DeepMind affirme avoir utilisé son système AlphaProof Code pour réaliser ce travail sur du code compilé du protocole Signal, avec des agents d’IA et le vérificateur de preuves Lean.

L’expérience porte sur des garanties cryptographiques précises, pas sur la sécurité absolue de l’application Signal. Elle montre surtout comment l’IA peut participer à une vérification formelle exigeante, en laissant des choix importants aux chercheurs et en confiant le contrôle mathématique final à un logiciel spécialisé.

Du modèle cryptographique au code exécuté

Un protocole de chiffrement décrit les règles permettant, par exemple, de protéger un échange et d’authentifier les interlocuteurs. Mais une conception correcte ne suffit pas : le programme qui la met en œuvre peut contenir une erreur. La vérification formelle cherche à établir mathématiquement que le code respecte des propriétés définies à l’avance, sous des hypothèses elles aussi explicites.

DeepMind indique avoir travaillé sur du code compilé de libsignal, la bibliothèque qui implémente le protocole Signal. Cette étape est importante : l’équipe ne s’est pas arrêtée à une description théorique du protocole, mais a cherché à relier des garanties de sécurité au code produit après compilation.

Le système, baptisé AlphaProof Code, répartit le travail entre plusieurs modèles et agents. Selon la description publiée par Google DeepMind, des chercheurs ont d’abord traduit les objectifs de sécurité en spécifications mathématiques, puis des agents alimentés par Gemini ont construit des preuves formelles. Le billet de DeepMind mentionne plus de six millions de lignes produites dans le langage Lean. Ce volume ne signifie pas que l’IA a écrit six millions de lignes de logiciel : il s’agit des artefacts servant à formaliser et à vérifier les démonstrations.

Ce que Lean vérifie, et ce que les chercheurs décident

Lean est un assistant de preuve. Il contrôle qu’une démonstration respecte les règles logiques du système et établit bien le résultat formulé. Il ne décide pas, à lui seul, si les propriétés choisies correspondent à toutes les attentes d’un utilisateur, ni si les hypothèses de départ décrivent correctement le monde réel.

Cette distinction est centrale. Les experts ont participé à la définition de ce qui devait être prouvé et ont relu les spécifications, selon DeepMind. Les agents ont ensuite exploré des pistes de démonstration, tandis que Lean vérifiait leur validité formelle. Le système peut ainsi réduire une partie du travail de recherche d’une preuve, mais le périmètre de la preuve reste un choix humain.

Une démonstration formelle n’est donc pas un audit universel. Si une propriété n’est pas incluse dans les spécifications, la preuve ne la couvre pas. Si une fonction cryptographique est tenue pour sûre sans que son implémentation soit vérifiée, cette hypothèse reste un maillon extérieur au résultat. La conclusion correcte est conditionnelle : le code satisfait les propriétés formalisées, dans le cadre défini et sous les hypothèses retenues.

Quatre semaines, deux bugs réintroduits

DeepMind annonce que l’expérience a duré quatre semaines. Pour tester si la méthode pouvait distinguer du code conforme d’une version défectueuse, l’équipe a aussi réintroduit deux bogues connus, corrigés auparavant, dans une version isolée du code. Selon l’entreprise, le système a alors produit des preuves vérifiées par machine montrant que ces variantes ne respectaient plus les garanties examinées.

Ce test est utile parce qu’il met la méthode face à des erreurs concrètes, au lieu de mesurer seulement sa capacité à produire une démonstration sur une version correcte. Mais il ne constitue pas un taux de détection généralisable : deux défauts réintroduits ne représentent ni toutes les catégories de vulnérabilités, ni tous les logiciels, ni toutes les façons dont un système pourrait échouer.

La frontière de la preuve reste précise

Les garanties examinées concernent le cœur cryptographique et des échanges individuels. Le périmètre décrit laisse de côté l’application dans son ensemble, les conversations de groupe et les usages sur plusieurs appareils. Elles ne constituent pas non plus une vérification de WhatsApp ou de Google Messages, même si ces services utilisent des éléments du protocole Signal. Une bibliothèque ou un protocole commun ne rend pas identiques les applications qui l’intègrent, leurs versions et leurs configurations.

La vérification ne signifie pas davantage qu’aucune vulnérabilité inconnue ne subsiste. Elle réduit l’incertitude sur des propriétés définies et sur le code inclus dans l’analyse. D’autres composants, les interfaces, les systèmes d’exploitation, la gestion des clés ou des fonctions laissées hors périmètre peuvent soulever des questions distinctes.

Pour les utilisateurs, l’intérêt immédiat est donc moins un nouveau réglage qu’une méthode de contrôle susceptible de rendre certaines garanties plus difficiles à contester ou à enfreindre par inadvertance. Pour les équipes qui conçoivent des logiciels critiques, l’enjeu est de savoir si des agents peuvent alléger le coût humain de preuves qui demandaient jusque-là un travail spécialisé important. DeepMind évoque des applications possibles à d’autres logiciels, mais la capacité à étendre cette approche à des systèmes plus vastes reste à démontrer.

Les spécifications et les preuves publiées par DeepMind donnent à d’autres spécialistes de quoi examiner et reproduire le travail. C’est cette possibilité de contrôle, associée à un périmètre clairement défini, qui permet de juger l’apport de l’IA : non pas une certification générale de « sécurité », mais une aide à établir certaines propriétés du code, avec des humains qui choisissent ce qui compte et un vérificateur formel qui contrôle la démonstration.