Google DeepMind a formellement vérifié des éléments clés du protocole Signal grâce à une IA agentique et à un nouveau cadre, AlphaProof Code. L'équipe publie ses preuves, sans avoir découvert de nouvelles failles, tout en reconnaissant des limites d'échelle et des inconnues sur la viabilité économique.
Coûts, produit commercial et passage à l’échelle restent incertains
La capacité d’une vérification formelle automatisée par l’IA à s’étendre à grande échelle et à un coût viable demeure une question ouverte dans le secteur technologique. DeepMind a réalisé gratuitement une analyse du protocole Signal dans le cadre d’un projet de recherche. Google a refusé de communiquer le coût de cette analyse et n’a pas souhaité préciser s’il envisageait un produit ou un service commercial de vérification formelle.
Une démarche human-in-the-loop revendiquée par DeepMind
Les chercheurs décrivent un processus de collaboration entre humains et IA, où des agents contribuent et s’auto-corrigent à presque chaque phase, tout en sollicitant l’intervention humaine à des moments clés. Swarat Chaudhuri, chercheur chez DeepMind, rejette l’idée d’un système où l’IA se fixe ses propres objectifs et génère ses preuves sans contrôle humain, préférant un équilibre entre autonomie de l’IA et supervision humaine. Avant l’IA, spécifier puis prouver formellement des propriétés logicielles était très chronophage pour les humains, et l’IA agentique permet de réduire ce temps. DeepMind précise toutefois que l’analyse ne couvre pas l’application mobile Signal dans son ensemble et présente ces résultats comme une étape d’un processus plus vaste, en soulignant que généraliser cette approche à tous les logiciels prendra du temps.
Vous suivez la course aux modèles IA ?
Chaque sortie (GPT, Claude, Gemini, Mistral…) décryptée le soir même, en 5 min. Gratuit.
Inclus dès l'inscription : notre sélection des meilleurs guides & comparatifs IA.
Choisissez votre rythme
Gratuit · Pas de spam · Désabonnement en 1 clic
Ce que DeepMind a vérifié, avec AlphaProof Code et en 4 semaines
DeepMind a utilisé une IA agentique pour vérifier formellement plusieurs garanties cryptographiques du protocole Signal. Réalisée en quatre semaines et basée sur le cadre AlphaProof Code, l’évaluation n’a révélé aucune vulnérabilité nouvelle dans les parties examinées. Sur d’anciennes versions de Signal contenant des failles connues et corrigées, l’outil a correctement identifié les problèmes, montrant que ces versions ne pouvaient pas être vérifiées formellement. Les chercheurs publient la spécification et la preuve développées pour soutenir d’autres travaux de vérification.
Pourquoi cela compte pour les messageries et au‑delà
Cette étape apporte une validation indépendante supplémentaire pour la cryptographie utilisée par des services comme Signal, Google Messages et WhatsApp. DeepMind indique avoir bénéficié de travaux antérieurs de vérification formelle menés par la Signal Foundation. Ehren Kret, directeur technique de Signal, souligne que les vérifications précédentes portaient sur des portions plus restreintes du code, tandis que l’approche de DeepMind permet une expansion significative et renforce la confiance dans les garanties de confidentialité alors que les menaces liées à l’IA augmentent. Les partisans de la vérification formelle la désignent fréquemment comme le « Saint Graal », puisqu’elle s’appuie sur des méthodes mathématiques afin de démontrer l’absence de failles critiques. Pour des services à fort enjeu, l’objectif optimal consisterait à appliquer la vérification formelle à chaque code source ainsi qu’à toutes les chaînes d’approvisionnement logicielles. Selon Pushmeet Kohli, scientifique en chef chez Google Cloud et vice-président de la recherche chez DeepMind, disposer d’une telle technologie pourrait apporter une garantie supplémentaire à des secteurs comme la banque, qui cherchent à démontrer certaines propriétés essentielles de leurs systèmes. Toutefois, l’industrialisation et l’efficacité à grande échelle de ces méthodes restent à établir.
