Au lieu de s’appuyer uniquement sur des auditeurs humains, les développeurs peuvent de plus en plus utiliser l’IA pour prouver mathématiquement que le code se comporte correctement.
Vitalik Buterin, co-fondateur d'Ethereum, a répondu aux préoccupations croissantes selon lesquelles la recherche de bogues basée sur l'IA submergerait les développeurs et créerait des opportunités d'exploitation non-stop sur les blockchains.
Selon lui, dans un avenir proche, l’utilisation de cette technologie pourrait effectivement rendre les systèmes cryptographiques plus sécurisés. Il affirme que la vérification formelle assistée par l’IA pourrait devenir l’une des défenses les plus solides contre les failles de sécurité des infrastructures cryptographiques et Internet.
L’IA pourrait renforcer la sécurité au lieu de la briser
La vérification formelle est la pratique consistant à rédiger des preuves mathématiques sur un logiciel qu'un ordinateur peut vérifier automatiquement au lieu que des personnes les examinent. Ce concept existe depuis des décennies ; cependant, cela n’a jamais fait son chemin car générer manuellement de telles preuves était plutôt fastidieux pour les développeurs de logiciels, et beaucoup d’entre eux ne s’en sont jamais souciés.
Maintenant, Buterin dit que l’IA a changé cette équation et qu’au lieu que les développeurs écrivent eux-mêmes les preuves, ils peuvent demander à une IA d’écrire à la fois le code et les preuves qui l’accompagnent. Ils vérifient ensuite simplement que la déclaration finale prouvée est bien ce qu’ils voulaient prouver.
Le développeur a décrit un scénario dans lequel les modèles d'IA deviennent suffisamment puissants pour automatiser la recherche de bogues dans le code existant, puis a demandé ce que cela signifierait pour les systèmes où une seule faille peut tout coûter aux utilisateurs.
Sa réponse a été que la vérification formelle, effectuée de bout en bout, vous permet de prouver mathématiquement qu'un morceau de code se comporte exactement comme prévu, de sorte qu'une IA suffisamment puissante recherchant des failles examinerait un code dont il a déjà été prouvé qu'elle n'en contenait pas.
Il a également évoqué des projets d’infrastructure Ethereum spécifiques dans lesquels cette approche est déjà tentée. L'un d'eux est Arklib, qui travaille à une implémentation STARK entièrement vérifiée formellement. Un autre est evm-asm, qui construit un EVM écrit dans un assemblage RISC-V de bas niveau et vérifie son exactitude par rapport à une implémentation de référence lisible par l'homme.
Vous aimerez peut-être aussi :
Sur la question de savoir quels modèles d'IA sont réellement utiles pour cela, Buterin a déclaré qu'il trouvait Claude et Deepseek 4 Pro suffisants pour rédiger des preuves Lean.
Il a également signalé Leanstral, un modèle à pondération ouverte plus petit, spécialement adapté au Lean, comme étant capable de fonctionner localement et de surpasser des modèles à usage général beaucoup plus grands sur des critères de vérification formels.
Mais il y a des limites
Malgré son enthousiasme pour la vérification formelle, Buterin a également consacré une partie importante de son essai à expliquer les échecs de cette méthode dans la pratique.
Cela inclut les bogues dans les compilateurs vérifiés ; des bibliothèques où seule une partie du code a été prouvée, et où les parties non prouvées se sont avérées être le problème ; et des spécifications techniquement éprouvées mais qui ne reflétaient tout simplement pas ce que le développeur voulait réellement garantir.
Cependant, sa conception plus large est que la vérification formelle ne remplace pas toutes les pratiques de sécurité mais constitue un outil puissant dans une tendance à plus long terme vers moins de bogues par ligne de code.
Le contexte est pertinent ici, étant donné que le jour de la parution du message de Buterin, le secteur de la cryptographie était sous le choc d'un troisième exploit majeur en seulement quatre jours après qu'un pirate informatique s'est enfui avec plus de 76 millions de dollars de crypto provenant du pont inter-chaînes du protocole Echo.
Quelques jours plus tôt, des rapports ont fait état d'un piratage de THORChain, qui a coûté plus de 10 millions de dollars à la plateforme.
Une autre attaque a eu lieu après celle-là, ciblant le pont Verus-Ethereum, au cours de laquelle un pirate informatique a profité de l'absence de contrôle de validation pour voler 11,58 millions de dollars. C’est le genre de défaut spécifique et localisé qu’une vérification formelle aurait pu détecter.
Voir l’article original en anglais
