Vitalik : Quelle est la clé de la prochaine phase d'Ethereum ?

Auteur : Vitalik Buterin

Traduit par : Jiahua, ChainCatcher

Un merci tout particulier à Yoichi Hirai, Justin Drake, Nadim Kobeissi et Alex Hicks pour leurs commentaires et leur relecture.

Ces derniers mois, un nouveau paradigme de programmation a rapidement gagné en popularité au sein des cercles de développement d'Ethereum et dans de nombreux autres secteurs de l'informatique : écrire du code directement dans des langages de très bas niveau (tels que le bytecode EVM, le langage assembleur) ou en Lean, et utiliser des preuves mathématiques automatiquement vérifiables écrites en Lean pour en valider l'exactitude.

Si elle est correctement mise en œuvre, cette approche a non seulement le potentiel de produire un code extrêmement efficace, mais elle est également beaucoup plus sûre que les méthodes de programmation précédentes. Yoichi Hirai la qualifie de « forme ultime de développement logiciel ».

Cet article tentera de dévoiler les principes sous-jacents, d'explorer ce que la vérification formelle des logiciels peut accomplir et d'identifier ses faiblesses et ses limites dans Ethereum et d'autres domaines.

Qu'est-ce que la vérification formelle ?

La vérification formelle désigne le processus de rédaction des démonstrations de théorèmes mathématiques de manière à ce qu'elles puissent être vérifiées automatiquement. Pour illustrer cela par un exemple relativement simple mais intéressant, prenons un théorème fondamental concernant la suite de Fibonacci : un nombre sur trois est pair, les autres étant impairs.

1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 …

Une manière simple de le prouver consiste à utiliser le raisonnement par récurrence, en avançant de trois étapes à la fois.

Le premier cas est celui de base. Soit F1 = F2 = 1, F3 = 2. Par observation, on constate que l'affirmation (« Fi est pair lorsque i est un multiple de 3, sinon il est impair ») est vraie avant x = 3.

Vient ensuite le cas inductif. Supposons que l'énoncé soit vrai avant 3k+3, c'est-à-dire que nous savons déjà que la parité de F3k+1, F3k+2 et F3k+3 est respectivement impaire, impaire et paire. Nous pouvons alors calculer la parité du groupe de trois nombres suivant :

F3k+4 = F3k+2 + F3k+3 = impair + pair = impair

F3k+5 = F3k+3 + F3k+4 = pair + impair = impair

F3k+6 = F3k+4 + F3k+5 = impair + impair = pair

Ainsi, sachant que l'énoncé est vrai avant 3k+3, nous en déduisons qu'il est vrai avant 3k+6. Nous pouvons appliquer ce raisonnement à plusieurs reprises, nous assurant ainsi que cette règle est valable pour tous les entiers.

Cet argument suffit à convaincre les humains. Mais que faire si l'on veut prouver quelque chose de cent fois plus complexe, et être absolument certain de ne pas s'être trompé ? Dans ce cas, il est possible de fournir une preuve convaincante pour un ordinateur.

Voici comment cela se présente :

-- La suite de Fibonacci avec fib 0 = 0, fib 1 = 1, fib 2 = 1 (indices décalés de 1)

def fib : Nat → Nat

| 0 => 0

| 1 => 1

| n + 2 => fib (n + 1) + fib n

-- Affirmation : fib (3k+1) est impair, fib (3k+2) est impair, fib (3k+3) est pair.

-- De manière équivalente : chaque troisième nombre de Fibonacci à partir de fib 3 est pair.

-- Nous prouvons les trois simultanément par récurrence sur k, puisque chaque cas

-- du bloc suivant est construit à partir du bloc précédent.

théorème fib_triple (k : Nat) :

fib (3 * k + 1) % 2 = 1 ∧

fib (3 * k + 2) % 2 = 1 ∧

fib (3 * k + 3) % 2 = 0 := par

induction k avec

| zéro => décider

| suc k ih =>

-- Réécrivez les nouveaux indices sous la forme (quelque chose) + 2 pour que fib se déroule.

affiner ⟨?_, ?_, ?_⟩

