DeepMind vérifie formellement des garanties clés du protocole Signal

Google DeepMind a utilisé AlphaProof Code, un système d’IA dédié aux preuves mathématiques, pour vérifier plusieurs garanties de sécurité du protocole Signal, la couche cryptographique qui protège aussi WhatsApp et Google Messages. Selon Wired, l’étude a duré quatre semaines et n’a révélé aucune nouvelle vulnérabilité dans les parties examinées. L’enjeu dépasse Signal : la vérification formelle promet de prouver qu’un bug précis n’existe pas, au lieu de seulement le chercher. Pas exactement le genre de conclusion qui fait lever les bras au ciel, mais c’est une avancée sérieuse.

Une preuve mathématique, pas un simple test de plus

La vérification formelle consiste à démontrer par les maths qu’un logiciel respecte bien ses propriétés de départ. En théorie, cela évite de compter uniquement sur des tests qui, eux, peuvent passer à côté d’un défaut. En pratique, l’exercice reste lent, car il faut traduire les propriétés en formules, puis construire la preuve. DeepMind explique que ses agents automatisent une grande partie de cette dernière étape, tout en laissant des humains contrôler les points clés.

Le périmètre étudié reste étroit : AlphaProof Code n’a pas prouvé tout Signal, mais seulement certaines garanties cryptographiques du protocole. DeepMind a aussi testé l’outil sur d’anciennes versions connues pour contenir des vulnérabilités déjà corrigées. Résultat : le système les a bien signalées et a conclu que ces versions ne pouvaient pas être vérifiées, ce qui correspond au comportement attendu d’un vérificateur fiable.

Signal sert de banc d’essai, mais la méthode vise plus large

Signal n’est pas tombé dans l’angle mort de la vérification formelle par hasard. L’application a déjà intégré ce type de travail dans la conception de son post-quantum ratchet, avec l’aide de Cryspen, pour vérifier mécaniquement ses protocoles. Ehren Kret, chief technology officer de Signal, a déclaré : « While prior formal verification focused on smaller portions of the code, Google DeepMind’s approach enables significant expansion. As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code’s privacy guarantees. »

Du côté de DeepMind, Swarat Chaudhuri, research scientist, a résumé la philosophie du projet ainsi : « We don’t want this sort of vibe world where AI is generating the goals and AI is generating the proofs and basically taking tests that are self-written. There’s a middle ground. » Cette nuance compte, car l’automatisation totale reste loin d’être acquise. Le chercheur a aussi reconnu qu’il y a « a long distance to go » avant de viser « all the software of the world ».

Ce que Google ne dit pas encore sur le coût

Le travail a été mené gratuitement, dans le cadre d’un projet de recherche, et Google n’a pas indiqué ce que cela coûterait s’il fallait l’industrialiser. L’entreprise n’a pas non plus dit si elle entendait vendre la vérification formelle comme produit ou service. C’est souvent là que les belles promesses techniques rencontrent la feuille de prix, et la feuille de route.

Pour DeepMind, l’intérêt stratégique est clair : si l’IA peut aider à certifier des briques cryptographiques critiques, l’approche pourrait intéresser des banques, des éditeurs de logiciels ou des services manipulant des données sensibles. Pushmeet Kohli, vice president of research, l’a formulé ainsi : « If you can now verify the correctness of these implementations, then you can rest easy. You can imagine banks, imagine all those other companies who rely on assurances and who worry about bugs who could now say, ‘I can prove these properties.’ »

Une course à la cybersécurité plus large que Signal

Cette annonce arrive alors que plusieurs laboratoires d’IA tentent d’appliquer leurs modèles à la sécurité. OpenAI dit que GPT-6 Cyber a trouvé 81 failles cachées dans Firefox ; Google a donné à des défenseurs de la cybersécurité un accès anticipé à Gemini 4 Carbon ; Anthropic affirme de son côté que Claude a résolu une énigme cryptographique de la NSA vieille de 25 ans. Dans ce contexte, DeepMind mise sur une approche moins spectaculaire mais plus robuste : non pas seulement débusquer des bugs, mais prouver qu’une partie du code ne peut pas en contenir certains.

Reste la vraie question, la seule qui compte à terme pour le marché : est-ce que cette méthode peut s’étendre à des logiciels plus complexes, à grande échelle, et à un coût raisonnable ? Pour l’instant, DeepMind apporte une démonstration crédible sur un protocole déjà très étudié. Le saut vers le reste du logiciel mondial, lui, n’est pas encore écrit.