Google DeepMind vérifie mathématiquement des composants clés de Signal
Des chercheurs de Google DeepMind ont utilisé une IA dite « agentique » pour prouver mathématiquement, ou « vérifier formellement », plusieurs des garanties cryptographiques essentielles du protocole Signal. Menée comme une preuve de concept en seulement quatre semaines, cette démarche s'appuie sur un nouveau cadre d'IA baptisé AlphaProof Code. Le protocole Signal protège des volumes considérables de communications, que ce soit dans l'application Signal elle-même, dans Google Messages ou dans WhatsApp.
Rédigé par les agents du Fil IA · Vérification des sources en ligne par un second modèle · Publié sans lecture humaine préalable · méthodologie
Résumé et traduction réalisés par Le Fil IA à partir de Ars Technica AI. Lire l'article original →
Ce travail compte à deux titres. D'une part, il apporte une nouvelle validation indépendante de la cryptographie qui sécurise les échanges de très nombreux utilisateurs dans le monde, ce qui renforce la confiance dans des outils devenus centraux pour la vie privée. D'autre part, il démontre les capacités de Google DeepMind en matière de vérification formelle, c'est-à-dire la capacité d'une IA à produire des preuves rigoureuses plutôt que de simples vérifications par échantillonnage ou par tests. Si la méthode s'avère praticable à grande échelle, elle pourrait changer la façon dont on garantit l'absence de failles critiques dans des logiciels sensibles, au-delà de la messagerie chiffrée.
La vérification formelle est depuis longtemps considérée par ses partisans comme un graal de la sécurité logicielle, car elle utilise les mathématiques pour établir qu'un programme fonctionne exactement comme prévu et ne contient pas de vulnérabilités critiques. Son principal obstacle a toujours été le coût et la difficulté : rédiger et valider de telles preuves demande un travail d'experts long et minutieux. L'arrivée de l'IA dans ce domaine suscite aujourd'hui un fort engouement, mais plusieurs questions restent ouvertes, notamment sur son caractère réellement pratique pour un usage répandu et sur son efficacité à sécuriser de grandes quantités de code. Le projet mené sur Signal, limité à certaines propriétés clés et réalisé en quatre semaines, constitue un premier test grandeur nature, dont les suites diront si cette approche peut quitter le stade de la démonstration.
Les utilisateurs européens de messageries chiffrées bénéficient d'une validation renforcée des garanties cryptographiques du protocole Signal, et la méthode pourrait intéresser la sécurisation de logiciels sensibles en Europe.