· afficher (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1

oméga

· afficher (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1

oméga

· afficher (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)

+ (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0

oméga

Il s'agit du même raisonnement, mais exprimé en Lean. Lean est un langage de programmation couramment utilisé pour écrire et vérifier des démonstrations mathématiques.

Cela diffère à juste titre de la preuve « humaine » donnée ci-dessus : ce qui est intuitif pour un ordinateur (au sens traditionnel du terme « ordinateur », c’est-à-dire un programme « déterministe » composé d’instructions si/alors, plutôt que de grands modèles de langage) est fondamentalement différent de ce qui est intuitif pour les humains.

Dans la preuve ci-dessus, vous n'avez pas souligné le fait que fib(3k+4) = fib(3k+3) + fib(3k+2), mais plutôt souligné que fib(3k+3) + fib(3k+2) est impair, alors qu'une stratégie dans Lean appelée omega combine automatiquement cela avec sa connaissance de la définition de fib(3k+4).

Dans les démonstrations plus complexes, il faut parfois indiquer explicitement quelle loi mathématique permet d'effectuer l'étape en cours, et parfois utiliser des noms obscurs comme Prod.mk.inj.

En revanche, vous pouvez développer d'énormes expressions polynomiales en une seule étape et prouver leur validité avec une simple expression comme « omega » ou « ring ».

Ce caractère contre-intuitif et complexe explique en grande partie pourquoi, malgré l'existence de preuves vérifiables par machine depuis près de 60 ans, le domaine reste confidentiel. Cependant, grâce au développement rapide de l'intelligence artificielle, de nombreuses choses autrefois impossibles deviennent désormais rapidement possibles.

Quand les preuves mathématiques commencent à protéger le code

Jusqu'ici, vous vous dites peut-être : eh bien, les ordinateurs peuvent vérifier les démonstrations de théorèmes mathématiques, donc nous pouvons enfin déterminer quelles nouvelles conclusions farfelues sur les nombres premiers sont vraies et lesquelles ne sont que des erreurs dans des articles PDF de cent pages.

Peut-être pourrons-nous même déterminer si les opinions de Shinichi Mochizuki sur la conjecture ABC sont correctes !

Mais, curiosité mise à part, et alors ?

Il existe de nombreuses réponses possibles. Mais l'une des plus importantes à mes yeux est la vérification de l'exactitude des programmes informatiques, notamment ceux qui effectuent des tâches cryptographiques ou liées à la sécurité.

Après tout, les programmes informatiques sont des objets mathématiques, donc prouver qu'un programme informatique s'exécute d'une certaine manière constitue en soi un théorème mathématique.

Par exemple, supposons que vous souhaitiez prouver si un logiciel de communication chiffrée comme Signal est réellement sécurisé. Vous pouvez définir mathématiquement ce que signifie « sécurisé » dans ce contexte.

En résumé, vous démontrez que, sous certaines hypothèses cryptographiques, seuls ceux qui possèdent la clé privée peuvent connaître le contenu du message. En réalité, de nombreuses autres propriétés de sécurité sont cruciales.

Il s'avère qu'une équipe travaille effectivement à résoudre ce problème ! L'un de leurs théorèmes de sécurité se présente ainsi :

théorème passif_secret_le_ddh

(g : G)

(adv : PassiveAdversary G SK) :

passifSecrecyAdvantage (F := F) g adv ≤

ProbComp.boolDistAdvantage

(DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))

(DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))

Voici un résumé de sa signification selon Leanstral :

Le théorème passivesecrecyle_ddh est une réduction compacte démontrant que la confidentialité passive des messages X3DH est au moins aussi difficile à compromettre que l'hypothèse DDH dans le modèle de l'oracle aléatoire. Si un adversaire parvient à compromettre la confidentialité passive des messages X3DH, il peut également compromettre DDH.

Puisque l'on suppose que DDH est difficile à casser, X3DH est également protégé contre les attaques passives. Ce théorème démontre que si un adversaire peut observer passivement les messages d'échange de clés de Signal, il ne peut distinguer la clé de session produite d'une clé aléatoire avec une probabilité non négligeable.

Si vous combinez cela avec une preuve correcte de l'implémentation du chiffrement AES, vous obtenez la preuve que le chiffrement du protocole Signal est sécurisé contre les attaques passives.

Des projets similaires ont également prouvé que les implémentations de TLS et d'autres éléments de la cryptographie interne au navigateur sont sécurisées.

Si vous effectuez une vérification formelle complète de bout en bout, vous prouvez non seulement qu'une description théorique du protocole est sécurisée, mais aussi que le code spécifique exécuté par les utilisateurs est également sécurisé en pratique.

Du point de vue de l'utilisateur, cela renforce considérablement la méfiance : pour faire pleinement confiance au code, il n'est pas nécessaire de vérifier l'intégralité du code source ; il suffit de vérifier les affirmations le concernant qui ont été prouvées.

Il convient toutefois de garder à l'esprit quelques mises en garde importantes, notamment concernant la signification concrète du mot « sécurisé », qui revêt une importance capitale.

Il est facile d'oublier de démontrer ces affirmations pourtant essentielles. Il est facile de constater que, parfois, les affirmations à démontrer ne sont pas plus simples à décrire que le code lui-même.

Il est facile d'introduire par inadvertance dans la démonstration des hypothèses qui, au final, s'avèrent erronées. Il est également facile de décider qu'une seule partie du système nécessite une démonstration formelle, pour ensuite découvrir de graves vulnérabilités dans d'autres parties (voire au niveau matériel).

Même l'implémentation Lean elle-même peut comporter des bogues. Mais avant d'aborder tous ces détails fastidieux, penchons-nous d'abord sur l'utopie qui pourrait résulter d'une vérification formelle correctement et idéalement menée à bien.

Vérification formelle conçue pour la sécurité

Les bugs dans les codes informatiques sont terrifiants.

Lorsque vous intégrez des cryptomonnaies dans des contrats intelligents à chaîne immuable, et que la Corée du Nord peut automatiquement vider vos comptes en cas de bug dans le code sans que vous ayez aucun recours, les bugs dans le code deviennent encore plus terrifiants.

Lorsque tout cela est enveloppé dans des preuves à divulgation nulle de connaissance, les bugs deviennent encore plus terrifiants car si quelqu'un parvient à pirater le système de preuves à divulgation nulle de connaissance, il peut extraire tout l'argent, et nous n'avons aucune idée de ce qui s'est mal passé (pire encore, nous ne savons même pas quand cela s'est produit).

Lorsque nous disposerons, d'ici deux ans, de puissants modèles d'IA, comme celui de Claude Mythos, capables de détecter automatiquement ces bugs, les bogues dans le code deviendront encore plus terrifiants.

Face à cette réalité, certains préconisent d'abandonner le principe même des contrats intelligents, allant jusqu'à croire qu'Internet ne peut être un domaine où les défenseurs peuvent avoir un avantage asymétrique sur les attaquants.

Quelques citations :

Pour renforcer la sécurité d'un système, il faut dépenser plus de jetons que l'attaquant n'en utilise pour exploiter les vulnérabilités.

Et:

Notre secteur repose sur un code déterministe. On l'écrit, on le teste, on le déploie, on est sûr qu'il fonctionne, mais d'après mon expérience, ce contrat est en train de se rompre.

Parmi les principaux opérateurs d'entreprises véritablement natives de l'IA, le code source est devenu un élément auquel on « fait confiance » pour son exécution, et il n'est plus possible de spécifier précisément sa probabilité de succès.

Pire encore, certains pensent que la seule solution est d'abandonner l'open source.

Pour la cybersécurité, cela augure d'un avenir sombre. Et pour ceux d'entre nous qui attachent de l'importance à la décentralisation et à la liberté d'Internet, c'est une perspective extrêmement pessimiste.

L'esprit cypherpunk tout entier repose fondamentalement sur l'idée que sur Internet, les défenseurs ont l'avantage, et que construire un « château » numérique (que ce soit par le biais du chiffrement, des signatures ou des preuves) est beaucoup plus facile que d'en détruire un.

Si nous perdons cela, la sécurité d'Internet ne pourra provenir que d'économies d'échelle, de la traque des attaquants potentiels dans le monde entier et, plus largement, ne pourra se résumer qu'à un choix entre domination et destruction.

Je ne suis pas d'accord ; j'ai une vision plus optimiste de l'avenir de la cybersécurité.

Je crois que les défis posés par les puissantes capacités de détection de vulnérabilités de l'IA sont considérables, mais qu'il s'agit d'un défi transitoire. Une fois la situation stabilisée et un nouvel équilibre atteint, l'environnement sera plus favorable aux défenseurs qu'auparavant.

Mozilla partage mon avis. Pour les citer :

Vous devrez peut-être revoir vos priorités et consacrer une énergie soutenue et concentrée à cette tâche, mais il y a de l'espoir au bout du tunnel.

Nous sommes très fiers de la façon dont notre équipe relève ce défi, et d'autres le seront aussi. Notre travail n'est pas terminé, mais nous avons surmonté la tempête et entrevoyons un avenir non seulement à la hauteur, mais bien meilleur.

Les défenseurs ont enfin l'occasion de l'emporter de façon décisive. … Les défauts sont limités, et nous entrons dans un monde où nous pourrons enfin tous les déceler.

Si vous recherchez les mots « formel » et « vérification » dans l’article de Mozilla à l’aide de Ctrl+F, vous ne trouverez aucun résultat. L’avenir positif de la cybersécurité ne repose pas entièrement sur la vérification formelle ni sur aucune autre technologie en particulier.

De quoi cela dépend-il ? Essentiellement, de ce graphique :

Évolution des vulnérabilités CVE au fil du temps

Depuis des décennies, de nombreuses technologies ont contribué à la diminution du nombre de vulnérabilités :

Systèmes de types

Langues à sécurité mémoire

Améliorations de l'architecture logicielle (notamment le sandboxing, le contrôle des permissions et, plus largement, la distinction entre « base informatique de confiance » et « autre code »)

de meilleures méthodes de test

Une base de connaissances en constante expansion sur les modèles de codage sécurisés et non sécurisés

Un nombre croissant de bibliothèques logicielles pré-écrites et auditées

La vérification formelle assistée par l'IA ne doit pas être considérée comme un paradigme entièrement nouveau, mais plutôt comme un puissant accélérateur de tendances et de paradigmes déjà en cours.

La vérification formelle n'est pas une solution miracle. Elle est cependant particulièrement adaptée aux situations où l'objectif est bien plus simple que la mise en œuvre. C'est notamment le cas pour certaines technologies extrêmement complexes et délicates que nous devrons déployer lors de la prochaine itération majeure d'Ethereum : les signatures résistantes à l'informatique quantique, les STARK, les algorithmes de consensus et les ZK-EVM.

STARK est un logiciel très complexe. Mais les propriétés de sécurité fondamentales qu'il implémente sont faciles à comprendre et à formaliser : si vous voyez un hachage H pointant vers le programme P, l'entrée x et la sortie y, alors soit (i) l'algorithme de hachage utilisé dans STARK a été cassé, soit (ii) P(x) = y.

Nous avons donc le projet Arklib, qui tente de créer une implémentation STARK entièrement vérifiée formellement (voir VCV-io, qui fournit l'infrastructure de calcul oracle fondamentale pour la vérification formelle de divers autres protocoles cryptographiques, dont beaucoup sont des dépendances de STARK).

Plus ambitieusement encore, il y a evm-asm : un projet visant à construire une implémentation EVM complète et formellement vérifiée.

Les propriétés de sécurité ne sont pas aussi simples ici : l’objectif est essentiellement de prouver son équivalence avec une autre implémentation EVM écrite en Lean, même si cette implémentation peut être écrite pour maximiser l’intuitivité et la lisibilité sans tenir compte de l’efficacité d’exécution spécifique.

Il est possible que nous obtenions dix implémentations d'EVM, toutes prouvées équivalentes, et qu'elles contiennent toutes la même faille fatale permettant à un attaquant de vider les ETH des adresses auxquelles il n'est pas autorisé à accéder.

Mais cette hypothèse est bien moins probable que l'existence de telles failles dans certaines implémentations actuelles de l'EVM. Une autre propriété de sécurité dont nous n'avons compris l'importance qu'après de douloureuses expériences, à savoir la résistance aux attaques par déni de service (DoS), est également facile à formaliser.

Deux autres domaines importants sont :

Consensus tolérant aux pannes byzantines. Formaliser l'ensemble des propriétés de sécurité attendues s'avère tout aussi complexe, mais compte tenu de la fréquence des bogues, cela mérite d'être tenté. C'est pourquoi nous développons actuellement des implémentations Lean et des preuves de protocoles de consensus en Lean.

Langages de programmation de contrats intelligents : voir la vérification formelle dans Vyper et Verity.

Dans tous ces cas, l'un des principaux avantages de la vérification formelle réside dans le fait que ces preuves sont véritablement complètes. Généralement, les bogues les plus gênants sont des bogues d'interaction qui se cachent à l'interface de deux sous-systèmes considérés indépendamment.

Pour les humains, raisonner sur l'ensemble du système de bout en bout est trop difficile. Mais les systèmes automatisés de vérification des règles peuvent le faire.

La vérification formelle, conçue pour l'efficacité

Examinons de plus près evm-asm. Il s'agit d'une implémentation EVM, mais écrite directement en assembleur RISC-V.

Authentique.

Voici le code d'opération ADD :

importer EvmAsm.Rv64.Program

espace de noms EvmAsm.Evm64

ouvrir EvmAsm.Rv64

/-- ADD EVM 256 bits : binaire, retire 2, empile 1.

Membre 0 : LD, LD, ADD, SLTU (transport), SD (5 instructions).

Membres 1-3 : LD, LD, ADD, SLTU (carry1), ADD (carryIn), SLTU (carry2), OU (carryOut), SD (8 chacun).

Puis ADDI sp, sp, 32.

Registres : x12=sp, x7=acc, x6=opérande, x5=retenue, x11=retenue1.-/

def evm_add : Programme :=

-- Membre 0 (5 instructions)

LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;

AJOUTER .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;

-- Membre 1 (8 instructions)

LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;

AJOUTER .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

AJOUTER .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

OU' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;

-- Membre 2 (8 instructions)

LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;

AJOUTER .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

AJOUTER .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

OU' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;

-- Membre 3 (8 instructions)

LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;

AJOUTER .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

AJOUTER .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

OU' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;

-- réglage sp

ADDI .x12 .x12 32

fin EvmAsm.Evm64

Le choix de RISC-V s'explique par le fait que les démonstrateurs ZK-EVM développés fonctionnent généralement en prouvant du code RISC-V et en compilant les clients Ethereum pour RISC-V. Par conséquent, si vous disposez d'une implémentation EVM écrite directement en RISC-V, il s'agit de l'implémentation la plus rapide disponible.

RISC-V peut également être simulé très efficacement sur des ordinateurs ordinaires (et il existe des ordinateurs portables RISC-V disponibles sur le marché).

Bien sûr, pour parvenir à une vérification de bout en bout, il faut vérifier formellement l'implémentation de RISC-V elle-même (ou l'arithmétique du démonstrateur), mais ne vous inquiétez pas, des travaux existent déjà dans ce domaine.

Écrire du code directement en assembleur est une pratique courante il y a cinquante ans. Depuis, nous avons abandonné cette pratique au profit des langages de haut niveau.

Les langages de haut niveau font des compromis sur l'efficacité, mais en contrepartie, ils permettent un codage beaucoup plus rapide et, plus important encore, une compréhension beaucoup plus rapide du code des autres, ce qui est essentiel pour la sécurité.

Grâce à la combinaison de la vérification formelle et de l'intelligence artificielle, nous avons la possibilité de « retourner vers le futur ».

Plus précisément, nous pouvons faire en sorte qu'une IA écrive du code assembleur, puis qu'elle rédige une preuve formelle pour vérifier que ce code assembleur possède les propriétés souhaitées.

À tout le moins, les propriétés souhaitées peuvent simplement correspondre à une équivalence parfaite avec une implémentation optimisée pour la lisibilité et écrite dans un langage de haut niveau convivial.

Nous n'avons plus besoin d'un seul objet de code pour équilibrer lisibilité et efficacité ; nous avons désormais deux objets indépendants : l'un (l'implémentation en assembleur) optimisé uniquement pour l'efficacité tout en tenant compte des exigences de son environnement d'exécution spécifique ; l'autre (la déclaration de sécurité ou l'implémentation en langage de haut niveau) optimisé uniquement pour la lisibilité, et nous prouvons ensuite l'équivalence entre les deux par une démonstration mathématique.

