Une preuve qui descend jusqu’au programme compilé
Google DeepMind annonce le 10 novembre avoir utilisé AlphaProof Code pour démontrer certaines propriétés de sécurité de libsignal, l’implémentation de référence du protocole Signal. Le résultat porte sur le programme compilé en code machine, plutôt que seulement sur une description mathématique du protocole ou sur des fonctions isolées. C’est une étape importante : une conception peut être solide sur papier et être affaiblie par une erreur dans la façon dont le logiciel la réalise. L’équipe affirme qu’il s’agit de la première vérification formelle à cette profondeur d’un protocole cryptographique largement déployé. Signal est utilisé dans plusieurs services de messagerie, mais cette formulation ne signifie pas que les applications mobiles ont toutes été vérifiées. Les travaux portent sur une partie délimitée de la bibliothèque partagée et sur des garanties précises. Le mot « preuve » a donc ici un sens technique strict : un résultat mathématique vérifié dans un cadre défini, et non une certification générale de sécurité.
Six millions de lignes de preuve, avec des humains dans la boucle
AlphaProof Code répartit le travail entre agents. Des chercheurs et des modèles les aident à formuler les propriétés à établir; des agents de preuve produisent ensuite du code Lean, un langage où les démonstrations sont vérifiées mécaniquement. Pour ce cas, DeepMind rapporte environ 6,5 millions de lignes de preuve Lean, adossées à quelque 26 000 lignes de spécifications et de sémantique du processeur AArch64 qui forment la base de confiance. Ce ne sont pas six millions de lignes du logiciel Signal. Les agents ont travaillé sur libsignal v0.105.4, compilé avec Rust dans un petit programme de ligne de commande pour processeurs AArch64. La preuve couvre notamment l’établissement de session PQXDH et le Triple Ratchet, avec des propriétés de confidentialité passée, d’authentification et de sécurité après compromission. Les humains ont défini et révisé les spécifications; Lean vérifie les démonstrations produites. DeepMind dit que le travail a pris quatre semaines à une équipe de cinq personnes utilisant les agents en continu. Il ne s’agit donc pas d’une validation autonome lancée en quelques minutes.
Pourquoi regarder le code machine change la portée
La cryptographie d’un protocole ne se résume pas à quelques équations. Le logiciel doit aussi gérer un état de session, des messages reçus dans le désordre, le stockage temporaire de clés, les formats de données et les erreurs. Une faute dans ces détails peut annuler une protection théorique. Ici, les chercheurs ont relié le comportement du binaire compilé à leurs modèles et propriétés, en examinant également les opérations de gestion d’état couvertes par le programme étudié. Pour éprouver leur méthode, ils ont réintroduit dans des copies isolées deux bogues historiques déjà corrigés dans libsignal. Le système a alors démontré que les versions modifiées violaient les propriétés visées. C’est un test utile : les théorèmes réagissent à des défauts connus au lieu de simplement confirmer le programme choisi. Il ne mesure toutefois pas le taux de détection de toutes les vulnérabilités possibles. Les artefacts et les preuves sont publiés, ce qui permettra à d’autres spécialistes d’examiner les hypothèses et de refaire une partie du travail.
Une avancée réelle, avec un périmètre à garder en vue
Le résultat ne prouve pas que Signal est invulnérable. L’étude vérifie un programme de commande qui relie certaines fonctions de libsignal v0.105.4; elle ne couvre pas toutes les applications Signal, leurs interfaces, leurs serveurs, leurs systèmes d’exploitation, les conversations de groupe ni toutes les fonctions de la bibliothèque. La génération de clés n’est pas comprise dans les théorèmes décrits. Une preuve sur un binaire et un scénario ne se transpose pas automatiquement à une autre version ou à une autre compilation. La base de confiance compte aussi. Les spécifications doivent exprimer correctement les garanties attendues; la sémantique AArch64, le noyau Lean, certains contrats de fonctions cryptographiques et des hypothèses sur les primitives restent nécessaires. La publication distingue des modèles symboliques et computationnels, chacun avec ses limites. Par exemple, certains comportements de guérison post-quantique ne sont pas établis par les théorèmes computationnels présentés. Une démonstration formelle est donc une assurance forte sur des affirmations précises, sous des hypothèses précises, pas une preuve que toute attaque est impossible.
Ce que les équipes québécoises peuvent en retenir
Pour les organisations qui développent des logiciels sensibles, l’idée pratique n’est pas de demander à un agent conversationnel si le code est sûr. Il faut choisir une propriété vérifiable, écrire une spécification que des spécialistes peuvent examiner, puis vérifier indépendamment que le binaire livré correspond bien au programme analysé. Les équipes peuvent réserver cette approche aux composants dont une défaillance aurait un impact élevé : authentification, mise à jour sécurisée, gestion des clés ou fonctions critiques d’un appareil médical. Les essais d’intrusion, la revue de code et la réponse aux incidents restent nécessaires : ils cherchent d’autres catégories de défauts et couvrent souvent un périmètre différent. La leçon est plutôt que des agents peuvent aider à produire et à auditer une masse de preuves formelles jusque-là coûteuse à construire. Avant d’adopter ce type d’outil, une équipe devrait demander quelles affirmations sont démontrées, quelle part du système reste hors périmètre, quelles hypothèses sont accordées et si les artefacts peuvent être reproduits. L’avancée est notable; sa valeur dépendra de la transparence et de la vérification indépendante.
