AlphaProof Code vérifie des garanties cryptographiques de Signal jusque dans le code compilé
Des agents ont construit des preuves Lean sur une version compilée de libsignal. Les garanties concernent des composants précis du protocole.
Google DeepMind a présenté le 10 novembre AlphaProof Code. Son équipe a utilisé ce dispositif pour vérifier des propriétés de libsignal, la bibliothèque de référence du protocole Signal. Le rapport technique décrit des preuves portant sur une compilation AArch64 de code Rust non modifié. L’annonce de Google DeepMind situe le travail à quatre semaines et l’attribue à une collaboration entre chercheurs et agents.
Les chercheurs ont examiné deux parties du protocole. PQXDH sert à établir des secrets de départ pour une conversation. Triple Ratchet renouvelle les clés au fil des échanges. Les preuves portent notamment sur la confidentialité de la poignée de main et l’authentification. Elles couvrent aussi la protection des messages passés et des garanties de récupération après une compromission temporaire dans les conditions modélisées.
Le travail commence par la propriété à vérifier
Les chercheurs et des agents ont formulé en Lean les propriétés que le programme doit respecter. Les experts ont revu les spécifications. Cette étape détermine ce que les résultats signifient. Une vérification peut démontrer qu’un programme satisfait un énoncé précis. Il reste à établir que cet énoncé correspond à la protection que l’on cherche dans la pratique.
L’équipe a compilé la bibliothèque dans un petit programme en ligne de commande et utilisé une description formelle du jeu d’instructions AArch64. Le rapport fait état d’environ 6,5 millions de lignes de preuves Lean contrôlées par la machine. Les agents fondés sur Gemini Carbon ont produit des preuves. Le noyau de Lean les a vérifiées contre la spécification approuvée. Les preuves et spécifications publiées permettent de consulter les matériaux que les auteurs ont mis à disposition.
Deux anciennes failles comme contre-épreuve
Les chercheurs ont réintroduit séparément deux défauts déjà corrigés dans une copie isolée. Le dispositif a produit des preuves de l’insécurité des versions ainsi modifiées selon Google DeepMind. Ce contrôle permet de regarder si la méthode distingue au moins ces cas connus d’une version qui satisfait la propriété visée. L’enquête de WIRED précise que le travail a aussi bénéficié de vérifications antérieures menées par Signal.
Les frontières de la démonstration
Le cadre comprend des hypothèses sur les primitives cryptographiques et sur des fonctions appelées par le programme. La preuve dépend aussi du modèle de menace utilisé et de la description des instructions de la machine. Le rapport délimite donc un binaire et un ensemble de propriétés. Il ne donne pas une certification de toute l’application Signal ni des variantes du protocole dans d’autres messageries.
Le résultat met en lumière l’écart entre un protocole décrit sur le papier et le logiciel qui l’exécute. Un programme compilé doit se comporter comme le modèle de référence le prévoit y compris dans les situations couvertes où un adversaire intervient. Le travail fait le lien entre ces niveaux sur des portions de libsignal. Il ne suffit pas pour conclure à l’absence de tout défaut dans une application qui utilise cette bibliothèque.
Comme dans la formalisation de la preuve de Fermat par des agents Claude, Lean donne un moyen de contrôler un raisonnement produit par des agents. Ici le point difficile tient aussi à la traduction du comportement d’un programme réel et des capacités d’un attaquant en énoncés précis. La publication des preuves rend cette traduction examinable au-delà de la démonstration d’éditeur.