Les utilisateurs peuvent vérifier (automatiquement) cette preuve une seule fois, et à partir de ce moment-là, ils n'ont plus qu'à exécuter la version rapide.

Cette approche est incroyablement puissante, et ce n'est pas par hasard que Yoichi Hirai la qualifie de « forme ultime de développement logiciel ».

La vérification formelle n'est pas une solution miracle.

Dans les domaines de la cryptographie et de l'informatique, il existe une tradition presque aussi ancienne que l'histoire des méthodes formelles elle-même : la tradition de critiquer les méthodes formelles (ou plus largement, le recours aux « preuves »).

Ces écrits regorgent d'exemples concrets. Commençons par les preuves manuscrites des débuts de la cryptographie rudimentaire, en citant les critiques de Menezes et Koblitz de 2004 :

En 1979, Rabin a proposé une fonction cryptographique qui était «prouvablement» sûre dans un certain sens, c'est-à-dire qu'elle possédait une propriété de sécurité réductionniste.

L'énoncé de sécurité réductionniste indique que quiconque peut trouver le message m à partir du texte chiffré y doit également être capable de factoriser n. … Peu de temps après que Rabin ait proposé son schéma de chiffrement, Rivest a souligné que, paradoxalement, cette caractéristique même qui lui confère une sécurité supplémentaire conduirait à un effondrement complet face à un attaquant connu sous le nom de « texte chiffré choisi ».

