Google DeepMind affirme avoir utilisé AlphaProof Code pour vérifier mathématiquement des propriétés de sécurité clés de libsignal, l’implémentation de référence du protocole de messagerie Signal. Le travail a pris quatre semaines. Selon DeepMind, une vérification comparable mobilisait jusqu’ici des équipes d’experts pendant des années.
Le système associait des chercheurs humains à des agents d’IA. Ensemble, chercheurs et IA ont traduit les objectifs de sécurité de Signal en spécifications mathématiques, qui ont ensuite été examinées par des personnes. Les agents propulsés par Gemini Carbon ont alors généré environ 6,5 millions de lignes de code de preuve en Lean. Lean est un langage de programmation dont le vérificateur peut établir si une preuve mathématique respecte ses règles. Les agents ont signalé environ un pour cent de la base de code pour examen humain.
Que couvre la preuve ?
Les chercheurs ont vérifié le code machine compilé de la poignée de main post-quantique PQXDH et du Triple Ratchet de libsignal. Ils ont démontré certaines propriétés, notamment la confidentialité persistante, l’authentification et la protection après la compromission d’un appareil. L’article de recherche indique que le code a été compilé à partir de Rust non modifié avec un compilateur standard, puis vérifié sous forme de code machine AArch64.
Cette démarche va au-delà de la preuve qu’une conception abstraite est sécurisée : elle relie des garanties de sécurité spécifiées au code compilé. DeepMind la présente comme la première vérification formelle, à ce niveau de détail, de l’implémentation d’un protocole cryptographique largement déployé. L’équipe a également réintroduit deux bogues déjà corrigés dans une version isolée du code ; le système a produit des preuves montrant que les versions comportant ces bogues ne respectaient pas les propriétés de sécurité énoncées.
La preuve a ses limites
Il ne s’agit pas d’une garantie mathématique que chaque composant de Signal, ou chaque application utilisant le protocole, est exempt de problèmes de sécurité. La preuve porte sur certaines propriétés de libsignal, et non sur l’application dans son ensemble. Elle repose aussi sur des spécifications approuvées, le vérificateur de Lean et des contrats portant sur des routines cryptographiques de bas niveau. The Register souligne que le résultat ne prouve pas la confidentialité computationnelle des octets des messages réels ; l’article de DeepMind décrit des preuves dans des modèles symboliques et computationnels, qui reposent sur des hypothèses concernant les primitives cryptographiques sous-jacentes.
DeepMind indique qu’elle met les documents de vérification à la disposition d’autres équipes. Elle espère appliquer cette approche à des domaines comme les micrologiciels de dispositifs médicaux et les logiciels de réseaux électriques, mais précise qu’il faudra poursuivre les recherches pour l’étendre. Ce travail constitue une étape vers la vérification d’un plus grand nombre de logiciels utilisés dans le monde réel, mais ne signifie pas que ces autres systèmes ont été vérifiés.
Pourquoi c'est important
Pour les utilisateurs de Signal, ce travail apporte une preuve vérifiée par machine de propriétés de sécurité précises dans l’implémentation de base de son protocole. Il ne démontre pas que l’application entière est exempte de bogues, et la preuve repose sur des hypothèses concernant les composants cryptographiques.
