Google DeepMind vérifie formellement la sécurité de Signal

Une méthode hybride

Les chercheurs ont d'abord utilisé divers modèles pour transformer les objectifs de sécurité de Signal en une spécification mathématique relue par des humains. Des agents Gemini Carbon ont ensuite généré du code Lean prouvant la correction de l'implémentation de libsignal. Ils ont produit 6,5 millions de lignes de Lean, puis une passe d'audit a signalé les éléments nécessitant une relecture humaine.

Le résultat reste théorique : il suppose une cryptographie parfaite et ne garantit pas le secret computationnel des octets. Il constitue néanmoins une assertion de correction significative, et un pas vers le défi lancé en avril par la Beneficial AI Foundation : vérifier formellement le protocole et l'application Signal avec Lean.

Un coût en forte baisse

La vérification formelle exigeait jusqu'ici des efforts considérables : 20 années-personnes pour le micronoyau seL4, six ans pour le compilateur C vérifié CompCert. Le travail sur Signal a pris quatre semaines à cinq personnes, avec « pas mal de jetons », selon l'article des chercheurs.

Pour Swarat Chaudhuri, de Google DeepMind, la vérification passe désormais à l'échelle ; la vraie question est de savoir quoi vérifier, un processus qui garde l'humain dans la boucle. Face à la montée des capacités offensives de l'IA, l'étape suivante consiste à appliquer la technique dès la conception de tout logiciel. « La prochaine frontière, ce n'est pas la preuve mais la spécification », estime-t-il.