Autrement dit, si l'attaquant parvient d'une manière ou d'une autre à tromper Alice pour qu'elle déchiffre le texte chiffré qu'il a choisi, alors l'attaquant peut suivre les mêmes étapes que Sam a utilisées dans le paragraphe précédent pour factoriser n.

Menezes et Koblitz ont ensuite fourni d'autres exemples. Le constat est le suivant : les conceptions visant à rendre les protocoles de chiffrement plus « vérifiables » les rendent souvent moins « naturels », ce qui augmente la probabilité d'échecs imprévus par leurs concepteurs.

Revenons-en maintenant aux preuves et au code vérifiables par machine. Voici un article de 2011 qui a découvert des vulnérabilités dans un compilateur C formellement vérifié : article :

Le deuxième problème CompCert que nous avons trouvé se manifeste par deux bogues qui conduisent à la génération du code suivant : stwu r1, -44432(r1) où une grande trame de pile PowerPC est allouée.

Le problème vient du dépassement de capacité du champ de déplacement 16 bits. La sémantique PPC de CompCert ne spécifie aucune limite à la largeur de cette valeur immédiate ; elle suppose que l’assembleur détectera les valeurs hors plage.

Il existe également un article de 2022 :

Dans CompCert-KVX, le commit e2618b31 a corrigé un bogue : l’instruction « nand » était affichée comme « and » ; « nand » n’était utilisé que dans le rare cas où il s’agissait de l’opérateur ~ (a & b). Ce bogue a été découvert lors de la compilation de programmes générés aléatoirement.

