AlphaProof Code a prouvé la correction du noyau de chiffrement de Signal en 4 semaines au lieu de plusieurs années

Les tests montrent que le code fonctionne sur les données d'entrée que vous avez songé à vérifier. Pour le chiffrement, cela ne suffit pas : un bug qui n'a pas été trouvé en cinq ans reste un bug. C'est pourquoi, dans les endroits les plus critiques, on recourt à la vérification formelle, c'est-à-dire à la preuve mathématique de la correction. Cela fonctionne, mais coûte cher : il faut de rares spécialistes et des années de travail. DeepMind affirme avoir trouvé un moyen de réduire fortement ce délai.

Ce que DeepMind a présenté

L'équipe a présenté AlphaProof Code, un système qui prouve, sans erreur, qu'un programme est conforme à sa spécification de sécurité. La démonstration a été réalisée sur le noyau du protocole de chiffrement de Signal. Selon les chercheurs Pushmeet Kohli et Swarat Chaudhuri, dans le blog de DeepMind, un tel travail prend habituellement des années, alors qu'ici quatre semaines ont suffi.

Il y a aussi une seconde différence. Les tentatives précédentes de vérification de Signal s'arrêtaient au niveau de la conception théorique : on prouvait que le protocole lui-même était correctement construit. AlphaProof Code a vérifié le véritable code cryptographique qui s'exécute sur les appareils des utilisateurs. Les erreurs les plus désagréables se cachent souvent entre un beau schéma et son implémentation, et c'est précisément cet écart qui a été comblé ici.

Comment cela fonctionne, sur un exemple simple

Imaginez une fonction qui additionne deux nombres. Un test vérifiera quelques dizaines de combinaisons. Une preuve en langage Lean fonctionne autrement : elle montre que le résultat est correct pour toutes les valeurs d'entrée, et Lean vérifie mécaniquement chaque étape. Si le raisonnement a une faille, il ne passe tout simplement pas la vérification.

Le processus se divise en deux étapes :

• D'abord, des experts humains formulent les exigences formelles de sécurité : ce que le code doit exactement garantir.
• Ensuite, des agents IA basés sur Gemini Carbon aident à mettre en forme les spécifications et prouvent indépendamment que le programme y est conforme.

Au total, les agents ont écrit plus de six millions de lignes en Lean. Le système a signalé environ 1 % de la base de code pour une vérification manuelle par des humains. Pour contrôler le dispositif, les chercheurs ont inséré deux erreurs dans le code, et les deux ont été détectées immédiatement. Le directeur technique de Signal, Eren Kret, affirme qu'une telle approche renforce la confiance dans la confidentialité des données face aux menaces croissantes liées à l'IA.

Ce qu'il faut garder à l'esprit

Premièrement : une preuve n'est valable que dans la mesure où la spécification l'est. Si les experts se sont trompés dans les exigences ou ont oublié une classe d'attaques, le système prouvera honnêtement la conformité à un objectif erroné. Le goulot d'étranglement se déplace de la rédaction des preuves vers la formulation des exigences, et cela ne supprime pas le rôle des humains.

Deuxièmement : il s'agit pour l'instant d'une démonstration sur un seul projet, présentée par le développeur lui-même. Le coût des calculs et la facilité à transposer la méthode à un autre langage et à une autre architecture ne sont pas précisés dans l'article. Nous n'avons pas vu d'évaluation indépendante du résultat.

Troisièmement : 1 % du code en relecture humaine semble modeste, mais il s'agit de cryptographie, où un seul fragment non vérifié peut dévaloriser tout le reste. Le marquage de ces zones fait partie de la méthode, pas de sa faiblesse.

Ce que cela signifie en pratique

Pour les développeurs, le signal principal est le suivant : on commence à automatiser la partie la plus coûteuse de la vérification, à savoir la rédaction des preuves. La capacité à formuler des exigences précises sur le code, par exemple des invariants et les limites du comportement admissible, sera plus précieuse que celle d'écrire des preuves à la main. Si vous travaillez avec la cryptographie, les paiements ou les protocoles, il vaut la peine de vous intéresser dès maintenant à Lean et aux outils similaires.

Pour les product managers et les fondateurs, c'est un nouvel argument de confiance. La phrase « le code est prouvé mathématiquement » est plus forte que « nous avons passé un audit ». Si le coût de la vérification passe réellement de plusieurs années à quelques semaines, cet argument deviendra accessible à d'autres que Signal.

DeepMind prévoit d'étendre la méthode aux réseaux électriques et aux dispositifs médicaux via des systèmes comme CodeMender. Le coût d'une erreur y est au moins aussi élevé que dans une messagerie, et les exigences y sont souvent plus strictes. Reste à voir si le résultat se reproduira sur d'autres projets et si des spécialistes indépendants le confirmeront.