L'IA de DeepMind prouve que le code de chiffrement de Signal tient ses promesses

Google DeepMind affirme que ses agents d'IA ont prouvé mathématiquement que le code de chiffrement de Signal pour les conversations à deux tient ses principales promesses de sécurité. Ce travail, présenté le 10 novembre, repose sur un nouveau système baptisé AlphaProof Code et a porté sur le programme compilé lui-même, c'est-à-dire le code qui s'exécute réellement. Selon DeepMind, c'est la première fois que l'implémentation d'un protocole cryptographique aussi répandu est vérifiée formellement, avec ou sans IA. Aucune nouvelle faille n'a été trouvée dans les parties couvertes.

Ce qui a été prouvé

La vérification formelle consiste à écrire une propriété de sécurité sous forme d'énoncé mathématique et à prouver que le programme la respecte toujours, au lieu de le tester sur des exemples. La plupart des travaux sur des protocoles comme Signal s'arrêtent à leur conception. DeepMind est descendu jusqu'au code machine : l'équipe a pris libsignal en version 0.105.4 et la bibliothèque spqr, les a compilées pour Linux sur ARM 64 bits avec le compilateur Rust standard et a raisonné sur l'exécutable obtenu, précise la description technique.

Les chercheurs ont d'abord traduit, avec plusieurs modèles d'IA, les objectifs de sécurité de Signal en spécifications formelles, toutes relues par un humain. Des agents fondés sur Gemini Carbon ont ensuite écrit les preuves en Lean, un langage dont le vérificateur contrôle chaque étape automatiquement. Le résultat compte environ 6,5 millions de lignes. Les agents en ont signalé près de 1 % pour une relecture humaine, et le projet a duré quatre semaines. Parmi les dix théorèmes prouvés figurent la confidentialité persistante, qui protège les anciens messages si une clé fuit plus tard, et la sécurité post-compromission, qui rétablit la protection après le piratage temporaire d'un appareil.

Pour vérifier que le système distingue le bon code du mauvais, l'équipe a réintroduit deux vrais bugs de Signal, corrigés depuis longtemps, dans une copie isolée du code. Dans les deux cas, AlphaProof Code a produit une preuve vérifiée par la machine que la version boguée n'était pas sûre.

Ce qui reste hors de la preuve

La description détaille les limites. Les applications mobiles n'ont pas été vérifiées directement, et les auteurs s'attendent seulement à ce que les résultats s'y appliquent si elles exécutent le code du protocole sans modification. Les groupes sont renvoyés à des travaux futurs. Les canaux auxiliaires, comme les fuites par le temps d'exécution ou la consommation électrique, ne sont pas couverts, pas plus que la génération des clés et l'usage sur plusieurs appareils. Les preuves supposent aussi que les briques cryptographiques de base sont solides. Le directeur technique de Signal, Ehren Kret, a déclaré que ce travail « donne encore plus de confiance » dans les garanties de confidentialité du code.

Le blog de DeepMind cite Signal et Google Messages parmi les applications qui utilisent ce protocole. WhatsApp a adopté le protocole Signal il y a des années, mais la preuve porte sur le code libsignal de Signal et non sur le logiciel de WhatsApp, elle n'apprend donc rien de neuf sur WhatsApp. Le travail s'est en partie appuyé sur une vérification formelle antérieure de Signal réalisée sans IA. La méthode est aussi coûteuse : Google a indiqué à Wired qu'elle demande beaucoup de calcul, et le chercheur Swarat Chaudhuri a estimé qu'il reste « un long chemin à parcourir » avant de pouvoir l'appliquer à tous les logiciels du monde, rapporte 9to5Mac. DeepMind a publié les preuves sur GitHub pour que des experts extérieurs puissent les contrôler.