Et aujourd'hui, en 2026, voici comment Nadim Kobeissi décrit les vulnérabilités des logiciels formellement vérifiés dans Cryspen :

En novembre 2025, Filippo Valsorda a signalé de manière indépendante que libcrux-ml-dsa v0.0.3 produisait des clés publiques et des signatures différentes sur différentes plateformes étant donné la même entrée déterministe.

Le bogue résidait dans la fonction d'encapsulation interne vxarqu64, qui implémentait l'opération XAR utilisée dans la permutation Keccak-f de SHA-3. Le mécanisme de repli transmettait des paramètres incorrects à l'opération de décalage, corrompant ainsi le condensé SHA-3 sur les plateformes ARM64 dépourvues de prise en charge matérielle de SHA-3.

Cela relève de la catégorie des défaillances de type I : la fonction interne a été marquée, mais l’ensemble du système NEON n’a pas fourni de preuve de sécurité ou d’exactitude en cours d’exécution.

Et:

La bibliothèque libcrux-psq implémente un protocole de chiffrement post-quantique à clé pré-partagée. Dans la méthode `decrypt_out`, le chemin de déchiffrement AES-GCM 128 appelle `.unwrap()` sur le résultat du déchiffrement au lieu de propager les erreurs. Un texte chiffré malformé peut entraîner le plantage du processus.

