L’IA de Google DeepMind prouve les garanties de chiffrement de Signal

Des chercheurs de Google DeepMind, filiale d'Alphabet Inc. ↘ 0.21%, ont utilisé un nouveau cadre d'IA baptisé AlphaProof Code pour prouver mathématiquement plusieurs des principales garanties cryptographiques du protocole Signal. Ce projet de preuve de concept de quatre semaines n'a révélé aucune nouvelle vulnérabilité dans les parties du protocole examinées, a rapporté WIRED le 10 novembrewired.com. Le résultat dépasse le cadre de l'application Signal. Le protocole sécurise également les messages sur Google Messages et WhatsApp de Meta Platforms, Inc. ↗ 0.22%. Cette analyse constitue donc un contrôle indépendant supplémentaire du chiffrement qui protège une grande partie des communications mondiales, selon WIRED. Elle montre également que les agents d'IA peuvent accélérer la vérification formelle, une méthode longtemps recherchée mais lente consistant à utiliser les mathématiques pour démontrer que le logiciel se comporte comme prévuwired.com. ## Ce que l'analyse a révélé Les chercheurs ont testé AlphaProof Code sur d'anciennes versions de Signal contenant des vulnérabilités connues, corrigées depuis longtemps. L'outil a correctement identifié ces failles et a montré que ces versions ne pouvaient pas être formellement vérifiées, rapporte WIRED. DeepMind publie les spécifications et la preuve qu'il a construites afin que d'autres efforts de vérification puissent les utiliserwired.com. La portée était limitée. Le travail n'a pas vérifié l'intégralité de l'application mobile Signal, et les chercheurs l'ont décrit comme une étape dans un processus plus long. "Nous sommes très enthousiastes face à ce résultat, mais il reste un long chemin à parcourir avant de pouvoir étendre cela à tous les logiciels du monde, et c'est ce que nous voulons faire", a déclaré Swarat Chaudhuri, chercheur chez DeepMind, à WIREDwired.com. L'équipe a précisé que les travaux de vérification formelle antérieurs effectués par Signal leur avaient donné une longueur d'avance. "Alors que la vérification formelle précédente se concentrait sur de plus petites portions du code, l'approche de Google DeepMind permet une expansion significative", a déclaré Ehren Kret, directeur de la technologie chez Signal, dans un communiqué, ajoutant que cette vérification donne à l'entreprise "une confiance encore plus grande" face à la montée des menaces de sécurité liées à l'IAwired.com. ## Un domaine encombré Les travaux de DeepMind interviennent alors que d'autres groupes poursuivent des objectifs similaires. En avril 2026, Signal, la Beneficial AI Foundation et Lean FRO ont lancé Signal Shot, un effort public visant à vérifier le protocole Signal et son implémentation en Rust à l'aide de l'assistant de preuve Lean. Le projet vise à traduire le code réel de Signal en Lean et à prouver qu'il correspond à un modèle vérifié du protocole, selon la fondation. Le résultat de DeepMind est distinct de ce projet, a noté Startup Fortunebeneficialaifoundation.org+2. ## Questions en suspens sur le coût Il n'est pas encore clair si la vérification automatisée par IA peut être mise à l'échelle à un coût viable. DeepMind a réalisé l'analyse de Signal gratuitement en tant que projet de recherche. Google a refusé de préciser le coût ou s'il prévoyait un produit de vérification commercial, rapporte WIREDwired.com. Chaudhuri a souligné qu'une avancée clé résidait dans un processus où les agents d'IA contribuent et corrigent leur propre travail, tandis que des humains le révisent à des étapes cruciales. "Nous ne voulons pas de ce monde où l'IA génère les objectifs, génère les preuves et passe essentiellement des tests qu'elle a elle-même écrits", a-t-il déclaré. "Il existe un juste milieu"wired.com.