Vitalik : Quelle est la clé de la prochaine étape d’Ethereum ?
TechFlow SélectionTechFlow Sélection
Vitalik : Quelle est la clé de la prochaine étape d’Ethereum ?
« Le code, c’est la loi » : telle était l’une des premières convictions du monde de la blockchain. Mais que se passe-t-il si le code lui-même contient un bogue ?
Dédié à des analyses Web3 approfondiesAuteur : Vitalik Buterin
Traduction : Jiahuan, ChainCatcher
Remerciements particuliers à Yoichi Hirai, Justin Drake, Nadim Kobeissi et Alex Hicks pour leurs retours et relectures.
Au cours des derniers mois, un nouveau paradigme de programmation s’est rapidement imposé aux avant-postes de la recherche avancée sur Ethereum, ainsi que dans de nombreux autres domaines du calcul : écrire directement du code dans des langages très bas niveau (par exemple le bytecode EVM, l’assembleur) ou en Lean, puis vérifier sa correction à l’aide de preuves mathématiques automatisées et vérifiables, rédigées elles aussi en Lean.
Bien menée, cette approche permet non seulement de produire des codes extrêmement efficaces, mais aussi d’atteindre un niveau de sécurité bien supérieur à celui offert par les méthodes de programmation traditionnelles. Yoichi Hirai qualifie ce paradigme de « forme ultime du développement logiciel ».
Cet article tente de démystifier ses principes fondamentaux, d’explorer ce que la vérification formelle des logiciels peut accomplir, et d’identifier ses faiblesses et limites, tant sur Ethereum qu’ailleurs.
Qu’est-ce que la vérification formelle ?
La vérification formelle consiste à rédiger des preuves de théorèmes mathématiques sous une forme pouvant être automatiquement vérifiée. Pour illustrer cela par un exemple relativement simple mais néanmoins intéressant, examinons un théorème élémentaire concernant la suite de Fibonacci : chaque troisième nombre est pair, tandis que les autres sont impairs.
1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 …
Une méthode simple pour démontrer ce résultat repose sur la récurrence mathématique, en progressant trois pas à la fois.
Tout d’abord, le cas de base. Posons F1 = F2 = 1, F3 = 2. Par observation, on constate que l’énoncé (« Fi est pair si i est multiple de 3, sinon impair ») est vérifié pour tout i < 3.
Ensuite, le cas inductif. Supposons que l’énoncé soit vérifié pour tout entier inférieur ou égal à 3k+3, c’est-à-dire que nous connaissons déjà la parité de F3k+1, F3k+2 et F3k+3, qui sont respectivement impair, impair et pair. Nous pouvons alors calculer la parité des trois nombres suivants :
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
Nous avons donc déduit que, si l’énoncé est vérifié jusqu’à 3k+3, il l’est également jusqu’à 3k+6. En appliquant répétitivement ce raisonnement, nous pouvons affirmer avec certitude que la règle s’applique à tous les entiers.
Ce raisonnement suffit à convaincre un humain. Mais que faire si vous souhaitez prouver quelque chose cent fois plus complexe, et être absolument certain de ne pas avoir commis d’erreur ? Eh bien, vous pouvez fournir à l’ordinateur une preuve qu’il sera capable de valider.
Voici comment cela se présente concrètement :
-- Suite de Fibonacci définie par 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
-- Énoncé : fib (3k+1) est impair, fib (3k+2) est impair, fib (3k+3) est pair.
-- Autrement dit : chaque troisième nombre de Fibonacci, à partir de fib 3, est pair.
-- Nous prouvons les trois assertions simultanément par récurrence sur k,
-- car chaque cas du bloc suivant repose sur le bloc précédent.
theorem fib_triple (k : Nat) :
fib (3 * k + 1) % 2 = 1 ∧
fib (3 * k + 2) % 2 = 1 ∧
fib (3 * k + 3) % 2 = 0 :=
by
induction k with
| zero => decide
| succ k ih =>
-- Réécrivons les nouveaux indices sous la forme (quelque chose) + 2 afin que fib se développe.
refine ⟨?_, ?_, ?_⟩
· show (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1
omega
· show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1
omega
· show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)
+ (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0
omega
Il s’agit du même raisonnement, mais exprimé en Lean — un langage de programmation couramment utilisé pour rédiger et vérifier des preuves mathématiques.
Cela diffère nettement de la preuve « humaine » présentée ci-dessus, et pour de bonnes raisons : ce qui est intuitif pour un ordinateur (au sens classique, c’est-à-dire un programme « déterministe » composé d’instructions if/then, et non pas un grand modèle de langage) diffère radicalement de ce qui l’est pour un humain.
Dans la preuve ci-dessus, vous ne mettez pas l’accent sur le fait que fib(3k+4) = fib(3k+3) + fib(3k+2), mais plutôt sur le fait que fib(3k+3) + fib(3k+2) est impair ; la stratégie appelée « omega » dans Lean, dont le nom est assez impressionnant, combine automatiquement cette information avec sa connaissance de la définition de fib(3k+4).
Dans des preuves plus complexes, vous devez parfois préciser explicitement, à chaque étape, quelle loi mathématique autorise ce passage, voire employer des noms obscurs comme Prod.mk.inj.
Mais, d’un autre côté, vous pouvez développer en une seule étape des expressions polynomiales gigantesques, et prouver leur validité simplement en une ligne, grâce à des tactiques comme « omega » ou « ring ».
Cette absence d’intuitivité et cette fastidieuse complexité expliquent largement pourquoi, bien que les preuves vérifiables par machine existent depuis près de 60 ans, ce domaine reste encore marginal. Toutefois, grâce à la progression fulgurante de l’intelligence artificielle, de nombreuses choses autrefois jugées impossibles deviennent aujourd’hui réalisables.
Lorsque les preuves mathématiques commencent à protéger le code
Jusqu’ici, vous vous êtes peut-être demandé : « Très bien, les ordinateurs peuvent désormais vérifier les preuves de théorèmes mathématiques, donc nous sommes enfin capables de distinguer, parmi les nouvelles et folles découvertes portant sur les nombres premiers, celles qui sont vraies de celles qui ne sont que des erreurs disséminées dans un PDF de cent pages. »
Peut-être même parviendrons-nous à trancher la question de la validité des travaux de Shinichi Mochizuki sur la conjecture abc !
Mais au-delà de la simple curiosité intellectuelle, à quoi cela sert-il ?
Il existe de nombreuses réponses possibles. Celle qui me semble particulièrement cruciale est la vérification de la correction des programmes informatiques, notamment ceux exécutant des tâches cryptographiques ou liées à la sécurité.
Après tout, un programme informatique est un objet mathématique, donc prouver qu’il se comporte d’une certaine manière constitue en soi un théorème mathématique.
Par exemple, supposons que vous vouliez démontrer que le logiciel de communication chiffrée Signal est véritablement sécurisé. Vous pouvez formaliser mathématiquement ce que signifie ici le terme « sécurisé ».
À un niveau élevé, vous cherchez à prouver que, sous certaines hypothèses cryptographiques, seule une personne détenant la clé privée peut obtenir la moindre information sur le contenu d’un message. Dans la pratique, de nombreuses propriétés de sécurité différentes sont toutes critiques.
Or, il existe effectivement une équipe qui travaille précisément sur ce problème ! L’un de leurs théorèmes de sécurité se présente ainsi :
theorem passive_secrecy_le_ddh
(g : G)
(adv : PassiveAdversary G SK) :
passiveSecrecyAdvantage (F := F) g adv ≤
ProbComp.boolDistAdvantage
(DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))
(DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))
Voici le résumé fourni par Leanstral de son sens :
Le théorème passive_secrecy_le_ddh est une réduction compacte montrant que la confidentialité passive des messages X3DH est au moins aussi difficile à violer que l’hypothèse DDH dans le modèle de l’oracle aléatoire. Si un attaquant parvient à casser la confidentialité passive des messages X3DH, alors il peut aussi casser DDH.
Puisque nous supposons que DDH est difficile à casser, X3DH est donc sécurisé contre les attaques passives. Ce théorème prouve que, si un adversaire observe passivement les messages d’échange de clés de Signal, il ne peut pas distinguer, avec une probabilité supérieure à une valeur négligeable, la clé de session générée de celle d’une clé aléatoire.
En combinant cette preuve avec celle de la correction de l’implémentation AES, on obtient une preuve que le protocole Signal est sécurisé contre les attaquants passifs.
Des projets similaires ont également prouvé la sécurité des implémentations de TLS et d’autres parties de la cryptographie intégrée aux navigateurs.
Si vous effectuez une vérification formelle complète bout à bout, vous ne prouvez pas seulement qu’une description théorique du protocole est sécurisée, mais bien que le code exécuté concrètement par les utilisateurs l’est aussi dans la pratique.
Du point de vue de l’utilisateur, cela renforce considérablement la confiance sans besoin de confiance préalable (trustlessness) : pour faire pleinement confiance au code, il n’est plus nécessaire d’inspecter l’intégralité du dépôt, mais uniquement les affirmations pour lesquelles il a été formellement prouvé.
Cependant, plusieurs grandes mises en garde importantes doivent être gardées à l’esprit, notamment quant à ce que signifie réellement ce mot crucial de « sécurité ».
Il est facile d’oublier de prouver les affirmations vraiment essentielles. Il est fréquent que l’affirmation à prouver ne soit pas plus simple à décrire que le code lui-même.
Il est facile d’introduire subrepticement dans la preuve des hypothèses finalement non valides. Il est aussi facile de décider qu’une seule partie du système nécessite réellement une vérification formelle, pour ensuite se faire piéger par de graves vulnérabilités présentes dans d’autres parties (voire dans le matériel lui-même).
Même l’implémentation de Lean elle-même pourrait contenir des bogues. Mais avant d’aborder tous ces détails ennuyeux, plongeons d’abord dans l’utopie que la vérification formelle, correctement et idéalement mise en œuvre, pourrait nous offrir.
La vérification formelle au service de la sécurité
Les bogues dans les codes informatiques sont effrayants.
Ils le deviennent encore plus lorsque vous placez des cryptomonnaies dans des contrats intelligents immuables sur une chaîne de blocs, et qu’un acteur tel que la Corée du Nord peut, dès qu’un bogue apparaît, drainer automatiquement tous vos fonds sans que vous puissiez contester.
Ils deviennent encore plus effrayants lorsqu’ils sont empaquetés dans des preuves à divulgation nulle de connaissance (zero-knowledge proofs), car si quelqu’un parvient à pirater le système de preuves ZK, il peut extraire l’intégralité des fonds, sans que nous puissions identifier ce qui s’est produit (pire encore, sans même savoir quand cela s’est produit).
Et ils deviennent encore plus effrayants lorsque nous disposons de puissants modèles d’IA, comme Claude Mythos deux versions plus tard, capables d’automatiser la découverte de ces bogues.
Certaines personnes réagissent à cette réalité en préconisant d’abandonner l’idée fondamentale des contrats intelligents, voire en estimant que le domaine du réseau ne peut plus être un terrain où les défenseurs détiennent un avantage asymétrique face aux attaquants.
Quelques citations :
« Pour renforcer un système, vous devez dépenser davantage de ressources (tokens) pour découvrir ses vulnérabilités que vos adversaires n’en dépensent pour les exploiter. »
Et :
« Notre secteur repose sur le code déterministe. On l’écrit, on le teste, on le publie, on est persuadé qu’il fonctionnera — or, selon mon expérience, cet accord tacite se brise. »
« Dans les meilleures entreprises natives de l’IA, les bases de code sont devenues des éléments auxquels on “croit” qu’elles fonctionnent, sans pouvoir plus précisément quantifier leur probabilité de succès. »
Pire encore, certains considèrent que la seule solution consiste à abandonner l’open source.
Pour la cybersécurité, ce serait un avenir sombre. En particulier pour ceux d’entre nous qui attachent de l’importance à la décentralisation et à la liberté sur Internet, c’est un scénario profondément pessimiste.
L’ensemble de l’esprit cypherpunk repose fondamentalement sur l’idée que, sur Internet, les défenseurs détiennent un avantage : construire un « château » numérique (qu’il s’agisse de chiffrement, de signatures ou de preuves) est bien plus facile que de le détruire.
Si nous perdons cet avantage, la sécurité sur Internet ne pourra plus reposer que sur les économies d’échelle, sur la traque mondiale des attaquants potentiels, et, au sens large, ne pourra plus être qu’un choix entre domination et destruction.
Je ne partage pas cet avis. J’ai une vision plus optimiste de l’avenir de la cybersécurité.
Je pense que le défi posé par les capacités accrues des IA à détecter les bogues est certes sévère, mais qu’il s’agit d’un défi transitoire. Une fois que la poussière sera retombée et que nous aurons atteint un nouvel équilibre, nous disposerons d’un environnement nettement plus favorable aux défenseurs qu’auparavant.
Mozilla partage cet avis. Voici ce qu’ils écrivent :
« Vous devrez probablement réorganiser toutes vos autres priorités et consacrer une attention soutenue et continue à cette tâche, mais il y a bel et bien une lumière 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 feront aussi. Notre travail n’est pas terminé, mais nous avons déjà traversé l’épreuve la plus difficile, et nous pouvons déjà entrevoir un avenir bien plus radieux qu’un simple rattrapage laborieux. »
« Les défenseurs ont enfin l’opportunité de remporter une victoire décisive… Les bogues sont en nombre fini, et nous entrons dans une ère où nous pourrons enfin tous les identifier. »
Or, si vous effectuez une recherche Ctrl+F sur les termes « formel » et « vérification » dans le billet de Mozilla, vous n’y 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 unique.
Sur quoi repose-t-il ? Fondamentalement sur ce graphique :
Baisse du nombre de vulnérabilités CVE au fil du temps
Depuis des décennies, de nombreuses technologies ont contribué à réduire le nombre de vulnérabilités :
- Les systèmes de typage
- Les langages garantissant la sécurité mémoire
- L’amélioration de l’architecture logicielle (notamment la sandboxing, les contrôles d’autorisations, et plus généralement la distinction explicite entre « base de code de confiance » et « autres codes »)
- De meilleures méthodes de test
- Un corpus croissant de connaissances sur les modèles de codage sécurisés et non sécurisés
- Une augmentation constante des bibliothèques logicielles pré-écrites et auditées
La vérification formelle assistée par l’IA ne doit pas être vue comme un nouveau paradigme à part entière, mais plutôt comme un accélérateur puissant d’une tendance et de paradigmes déjà en plein essor.
La vérification formelle n’est pas une panacée. Elle est cependant particulièrement adaptée aux situations où la spécification du comportement attendu est nettement plus simple que son implémentation. Cela est particulièrement vrai pour certaines technologies extrêmement complexes et délicates que nous devrons déployer dans la prochaine grande itération d’Ethereum : les signatures résistantes aux ordinateurs quantiques, les STARK, les algorithmes de consensus et les ZK-EVM.
STARK est un logiciel très complexe. Or, la propriété de sécurité fondamentale qu’il implémente est facile à comprendre et à formaliser : si vous voyez une preuve attestant qu’un programme P, pour une entrée x, produit une sortie y, alors soit (i) la fonction de hachage utilisée dans STARK a été cassée, soit (ii) P(x) = y.
C’est pourquoi le projet Arklib cherche à créer une implémentation STARK entièrement vérifiée formellement (voir VCV-io, qui fournit l’infrastructure de calcul d’oracle fondamentale utile pour vérifier formellement divers autres protocoles cryptographiques, dont beaucoup sont des dépendances de STARK).
Encore plus ambitieux est le projet evm-asm : il vise à construire une implémentation complète de l’EVM entièrement vérifiée formellement.
Ici, la propriété de sécurité est nettement moins évidente : l’objectif est essentiellement de prouver l’équivalence avec une autre implémentation de l’EVM écrite en Lean, mais conçue exclusivement pour maximiser l’intuitivité et la lisibilité, sans aucun souci d’efficacité d’exécution.
Il est possible que nous obtenions dix implémentations de l’EVM, toutes mutuellement prouvées équivalentes, et qu’elles contiennent toutes, par malchance, le même défaut fatal permettant à un attaquant de vider tous les ETH des adresses auxquelles il n’a pas accès.
Mais cette probabilité est nettement inférieure à celle qu’une implémentation actuelle de l’EVM comporte un tel défaut. Une autre propriété de sécurité, dont l’importance nous a été enseignée par de douloureuses leçons, est la résistance aux attaques par déni de service (DoS) — elle est, elle aussi, aisée à spécifier.
Deux autres domaines importants sont :
- Le consensus tolérant aux défaillances byzantines (BFT). Ici, formaliser toutes les propriétés de sécurité attendues est également difficile, mais vu la fréquence passée des bogues, cela vaut la peine d’essayer. C’est pourquoi nous disposons d’implémentations et de preuves de protocoles de consensus en cours de développement dans Lean.
- Les langages de programmation pour contrats intelligents : voir la vérification formelle dans Vyper et Verity.
Dans tous ces cas, l’une des grandes valeurs ajoutées de la vérification formelle réside dans le caractère véritablement bout à bout de ces preuves. Généralement, les bogues les plus coriaces sont des bogues d’interaction, qui se nichent à la frontière entre deux sous-systèmes considérés séparément.
Pour un humain, raisonner bout à bout sur l’ensemble du système est trop difficile. Un système automatisé de vérification des règles, lui, en est capable.
La vérification formelle au service de l’efficacité
Revenons sur evm-asm. Il s’agit d’une implémentation de l’EVM. Mais c’est une implémentation de l’EVM écrite directement en assembleur RISC-V.
Rien que la vérité.
Voici le code de l’opcode ADD :
import EvmAsm.Rv64.Program
namespace EvmAsm.Evm64
open EvmAsm.Rv64
/-- Addition EVM 256 bits : binaire, dépile 2 éléments, empile 1.
Limb 0 : LD, LD, ADD, SLTU (retenue), SD (5 instructions).
Limbs 1-3 : LD, LD, ADD, SLTU (retenue1), ADD (retenueEntrante), SLTU (retenue2), OR (retenueSortante), SD (8 instructions chacun).
Puis ADDI sp, sp, 32.
Registres : x12=sp, x7=acc, x6=operand, x5=carry, x11=carry1. -/
def evm_add : Program :=
-- Limb 0 (5 instructions)
LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;
ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;
-- Limb 1 (8 instructions)
LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;
-- Limb 2 (8 instructions)
LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;
-- Limb 3 (8 instructions)
LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;
-- Ajustement de la pile
ADDI .x12 .x12 32
end EvmAsm.Evm64
Le choix de RISC-V s’explique par le fait que les preuveurs ZK-EVM actuellement en construction fonctionnent généralement en prouvant des programmes RISC-V, après avoir compilé le client Ethereum vers RISC-V. Ainsi, une implémentation de l’EVM écrite directement en RISC-V devrait être la plus rapide possible.
RISC-V peut aussi être simulé très efficacement sur des ordinateurs classiques (et des ordinateurs portables RISC-V existent déjà sur le marché).
Bien entendu, pour obtenir une vérification véritablement bout à bout, vous devez aussi vérifier formellement l’implémentation RISC-V elle-même (ou l’arithmétisation du preuveur), mais ne vous inquiétez pas : ce travail existe déjà.
Écrire directement du code en assembleur était une pratique courante il y a cinquante ans. Depuis, nous avons abandonné cette méthode au profit de langages de haut niveau.
Les langages de haut niveau font un compromis sur l’efficacité, mais en échange, ils permettent d’écrire du code bien plus rapidement, et surtout, de comprendre bien plus facilement le code des autres — ce qui est indispensable pour la sécurité.
Grâce à la combinaison de la vérification formelle et de l’intelligence artificielle, nous avons l’opportunité de « revenir vers le futur ».
Plus précisément, nous pouvons laisser une IA écrire du code en assembleur, puis rédiger une preuve formelle vérifiant que ce code assembleur possède les propriétés requises.
Du moins, ces propriétés requises peuvent simplement consister à être parfaitement équivalent à une implémentation optimisée pour la lisibilité, écrite dans un langage de haut niveau convivial pour les humains.
Nous n’avons plus besoin d’un seul objet code qui équilibre lisibilité et efficacité, mais nous disposons désormais de deux objets indépendants : l’un (l’implémentation en assembleur), optimisé uniquement pour l’efficacité, tenant compte des besoins spécifiques de son environnement d’exécution ; l’autre (l’affirmation de sécurité, ou l’implémentation en langage de haut niveau), optimisé uniquement pour la lisibilité, puis nous prouvons mathématiquement l’équivalence entre les deux.
L’utilisateur peut (automatiquement) vérifier une seule fois cette preuve, puis, à partir de ce moment, exécuter uniquement la version rapide.
Cette méthode est extrêmement puissante, et Yoichi Hirai a raison de la qualifier de « forme ultime du développement logiciel ».
La vérification formelle n’est pas une panacée
Dans les domaines de la cryptographie et de l’informatique, une tradition presque aussi ancienne que la méthode formelle elle-même consiste à critiquer les méthodes formelles (ou plus largement, la dépendance à l’égard des « preuves »).
Cette littérature regorge d’exemples concrets. Commençons par les preuves manuscrites de la période initiale de la cryptographie, citées dans la critique de Menezes et Koblitz en 2004 :
« En 1979, Rabin proposa une fonction de chiffrement qui était, en un certain sens, “sécurisée de façon prouvable”, c’est-à-dire dotée d’une propriété de sécurité par réduction. »
« Une affirmation de sécurité par réduction stipule que toute personne capable de retrouver le message m à partir du texte chiffré y doit également être capable de factoriser n… Peu après la proposition du schéma de chiffrement de Rabin, Rivest fit remarquer, avec une ironie amère, que justement cette caractéristique, qui lui conférait une sécurité supplémentaire, provoquait son effondrement total face à un autre type d’attaquant, appelé “attaquant à chiffrés choisis”. »
« Autrement dit, si un attaquant peut, d’une manière ou d’une autre, inciter Alice à déchiffrer un texte chiffré de son choix, alors il peut suivre exactement les mêmes étapes que Sam, décrites dans le paragraphe précédent, pour factoriser n. »
Menezes et Koblitz donnent ensuite d’autres exemples. Le schéma récurrent est le suivant : la conception visant à rendre les protocoles cryptographiques plus « prouvables » rend souvent ces protocoles moins « naturels », ce qui augmente la probabilité qu’ils échouent dans des scénarios que les concepteurs n’avaient même pas envisagés.
Revenons maintenant aux preuves vérifiables par machine et au code. Voici un article publié en 2011, révélant un bogue dans un compilateur C formellement vérifié :
« Le deuxième problème que nous avons identifié dans CompCert se manifeste via deux bogues conduisant à la génération du code suivant : stwu r1, -44432(r1). Ce code alloue un cadre de pile PowerPC de grande taille. »
« Le problème réside dans le dépassement de la plage autorisée pour le champ de déplacement de 16 bits. La sémantique PPC de CompCert ne spécifie aucune limite sur la largeur de cet immédiat, et ses auteurs supposent que l’assembleur détectera les valeurs hors plage. »
Voici aussi un article publié en 2022 :
« Dans CompCert-KVX, le commit e2618b31 corrige un bogue : l’instruction “nand” était imprimée comme “and” ; “nand” n’était utilisée que dans le motif très rare ~(a & b). Ce bogue a été découvert en compilant des programmes générés aléatoirement. »
Et aujourd’hui, en 2026, voici comment Nadim Kobeissi décrit un bogue dans un logiciel formellement vérifié de Cryspen :
« En novembre 2025, Filippo Valsorda a signalé indépendamment que libcrux-ml-dsa v0.0.3 produisait, pour des entrées déterministes identiques, des clés publiques et des signatures différentes sur différentes plateformes. »
« Ce bogue résidait dans la fonction d’emballage interne _vxarq_u64, qui implémente l’opération XAR utilisée dans la permutation Keccak-f de SHA-3. Le mécanisme de secours transmettait des paramètres incorrects à l’opération de décalage, endommageant ainsi les empreintes SHA-3 sur les plateformes ARM64 dépourvues de support matériel SHA-3. »
« Il s’agit d’un défaut de type I : cette fonction interne était marquée, mais l’ensemble du backend NEON n’avait pas été soumis à une preuve de sécurité ou de correction à l’exécution. »
Et :
« La bibliothèque libcrux-psq implémente un protocole de clé pré-partagée post-quantique. Dans la méthode decrypt_out, le chemin de déchiffrement AES-GCM 128 appelait .unwrap() sur le résultat du déchiffrement au lieu de propager l’erreur. Un texte chiffré mal formaté pouvait ainsi faire planter le processus. »
Ces quatre problèmes appartiennent à l’un des deux types suivants :
- Cas où seule une partie du code a été vérifiée (car la vérification du reste était jugée trop difficile), et où il s’avère que le code non vérifié comporte plus de bogues — et de façon plus fatale — que ce que les auteurs avaient imaginé.
- Cas où les auteurs ont oublié de spécifier les propriétés clés devant être prouvées.
L’article de Nadim contient une classification des modes d’échec de la vérification formelle ; il mentionne également d’autres types d’échecs (par exemple, un autre cas majeur est celui où « la spécification formelle elle-même est erronée, ou où la preuve contient des affirmations fallacieuses acceptées silencieusement par le système construit »).
Enfin, examinons les échecs de la vérification formelle aux interfaces entre logiciel et matériel. Un problème courant ici est la capacité à prouver la résistance aux attaques par canaux auxiliaires (side-channel attacks).
Même si vous disposez d’une formulation cryptographique parfaitement sécurisée pour protéger vos messages, vous n’êtes pas pour autant en sécurité si une personne située à quelques mètres peut capter les fluctuations des signaux électriques et en déduire votre clé privée après quelques centaines de milliers d’opérations de chiffrement.
Voici un article sur l’« analyse différentielle de la consommation » (Differential Power Analysis), un exemple bien compris de ce type de technique.
L’analyse différentielle de la consommation 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 tels attaquants. Toutefois, toute preuve de ce type nécessite un modèle mathématique de l’attaquant, afin de pouvoir démontrer la sécurité contre lui.
On utilise parfois le « modèle à d sondes » : on suppose que l’attaquant peut interroger un nombre limité de positions dans le circuit. Mais certains types de fuites ne peuvent pas être capturés par ce modèle.
Comme observé 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 d’une position donnée, mais aussi de la variation de cette valeur, cela vous fournit généralement suffisamment d’informations pour récupérer ce que vous recherchez à partir de deux valeurs (ancienne et nouvelle), et non plus d’une seule.
Cet article propose une classification 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 bien plus habiles à anticiper de tels problèmes. Mais même aujourd’hui, elle n’est pas parfaite.
Dans une perspective globale, un fil conducteur principal se dégage. La vérification formelle est puissante.
Mais peu importe le jargon marketing qui la présente comme vous offrant une « correction prouvable », cette « correction prouvable » ne prouve fondamentalement pas que le logiciel (ou le matériel) est « correct ».
Selon la compréhension commune des humains, « correct » signifie approximativement : « le comportement de l’objet correspond à la compréhension qu’ont les utilisateurs des intentions du développeur ».
Et « sécurisé » signifie approximativement : « le comportement de l’objet ne contrevient pas aux attentes des utilisateurs ni ne porte atteinte à leurs intérêts ».
Dans les deux cas, la correction et la sécurité se ramènent à une comparaison entre un objet mathématique et les intentions ou attentes humaines.
Les intentions et attentes humaines sont, techniquement, aussi des objets mathématiques, puisque le cerveau humain fait partie de l’univers et obéit à des lois physiques que l’on pourrait simuler, étant donné 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.
À tous fins pratiques, ils constituent une boîte noire ; la seule raison pour laquelle nous avons une quelconque connaissance de nos propres intentions et attentes est que chacun d’entre nous a accumulé, au fil des années, une expérience d’observation de ses propres pensées et d’inférence des pensées d’autrui.
Et puisque nous ne pouvons pas insérer directement nos intentions humaines brutes dans un ordinateur, la vérification formelle ne peut pas prouver de comparaison avec ces intentions humaines.
Ainsi, la « correction prouvable » et la « sécurité prouvable » ne prouvent pas, en réalité, la « correction » ni la « sécurité » telles que nous les comprenons, humains. Rien ne le pourrait, sauf si nous parvenions à simuler entièrement le cerveau humain.
Alors, à quoi sert-elle réellement ?
J’ai tendance à considérer les suites de tests, les systèmes de typage et la vérification formelle comme des implémentations différentes — mais complémentaires — d’une même approche fondamentale de la sécurité des langages de programmation (ce qui est probablement la seule approche raisonnable).
Elles consistent toutes à spécifier de façon redondante nos intentions, sous des formes variées, puis à vérifier automatiquement que ces différentes spécifications sont mutuellement compatibles.
Prenons cet extrait de code Python :
def fib(n: int) -> int:
if n < 0:
raise Exception("Les valeurs négatives ne sont pas prises en charge")
elif 0 <= n < 2:
return n
else:
return fib(n-1) + fib(n-2)
if __name__ == '__main__':
assert [fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]
assert fib(15) == 610
Ici, vous exprimez votre intention de trois manières différentes :
- Explicitement, en implémentant la formule de Fibonacci dans le code
- Implicitement, via le système de typage (qui spécifie que les entrées, sorties et étapes intermédiaires récursives sont toutes des entiers)
- Via la méthode des « exemples empaquetés » : les cas de test
Exécuter le fichier compare la formule aux exemples. Le vérificateur de types peut vérifier la compatibilité des types : additionner deux entiers est une opération valide, produisant un autre entier.
Le système de typage est souvent une excellente méthode pour vérifier les calculs en physique : si vous calculez une accélération et obtenez une unité de m/s au lieu de m/s², vous savez que vous vous êtes trompé.
Les cas de test sont une instance concrète de la définition par « exemples empaquetés », une approche qui est souvent bien plus naturelle pour les humains lorsqu’ils manipulent des concepts, comparée à une définition explicite directe.
Plus vous pouvez exprimer vos intentions sous des formes différentes — idéalement des formes exigeant des modes de pensée radicalement distincts — et plus vous avez de chances, une fois que toutes ces expressions se sont révélées mutuellement compatibles, d’avoir effectivement exprimé ce que vous vouliez réellement.
La programmation sécurisée consiste à exprimer vos intentions de multiples façons différentes, puis à vérifier automatiquement que toutes ces expressions sont mutuellement compatibles.
La vérification formelle vous permet de pousser cette méthode encore plus loin. Grâce à elle, vous pouvez spécifier vos intentions de façon redondante, sous un nombre quasi illimité de formes différentes, et le programme ne sera validé que si toutes ces formes sont compatibles.
Vous pouvez spécifier une implémentation fortement optimisée et une implémentation extrêmement inefficace mais facile à lire pour les humains, puis vérifier qu’elles correspondent. Vous pouvez demander à vos dix amis de dresser la liste des propriétés mathématiques qu’ils pensent que votre programme devrait satisfaire, puis vérifier si toutes sont effectivement satisfaites.
Si ce n’est pas le cas, déterminez si le programme est fautif ou si la propriété mathématique a été mal formulée. Et vous pouvez accomplir tout cela de façon extrêmement efficace à l’aide de l’intelligence artificielle.
Comment commencer ?
Réaliste, vous ne rédigerez pas vous-même les preuves. La raison pour laquelle les méthodes formelles n’ont jamais connu de véritable popularité est que la plupart des gens ne parviennent pas à comprendre comment rédiger ces contenus obscurs. Pouvez-vous m’expliquer ce que signifie le code suivant ?
/-- Aide : ≤ ponctuelle au niveau de foldl avec un accumulateur. -/
private theorem foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (a b : 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 :=
by
match ds1, ds2, hLE with
| [], [], .nil => exact hAcc
| d1::ds1', d2::ds2', .cons hd htl =>
simp [List.foldl]
refine 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 voulez le savoir, il s’agit d’un des nombreux sous-lemmes d’une preuve spécifique d’une déclaration de sécurité pour une variante de signature SPHINCS.
Plus précisément, cette déclaration affirme que, sauf en cas de collision de hachage, la signature d’un message exigera, sur au moins une marche de hachage, une valeur supérieure à celle de toute autre signature de message, ce qui implique qu’elle contient des informations non calculables à partir de cette autre signature.)
Plutôt que de rédiger manuellement le code et les preuves, laissez une intelligence artificielle écrire pour vous le programme (soit directement en Lean, soit en assembleur pour la vitesse), tout en prouvant au passage toutes les propriétés souhaitées.
Cette tâche présente l’avantage d’être auto-vérifiée, donc vous n’avez pas besoin de la surveiller : il vous suffit de la laisser tourner seule pendant plusieurs heures.
Le pire scénario est qu’elle stagne sans progresser (ou, comme l’a fait un jour mon leanstral, qu’elle remplace, pour alléger sa propre charge de travail, l’affirmation qu’on lui avait demandé de prouver).
La seule chose que vous devrez vérifier à la fin est que l’affirmation prouvée correspond bien à vos attentes.
Dans la variante de signature SPHINCS, voici l’affirmation finale :
theorem wots_fullDigits_incomparable
{dig1 dig2 : List 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) :
¬ Forall₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧
¬ Forall₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)
Ceci se situe effectivement à la limite de la lisibilité :
Si les chiffres générés à partir d’un résumé de hachage (dig1) ne sont pas égaux à ceux générés à partir d’un autre résumé de hachage (dig2),
alors les deux affirmations suivantes sont toutes deux fausses :
- Pour tous les chiffres, le chiffre de dig1 est ≤ au chiffre de dig2
- Pour tous les chiffres, le chiffre de dig2 est ≤ au chiffre de dig1
Cela vaut également pour les « chiffres étendus » (wotsFullDigits) générés en ajoutant une somme de contrôle. Autrement dit, dans l’extension de dig1, certains chiffres seront inévitablement plus élevés, tandis que dans l’extension de dig2, d’autres chiffres seront plus élevés.
Concernant la rédaction de preuves à l’aide de grands modèles de langage, j’ai constaté que Claude et Deepseek 4 Pro sont tous deux compétents. Leanstral, un petit modèle open-source spécifiquement affiné pour écrire en Lean, constitue une alternative prometteuse.
Avec ses 119 milliards de paramètres, dont 6 milliards activés par token, il peut être exécuté localement, bien que lentement (environ 15 tokens/seconde sur mon ordinateur portable). Selon les benchmarks, Leanstral surpasse des modèles généraux bien plus volumineux :
Selon mon expérience personnelle actuelle, il est légèrement inférieur à Deepseek 4 Pro, mais reste tout à fait efficace.
La vérification formelle ne résout pas tous nos problèmes.
Toutefois, si nous voulons que le modèle de sécurité d’Internet ne repose plus sur la confiance aveugle accordée à quelques grandes organisations, nous devons passer à la confiance dans le code — y compris la confiance dans le code face à des adversaires dotés d’une intelligence artificielle puissante.
La vérification formelle assistée par l’IA constitue un pas décisif vers cet objectif.
Tout comme la blockchain et les ZK-SNARKs, l’IA et la vérification formelle sont des technologies extrêmement complémentaires.
La blockchain vous offre la vérifiabilité ouverte et la résistance à la censure, au prix de la confidentialité et de l’évolutivité, tandis que les ZK-SNARKs vous restituent la confidentialité et l’évolutivité (en fait, même davantage que précédemment).
L’IA vous donne la capacité de générer de grandes quantités de code, au prix de la précision, tandis que la vérification formelle vous restitue la précision (en fait, même davantage que précédemment).
Par défaut, l’IA engendrera une abondance de code extrêmement négligent, augmentant le nombre de bogues.
En effet, dans certains cas, accepter une augmentation des bogues constitue le bon compromis : si les bogues sont mineurs, un logiciel bogué peut être préférable à l’absence totale de ce logiciel.
Mais ici, la cybersécurité possède un avenir optimiste : les logiciels vont (continuer à) se scinder en une « périphérie non sécurisée » entourant un « cœur sécurisé ».
La périphérie non sécurisée s’exécutera dans une sandbox, avec uniquement les permissions minimales nécessaires à l’accomplissement de sa tâche.
Le cœur sécurisé supervisera l’ensemble. Si le cœur sécurisé tombe en panne, tout s’effondre — vos données personnelles, vos fonds, etc. Mais si une partie non sécurisée de la périphérie tombe en panne, le cœur sécurisé vous protège encore.
Lorsqu’il s’agit du cœur sécurisé, nous ne pouvons pas tolérer une prolifération de code bogué. Nous prendrons des mesures radicales pour maintenir sa taille réduite, voire la réduire encore davantage.
Au contraire, nous investirons l’ensemble des performances supplémentaires offertes par l’IA dans la tâche de rendre le cœur sécurisé encore plus sûr, afin qu’il puisse supporter la confiance extrêmement élevée que nous lui accordons dans une société hautement numérisée.
Le noyau d’un système d’exploitation (ou au moins une partie de celui-ci) constituera un tel cœur sécurisé.
Ethereum en sera un autre.
Espérons que, pour tous les calculs non intensifs en ressources, le matériel que vous utilisez deviendra le troisième.
Les systèmes liés à l’Internet des objets (IoT) constitueront le quatrième.
Du moins, au sein de ces cœurs sécurisés, le vieil adage « les bogues sont inévitables, vous ne pouvez qu’essayer de les trouver avant les attaquants » sera réfuté, remplacé par un monde bien plus prometteur où vous obtiendrez une sécurité réelle.
Mais si vous choisissez librement de confier vos actifs et vos données à des logiciels mal écrits, susceptibles de les avaler accidentellement dans un trou noir, eh bien, vous avez bien entendu cette liberté.
Bienvenue dans la communauté officielle TechFlow
Groupe Telegram :https://t.me/TechFlowDaily
Compte Twitter officiel :https://x.com/TechFlowPost
Compte Twitter anglais :https://x.com/BlockFlow_News
@VitalikButerin