Ces quatre problèmes se répartissent dans l'une des deux catégories suivantes :

Des cas où seule une partie du code a été vérifiée (car vérifier le reste était trop difficile), ce qui a permis de découvrir que le code non vérifié présentait plus de vulnérabilités que les auteurs ne l'avaient imaginé (et de manière plus mortelle).

Cas où les auteurs ont oublié de préciser des propriétés essentielles qui devaient être démontrées.

L'article de Nadim comprend une classification des modes de défaillance dans la vérification formelle ; il fournit également d'autres types de modes de défaillance (par exemple, un autre cas majeur est celui où « la spécification formelle elle-même est erronée, ou la preuve contient des déclarations fausses tacitement acceptées par le système construit »).

Enfin, nous pouvons examiner les échecs de la vérification formelle à l'interface entre logiciel et matériel. Un problème courant consiste à vérifier la résistance aux attaques par canaux auxiliaires.

Même si vous utilisez des formes cryptographiques parfaitement sécurisées pour protéger vos messages, si une personne située à quelques mètres de distance peut capter les fluctuations des signaux électriques et extraire votre clé privée après des centaines de milliers de chiffrements, votre sécurité reste compromise.

Cet article traite de « l'analyse de puissance différentielle », un exemple bien connu de telles techniques : article.

L'analyse différentielle de la consommation électrique est un type courant d'attaque par canal auxiliaire. Source : Wikipédia

Des tentatives ont toujours été faites pour prouver la sécurité face à de telles attaques. Cependant, toute preuve de ce type nécessite un modèle mathématique de l'attaquant permettant de démontrer la sécurité contre celui-ci.

On utilise parfois un « modèle de sondage direct » : on suppose que le nombre d’emplacements que l’attaquant peut interroger dans le circuit est limité. Cependant, ce modèle ne prend pas en compte certaines formes de fuites d’informations.

Comme on peut le constater dans cet article, un problème courant est la fuite transitoire : si vous pouvez observer un signal qui dépend non seulement de la valeur à un certain emplacement, mais aussi de la façon dont cette valeur change, cela suffit souvent pour récupérer les informations dont vous avez besoin à partir de deux valeurs (l’ancienne et la nouvelle valeur) plutôt que d’une seule.

Cet article propose des classifications d'autres formes de fuites.

Depuis des décennies, ces critiques de la vérification formelle ont contribué à son amélioration. Comparé au passé, nous sommes aujourd'hui mieux armés pour nous prémunir contre de tels problèmes. Mais même aujourd'hui, elle n'est pas parfaite.

Si l'on considère la situation dans son ensemble, un fil conducteur se dégage : la vérification formelle est un outil puissant.

Mais peu importe comment les termes marketing font passer la vérification formelle pour une garantie de « justesse prouvable », cette prétendue « justesse prouvable » ne prouve fondamentalement pas que le logiciel (ou le matériel) est « correct ».

Selon la plupart des conceptions humaines, « correct » signifie quelque chose comme : « le comportement des choses correspond à la compréhension qu'a l'utilisateur de l'intention du développeur ».

Et « sécurisé » signifie quelque chose comme : « le comportement des choses ne contrevient pas aux attentes de l'utilisateur et ne porte pas atteinte à ses intérêts ».

Dans les deux cas, la justesse et la sécurité se résument à une comparaison entre les objets mathématiques et les intentions ou attentes humaines.

Les intentions et les attentes humaines sont des objets mathématiquement complexes en soi ; après tout, le cerveau humain fait partie de l'univers et obéit à des lois physiques qui peuvent être simulées si l'on dispose d'une puissance de calcul suffisante.

Mais ce sont des objets mathématiques incroyablement complexes que ni les ordinateurs ni nous-mêmes ne pouvons comprendre, ni même lire.

En pratique, ce sont des boîtes noires ; nous ne comprenons nos intentions et nos attentes que grâce à des années d'expérience à observer nos pensées et à déduire celles des autres.

Et comme on ne peut pas intégrer des intentions humaines brutes dans un ordinateur, la vérification formelle ne peut pas prouver une comparaison avec les intentions humaines.

Par conséquent, la « correction prouvable » et la « sécurité prouvable » ne prouvent pas réellement la « correction » et la « sécurité » telles que nous, humains, les comprenons. Rien ne le permettra, à moins de pouvoir simuler pleinement le fonctionnement du cerveau humain.

Alors, à quoi ça sert ?

