DeepMind vérifie des garanties de Signal avec l’IA

LLéna

Google DeepMind a utilisé son cadre d’intelligence artificielle agentique AlphaProof Code pour vérifier mathématiquement plusieurs garanties cryptographiques du protocole Signal, dans un travail mené en 4 semaines, selon Wired. Cette vérification formelle a porté sur des propriétés du protocole, et non sur l’application mobile dans son ensemble : elle n’a donc pas évalué chaque composant du logiciel utilisé pour communiquer sur Signal. Dans les parties étudiées, l’analyse n’a révélé aucune nouvelle vulnérabilité. Elle a en revanche détecté des problèmes dans d’anciennes versions de Signal, où des failles connues avaient été corrigées depuis ; AlphaProof Code a aussi montré que le protocole de ces versions ne pouvait pas être vérifié formellement. Le résultat ne signale donc pas de nouvelle faille dans les éléments examinés, mais montre que l’outil a pu repérer des problèmes déjà identifiés dans des versions antérieures. Ce travail s’est appuyé sur des recherches antérieures de la Signal Foundation consacrées à la vérification formelle. Google DeepMind publie la spécification et la preuve élaborées pour l’analyse, afin de soutenir d’autres travaux dans ce domaine et de permettre à d’autres chercheurs de s’en servir. La vérification porte ici sur plusieurs garanties précises, sans établir que toute l’application est exempte de vulnérabilités. Les chercheurs de DeepMind soulignent que l’extension de cette méthode à de grandes quantités de code reste incertaine et qu’il reste un long chemin avant de pouvoir l’appliquer à tous les logiciels. L’efficacité de cette approche à grande échelle reste donc à démontrer.