Vitalik Buterin propose une vérification formelle assistée par l'IA pour protéger Ethereum contre les cyberattaques

Le co-fondateur d'Ethereum, Vitalik Buterin, a déclaré que les logiciels mathématiquement vérifiés deviennent essentiels pour protéger Ethereum et l'industrie plus large de la cryptographie contre les cyberattaques assistées par l'IA et les vulnérabilités logicielles.

Dans un article de blog publié lundi, Buterin a fait valoir que la « vérification formelle » assistée par l'IA pourrait aider à protéger les réseaux blockchain, les contrats intelligents et les systèmes de cryptographie contre les failles logicielles qui peuvent exposer les utilisateurs à des pertes financières irréversibles.

« Si cela est fait correctement, il a le potentiel de produire un code extrêmement efficace et d'être beaucoup plus sécurisé que la façon dont il a été programmé auparavant », a écrit Buterin, notant que le développeur Yoichi Hirai l'appelle « la forme finale du développement logiciel ».

La vérification formelle est un moyen de vérifier mathématiquement si un logiciel fonctionne correctement, avec une approche qui remonte aux travaux fondateurs des années 1950 et 1960. Selon Buterin, les progrès récents de l’IA rendent la technique plus pratique pour la recherche en génie logiciel et en sécurité.

« Si vous vérifiez formellement de bout en bout, vous prouvez non seulement qu'une certaine description du protocole est sécurisée en théorie, mais que le morceau de code spécifique que l'utilisateur exécute est sécurisé en pratique », a-t-il écrit. « Du point de vue de l'utilisateur, cela améliore considérablement la confiance sans avoir besoin de tiers : pour faire pleinement confiance au code, vous n'avez pas besoin de revoir l'intégralité du code, il vous suffit de vérifier les affirmations prouvées à son sujet. »

La publication de Buterin intervient à un moment où les chercheurs et les gouvernements avertissent que les modèles avancés d'IA s'améliorent rapidement dans la découverte et l'exploitation des vulnérabilités logicielles. Anthropic a restreint l'accès à son modèle de cybersécurité Claude Mythos à la suite de tests qui ont montré que le système pouvait identifier et exploiter de manière autonome les failles logicielles à des niveaux bien supérieurs à ceux des précédents modèles d'IA publics.

Le modèle a attiré l’attention des agences de renseignement et de sécurité en raison de ses capacités. En avril, Claude Mythos d'Anthropic a identifié 271 vulnérabilités dans Mozilla Firefox lors de tests internes, tandis qu'au début du mois, des chercheurs en sécurité ont noté qu'une première version du modèle avait permis de développer un exploit ciblant les protections de la puce M5 d'Apple. Des chercheurs de l'AI Security Institute du Royaume-Uni ont également découvert que le GPT-5.5 d'OpenAI a démontré des capacités offensives avancées en matière de cybersécurité.

« Les bugs dans le code informatique sont effrayants », a écrit Buterin.

Les bugs non découverts peuvent être dévastateurs pour les projets de cryptographie, où les failles logicielles peuvent être exploitées pour voler définitivement les fonds des utilisateurs avec peu de chances de récupération.

En avril, des attaquants du groupe Lazarus, soutenu par la Corée du Nord, ont réussi à drainer 292 millions de dollars de jetons de l'infrastructure Kelp DAO après avoir « empoisonné » les RPC internes utilisés par LayerZero Labs. Au total, on estime que les pirates informatiques parrainés par l’État nord-coréen ont volé à ce jour plus de 6 milliards de dollars de crypto-monnaie.

Buterin a noté que la vérification formelle pourrait également améliorer la confiance dans les logiciels générés par l'IA en démontrant que le code optimisé de bas niveau correspond à une implémentation de référence plus lisible.

« Une grande partie de la valeur ajoutée réside dans le fait que les tests sont véritablement de bout en bout », a écrit Buterin. « Souvent, les erreurs les plus problématiques sont les erreurs d'interaction trouvées à l'intersection de deux sous-systèmes analysés séparément. »

Cependant, même si Buterin voit le potentiel de l’IA pour aider à sécuriser le code des réseaux cryptographiques, il a averti que la vérification formelle ne peut pas éliminer complètement les risques de sécurité.

« La vérification formelle n'est pas une panacée. Mais elle est particulièrement adaptée aux situations où l'objectif est beaucoup plus simple que la mise en œuvre », écrit-il. « Cela est particulièrement vrai pour certaines des technologies les plus complexes que nous devrons mettre en œuvre dans la prochaine grande itération d'Ethereum : les signatures résistantes aux quantiques, les STARK, les algorithmes de consensus et les ZK-EVM. »

Buterin a rejeté l’idée selon laquelle des cyberattaques de plus en plus avancées finiraient par rendre impossible la protection des logiciels open source ou des systèmes décentralisés.

« Ce serait un avenir sombre pour la cybersécurité. C'est particulièrement un avenir extrêmement sombre pour ceux d'entre nous qui se soucient de la décentralisation et de la liberté d'Internet », a-t-il déclaré. « La philosophie cypherpunk repose fondamentalement sur l'idée que sur Internet, le défenseur a l'avantage. »

Au lieu de cela, Buterin a fait valoir que les futurs systèmes reposeront probablement sur une infrastructure « centrale » hautement protégée par une vérification formelle et des environnements de sécurité restreints.

« En ce qui concerne le noyau sécurisé, nous ne laissons pas les mauvais codes se multiplier », a-t-il ajouté. « Nous avons agi de manière agressive pour maintenir la taille du noyau de sécurité à une petite taille, et même la réduire davantage. »