J'ai tendance à considérer les suites de tests, les systèmes de types et la vérification formelle comme différentes implémentations d'une même approche sous-jacente de la sécurité des langages de programmation (qui est peut-être aussi la seule approche raisonnable).

Il s'agit de spécifier de manière redondante nos intentions de différentes manières, puis de vérifier automatiquement si ces différentes spécifications sont compatibles entre elles.

Prenons ce code Python comme exemple :

def fib(n: int) -> int:

si n < 0 :

lever une exception("Les valeurs négatives ne sont pas prises en charge")

sinon si 0 <= n < 2 :

renvoyer n

autre:

retourner fib(n-1) + fib(n-2)

si __name__ == '__main__':

assert [fib(i) pour i dans range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

affirmer que fib(15) == 610

Ici, vous exprimez vos intentions de trois manières différentes :

Plus précisément, en implémentant la formule de Fibonacci dans le code.

Implicitement, à travers le système de types (spécifiant que les entrées, les sorties et les étapes intermédiaires de la récursion sont toutes des entiers)

Par la méthode du « package d’exemple » : cas de test

L'exécution du fichier comparera la formule aux exemples. Le vérificateur de types peut vérifier la compatibilité des types : l'addition de deux entiers est une opération conforme et produira un autre entier.

Les systèmes de types sont souvent un bon moyen de vérifier un travail en physique : si vous calculez une accélération mais que vous obtenez une réponse en mètres/seconde au lieu de mètres/seconde², vous savez que vous avez fait une erreur.

Les cas de test sont une instance de la définition du « package d'exemple », ce qui constitue souvent une manière plus naturelle pour les humains de manipuler des concepts que des définitions explicites directes.

Plus vous parviendrez à exprimer vos intentions de différentes manières, idéalement de façon à vous amener à réfléchir différemment au problème, plus vous aurez de chances d'exprimer ce que vous désirez vraiment une fois que toutes ces expressions se seront révélées compatibles entre elles.

La programmation sécurisée consiste à exprimer ses intentions de plusieurs manières différentes, puis à vérifier automatiquement si toutes ces expressions sont compatibles entre elles.

La vérification formelle permet d'étendre cette approche. Elle permet de spécifier ses intentions d'une infinité de manières redondantes, et le programme ne peut être validé que si toutes ces formulations sont compatibles.

Vous pouvez spécifier une implémentation hautement optimisée et une implémentation très inefficace mais lisible par un humain, puis vérifier leur concordance. Vous pouvez demander à dix amis de vous fournir une liste de propriétés mathématiques que votre programme devrait posséder, puis vérifier s'il les satisfait toutes.

Si le test échoue, vérifiez si le programme est erroné ou si les propriétés mathématiques sont mal spécifiées. L'IA peut effectuer toutes ces opérations avec une efficacité remarquable.

Alors, comment commencer ?

En réalité, vous n'écrirez pas vous-même de démonstrations. Si les méthodes formelles n'ont jamais été populaires, c'est parce que la plupart des gens sont incapables de comprendre comment écrire ces formules complexes. Pouvez-vous m'expliquer ce que signifie le code suivant ?

/-- Fonction auxiliaire : ≤ point par point au niveau du pli avec un accumulateur. -/

théorème privé foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (ab : Nat) (hAcc : a ≤ b)

(hLE : Forall₂ (· ≤ ·) ds1 ds2) :

List.foldl (λ acc d => acc * w + d) a ds1 ≤

List.foldl (λ acc d => acc * w + d) b ds2 := par

faire correspondre ds1, ds2, hLE avec

| [], [], .nil => hAcc exact

| d1::ds1', d2::ds2', .cons hd htl =>

simple [Liste.foldl]

affiner foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl

exact Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd

(Si vous vous posez la question, il s'agit de l'un des nombreux sous-lemmes de la preuve d'une déclaration de sécurité spécifique pour une variante des signatures SPHINCS.

Plus précisément, l'énoncé est le suivant : sauf en cas de collision de hachage, la signature d'un message généré à partir d'un condensé de hachage (dig1) nécessitera une valeur plus élevée à au moins un endroit de l'échelle de hachage que la signature de tout autre message, contenant ainsi des informations qui ne peuvent pas être calculées à partir de cette autre signature.

Vous n'avez pas besoin d'écrire manuellement le code et les preuves ; il vous suffit de laisser l'IA écrire les programmes pour vous (directement en Lean ou, pour plus de rapidité, en langage assembleur) et prouver les propriétés souhaitées au cours du processus.

L'avantage de cette tâche est qu'elle s'auto-valide, vous n'avez donc pas besoin de la superviser ; il suffit de laisser l'IA fonctionner en continu pendant plusieurs heures.

Le pire scénario serait qu'il tourne en rond sans progresser (ou, comme l'a fait mon Leanstral une fois, qu'il remplace l'énoncé qu'on lui demandait de prouver pour alléger sa charge de travail).

Au final, la seule chose qu'il vous reste à vérifier est si les déclarations qu'il a prouvées répondent à vos exigences.

Dans le cas de la variante de signature SPHINCS, voici la déclaration finale :

théorème wots_fullDigits_incomparable

{dig1 dig2 : Liste Nat} {w l1 l2 : Nat}

(hw : 0 < w)

(hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)

(hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w)

(hL2suff : l1 * (w - 1) < w ^ l2)

(hNeq : dig1 ≠ dig2) :

¬ Pour tout₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧

¬ Pour tout₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)

C'est à la limite de l'illisible :

Si les nombres générés à partir d'un condensé de hachage (dig1) ne sont pas égaux à ceux générés à partir d'un autre condensé de hachage (dig2)

Alors aucune des deux conditions suivantes n'est remplie :

Pour tous les nombres, les nombres de dig1 ≤ les nombres de dig2

Pour tous les nombres, les nombres de dig2 ≤ les nombres de dig1

Dans les « nombres étendus » (wotsFullDigits) générés par l'ajout de sommes de contrôle, il y aura inévitablement des endroits où les nombres seront plus élevés que dans l'extension de dig2.

Pour ce qui est de l'utilisation de grands modèles de langage pour écrire des preuves, je trouve Claude et Deepseek 4 Pro tout à fait performants. Leanstral, un modèle de poids open source plus petit, spécifiquement optimisé pour l'écriture de démonstrations Lean, constitue une alternative prometteuse.

Il possède 119 milliards de paramètres, activant 6 milliards par jeton, et peut être exécuté localement, bien que plus lentement (environ 15 jetons/seconde sur mon ordinateur portable). D'après les tests de performance, Leanstral surpasse des modèles généraux beaucoup plus volumineux.

D'après mon expérience personnelle actuelle, il est légèrement moins efficace que Deepseek 4 Pro, mais reste tout de même très efficace.

La vérification formelle ne peut pas résoudre tous nos problèmes.

Cependant, si nous voulons que le modèle de sécurité Internet ne repose plus sur la confiance accordée à quelques organisations puissantes, nous devons nous tourner vers la confiance dans le code, ce qui inclut la confiance dans le code même face à de puissants adversaires utilisant l'IA.

La vérification formelle assistée par l'IA nous a permis de faire un grand pas vers la réalisation de cet objectif.

Tout comme la blockchain et les ZK-SNARKs, l'intelligence artificielle et la vérification formelle sont également des technologies hautement complémentaires.

La blockchain vous offre une vérifiabilité ouverte et une résistance à la censure au prix de la confidentialité et de l'évolutivité, tandis que les ZK-SNARK vous restituent la confidentialité et l'évolutivité (en fait, encore plus qu'auparavant).

L'intelligence artificielle vous permet d'écrire d'énormes quantités de code au détriment de la précision, tandis que la vérification formelle vous restitue la précision (en fait, même supérieure à celle d'avant).

Par défaut, l'IA générera une grande quantité de code extrêmement hâtif, et le nombre de bugs augmentera.

En fait, dans certains cas, tolérer une augmentation du nombre de bogues est le bon compromis : si les bogues sont mineurs, alors même un logiciel bogué vaut mieux que pas de logiciel du tout.

Mais ici, la cybersécurité a un avenir optimiste : les logiciels continueront de se diviser en « parties périphériques non sécurisées » autour d’un « noyau sécurisé ».

Les composants non sécurisés s'exécuteront dans des environnements isolés, avec uniquement les autorisations minimales nécessaires à l'exécution de leurs tâches.

Le noyau sécurisé gère l'ensemble du système. En cas de défaillance du noyau sécurisé, tout est compromis, y compris vos données personnelles, votre argent, etc. En revanche, si une partie périphérique non sécurisée tombe en panne, le noyau sécurisé continue de vous protéger.

En matière de noyau sécurisé, nous ne pouvons tolérer la prolifération de code défectueux. Nous prendrons des mesures radicales pour limiter la taille du noyau sécurisé, voire la réduire encore davantage.

Nous allons plutôt investir toutes les performances supplémentaires apportées par l'IA dans le renforcement de la sécurité du noyau central, afin qu'il puisse supporter les exigences de confiance extrêmement élevées que nous lui imposons dans une société hautement numérique.

Le noyau d'un système d'exploitation (ou du moins une partie de celui-ci) deviendra un tel noyau sécurisé.

Ethereum en sera un autre.

Avec un peu de chance, au moins pour tous les calculs non gourmands en ressources, le matériel que vous utilisez deviendra un tiers.

Les systèmes liés à l'Internet des objets seront les quatrièmes.

Au moins parmi ces noyaux sécurisés, le vieil adage « les bugs sont inévitables ; on ne peut qu'essayer de les trouver avant l'attaquant » sera réfuté, remplacé par un monde plus optimiste où vous atteindrez une véritable sécurité.

Mais si vous êtes prêt à confier vos actifs et vos données à un logiciel mal conçu qui risque de les engloutir accidentellement dans un trou noir, eh bien, vous avez certainement aussi cette liberté.