DeepMind prouve mathématiquement la sécurité du code de Signal en 4 semaines au lieu de plusieurs années

Quiconque a écrit de la cryptographie connaît cette désagréable réalité : un protocole peut être brillamment démontré sur le papier, et la vulnérabilité se retrouver malgré tout dans le code. Entre le schéma et l'implémentation s'étend un gouffre, et c'est précisément là que vivent les vrais bogues. Google DeepMind affirme avoir appris à des agents IA à combler ce gouffre pour l'un des protocoles les plus importants au monde, celui qui protège les conversations dans Signal et Google Messages.

Ce qui a été fait exactement

Le système s'appelle AlphaProof Code. Il s'agit d'un framework multi-agents reposant sur plusieurs LLM, qui répartit le travail comme le ferait une équipe de recherche. D'abord, des experts humains traduisent, avec l'aide des modèles, les objectifs de sécurité de Signal en spécifications mathématiques formelles. Chaque spécification est vérifiée manuellement par un humain. Ensuite, les agents basés sur Gemini Carbon rédigent les preuves elles-mêmes dans le langage Lean, pour un total de plus de six millions de lignes.

Vient ensuite le point le plus pratique. Lean vérifie lui-même la validité de chaque preuve, il n'est donc pas nécessaire de faire une confiance aveugle au modèle : une conclusion erronée ne passera tout simplement pas la vérification. Les agents ont en outre audité le résultat et signalé les endroits nécessitant le regard d'un humain. Cela représente environ 1 % de la base de code. Les experts se sont concentrés sur ces passages plutôt que sur la relecture de millions de lignes.

Pourquoi ce n'est pas un audit de plus

La vérification formelle classique des protocoles s'arrête au niveau de la conception : on démontre que le schéma est sûr. Ici, les agents sont allés plus loin et ont prouvé des propriétés pour le code compilé, celui qui s'exécute sur les appareils. Par exemple, que les messages restent protégés avant et après une compromission temporaire d'un appareil.

Pour vérifier l'honnêteté du système, les auteurs ont mené un test simple. Dans une version isolée du code de Signal, ils ont réintroduit deux bogues réels, corrigés auparavant. Dans les deux cas, le système a produit une preuve vérifiable par machine que cette version n'était pas sûre. Autrement dit, l'outil distingue le code correct du code incorrect au lieu de tout « approuver » indistinctement.

Selon DeepMind, l'ensemble a pris quatre semaines, alors que de tels travaux demandaient traditionnellement des années à des équipes d'experts. Le directeur technique de Signal, Eren Kret, a qualifié de percée majeure la traduction automatique de code de production en théorèmes Lean.

Limites et enseignements pratiques

Il faut garder la mesure de l'ampleur. Il s'agit d'un seul protocole, étudié depuis longtemps et avec soin, et l'essentiel des chiffres annoncés repose sur les déclarations de DeepMind elle-même. Les humains n'ont pas été retirés du processus : la définition de ce qui est « sûr » reste fixée par des experts, et une erreur dans la spécification donne la preuve de la mauvaise chose. Les auteurs eux-mêmes reconnaissent que le passage à l'échelle nécessite des recherches supplémentaires. Les domaines annoncés, firmwares de dispositifs médicaux et logiciels pour les réseaux électriques, ne sont pour l'instant que des projets.

Que cela signifie-t-il pour les développeurs et les fondateurs ?

• Le duo « le LLM écrit, le vérificateur formel accepte ou rejette » est un schéma qui fonctionne pour les tâches où le coût d'une erreur est élevé. Le modèle a le droit de se tromper, le vérificateur non.
• Si vous développez de la cryptographie, de la logique de paiement ou du code embarqué critique, la vérification formelle cesse d'être l'apanage d'équipes académiques disposant d'un budget de plusieurs années.
• Savoir formuler des spécifications devient plus précieux que savoir écrire des preuves. Le goulot d'étranglement se déplace vers la question : « que voulons-nous garantir, au fond ? »

Autre point positif : DeepMind publie les artefacts de vérification. On peut les étudier et s'en servir de modèle pour ses propres expériences avec Lean et les agents. Avec des outils comme CodeMender, qui détectent et corrigent les vulnérabilités, les preuves formelles deviennent une composante du dispositif de défense ordinaire, et non plus une rareté académique.