DeepMind vérifie formellement le protocole Signal avec une IA

Des chercheurs de Google DeepMind ont utilisé un cadre d’IA agentique, AlphaProof Code, pour prouver mathématiquement plusieurs garanties cryptographiques clés du protocole Signal, selon Wired. Ce travail, une preuve de concept menée en quatre semaines, relève de la vérification formelle : une méthode qui utilise les mathématiques pour s’assurer qu’un logiciel fait bien ce qu’on attend de lui, au lieu de tester quelques cas.

Le protocole Signal est le schéma de chiffrement de l’application Signal et, comme le rappelle Wired, il protège aussi les communications de Google Messages et de WhatsApp. L’analyse est donc présentée comme une validation indépendante supplémentaire d’une cryptographie qui protège un très grand volume de messages. Wired y voit une étape majeure pour la cryptographie comme pour l’IA, tout en insistant sur la portée limitée du résultat.

Qu’est-ce que DeepMind a réellement prouvé ?

L’équipe a prouvé « un certain nombre » des garanties clés du protocole, pas toutes. Wired précise que l’analyse n’a pas vérifié formellement l’ensemble de l’application mobile Signal, et les chercheurs présentent leur résultat comme une étape dans un processus plus large. « Nous sommes très enthousiastes, mais il reste une longue distance avant de pouvoir appliquer cela à tous les logiciels du monde, et nous voulons le faire », a déclaré à Wired Swarat Chaudhuri, chercheur chez DeepMind.

Selon le même article, l’analyse n’a trouvé aucune nouvelle vulnérabilité dans les parties du protocole examinées. Les chercheurs ont aussi lancé AlphaProof Code sur d’anciennes versions de Signal contenant des vulnérabilités connues et corrigées depuis longtemps : l’outil les a correctement repérées et a montré que ces versions ne pouvaient pas être vérifiées formellement. Ce test compte, car il montre que la méthode peut échouer quand une faille existe, et pas seulement réussir quand il n’y en a pas.

• Outil : AlphaProof Code, un nouveau cadre d’IA agentique de Google DeepMind.
• Durée : quatre semaines, dans le cadre d’une preuve de concept.
• Résultat : garanties cryptographiques clés prouvées ; aucune nouvelle vulnérabilité dans les parties analysées.
• Anciennes versions : failles connues et corrigées détectées, protocole déclaré non vérifiable.
• Publication : la spécification et la preuve sont diffusées pour aider d’autres travaux de vérification formelle.
• Coût : non communiqué ; l’analyse a été menée gratuitement, comme projet de recherche.

Comment l’IA et les humains se sont-ils partagé le travail ?

Avant l’ère de l’IA, il fallait décrire les propriétés à prouver, les traduire en formules, puis construire la preuve. Wired explique que l’IA agentique peut réduire fortement le temps de cette dernière étape, ce qui a rendu possible l’évaluation de Signal en quatre semaines. Les chercheurs de DeepMind ajoutent qu’ils partaient avec une avance, car la Signal Foundation avait déjà mené des travaux de vérification formelle sur des portions plus petites du code.

Ehren Kret, directeur technique de Signal, a déclaré dans un communiqué cité par Wired : « Alors que les vérifications formelles précédentes portaient sur de plus petites parties du code, l’approche de Google DeepMind permet une extension significative. » Il ajoute que vérifier rigoureusement l’implémentation renforce la confiance de Signal dans les garanties de confidentialité de son code, alors que les menaces de sécurité liées à l’IA augmentent.

DeepMind présente comme avancée principale un « processus de collaboration humain-IA » : les agents contribuent et se corrigent presque à chaque phase, tandis que des humains relisent aux moments clés. « Nous ne voulons pas d’un monde où l’IA génère les objectifs et génère les preuves », a dit Chaudhuri. Une preuve formelle ne garantit que les propriétés qui ont été écrites, d’où l’importance de la relecture humaine de la spécification.

Un effort parallèle autour de Signal

Le travail de DeepMind n’est pas la seule tentative de prouver la cryptographie de Signal. La Beneficial AI Foundation, avec Rolfe Schmidt de Signal et le Lean FRO, a lancé « Signal Shot », un projet public visant à vérifier le protocole et son implémentation en Rust avec l’assistant de preuve Lean. Il prévoit de traduire le code Rust de Signal en Lean avec l’outil Aeneas, et liste des composants à vérifier, dont l’échange de clés post-quantique PQXDH, le Double Ratchet et le SPQR/Triple Ratchet. Wired ne relie pas cette initiative à celle de DeepMind : ce sont deux efforts distincts.

Qu’est-ce qui reste incertain ?

La question ouverte, note Wired, est de savoir si la vérification formelle automatisée par IA peut passer à l’échelle à un coût raisonnable. Google a refusé de communiquer le coût de l’analyse de Signal et de dire s’il prévoit un produit ou un service commercial de vérification formelle. Pushmeet Kohli, scientifique en chef de Google Cloud et vice-président de la recherche de DeepMind, imagine que des banques et d’autres entreprises inquiètes des bogues pourraient affirmer qu’elles peuvent prouver certaines propriétés de leurs logiciels. C’est une vision, pas une offre annoncée.

Ce que ça change pour les entreprises

Pour une entreprise qui choisit une messagerie ou construit sur le protocole Signal, le résultat est un signal rassurant sur la conception du protocole, pas un certificat pour chaque application qui l’utilise : l’application Signal complète n’a pas été vérifiée, et le déploiement, les serveurs et les réglages d’un produit restent hors de la preuve. La spécification et la preuve publiées offrent aux équipes de sécurité de la matière à étudier et à réutiliser. Le coût et toute offre commerciale étant inconnus, il ne faut pas encore compter sur cette approche pour vérifier formellement son propre code, mais on peut déjà demander aux fournisseurs de logiciels critiques quelles propriétés sont spécifiées et prouvées.