Vitalik Buterin rejette l'idée d'une cybersécurité condamnée par l'IA

Buterin a écrit dans son message du 17 septembre sur X qu'il n'est pas d'accord avec l'idée de plus en plus répandue selon laquelle « le piratage par l'IA signifie que la cybersécurité est condamnée ». Il a déclaré que les personnes qui continuent de détenir des cryptomonnaies parient implicitement sur le fait que les systèmes numériques sécurisés peuvent survivre à des attaques automatisées plus puissantes, ajoutant qu'environ 90 % de sa propre valeur nette reste en cryptomonnaies.

Son argument repose sur la vérification formelle, une technique qui utilise des spécifications mathématiques et des preuves pour déterminer si un logiciel se comporte conformément à des propriétés prédéfinies. Buterin a utilisé la démonstration avancée de théorèmes mathématiques comme analogie, affirmant qu'une IA suffisamment capable pourrait aider à prouver que « ce programme est sécurisé », même lorsque le logiciel lui-même est complexe.

Buterin affirme que la vérification formelle peut favoriser les défenseurs

L'argument de Buterin ne traite pas la sécurité de l'IA comme une course où les chercheurs en défense trouvent simplement les bogues avant les attaquants. Son message décrit plutôt un modèle où les développeurs définissent les propriétés qu'un système doit satisfaire, puis utilisent des outils de preuve automatisés pour établir que l'implémentation les respecte.

La propre documentation de vérification formelle d'Ethereum décrit la technique en des termes plus restreints. Elle indique que la vérification formelle peut prouver mathématiquement qu'un contrat intelligent est conforme à une spécification formelle, offrant des garanties plus solides que les tests ordinaires pour les propriétés incluses dans cette spécification.

La même documentation d'Ethereum identifie une limite importante derrière les commentaires de Buterin. Une preuve établit que le logiciel satisfait la spécification vérifiée ; elle ne prouve pas automatiquement que les développeurs ont correctement défini chaque propriété de sécurité. Des spécifications mal choisies ou incomplètes peuvent laisser des comportements en dehors de la preuve.

Buterin a fait la même distinction dans son message. Il a soutenu qu'une définition trop étroite de la « sécurité » peut omettre des vecteurs d'attaque impliquant des domaines tels que les protocoles, les serveurs, les bases de données, les couches réseau, les caches ou d'autres composants de support. Sa direction proposée est donc de vérifier davantage l'ensemble du système au lieu d'étiqueter un petit groupe de modules comme critiques pour la sécurité.

Buterin avait déjà décrit la vérification formelle assistée par l'IA comme une possible « forme finale » du développement logiciel. Ses commentaires antérieurs appliquaient cette approche à des domaines incluant le consensus d'Ethereum, les systèmes à divulgation nulle de connaissance et la cryptographie résistante aux ordinateurs quantiques.

Ethereum teste déjà la sécurité assistée par l'IA

Les chercheurs d'Ethereum utilisent déjà l'IA dans les travaux de sécurité, bien que les systèmes actuels restent loin de la preuve automatique de la sécurité de l'ensemble du système.

L'équipe de sécurité du protocole de l'Ethereum Foundation a rapporté en juillet que des agents d'IA coordonnés avaient trouvé de véritables défauts dans les systèmes utilisés par Ethereum. Une découverte confirmée concernait un plantage accessible à distance dans l'implémentation réseau Gossipsub de Rust libp2p.

La faille est devenue CVE-2026-34219. Le registre de la base de données nationale des vulnérabilités des États-Unis indique que les versions antérieures à 0.49.4 pouvaient être plantées à distance via un message PRUNE spécialement conçu qui déclenchait un dépassement arithmétique lors de la gestion du backoff de Gossipsub. La version 0.49.4 a corrigé le problème.

L'équipe de sécurité de la Fondation a déclaré que la découverte de vulnérabilités n'était pas la partie la plus difficile du flux de travail de l'IA. Les chercheurs ont constaté que les agents d'IA généraient fréquemment des rapports convaincants impliquant des chemins d'exécution inaccessibles, des défaillances uniquement en mode débogage ou des preuves formelles qui passaient techniquement tout en prouvant une propriété plus faible que prévu.

La reproduction indépendante restait une exigence avant que l'équipe n'accepte une découverte. La Fondation a déclaré que des vérifications automatisées et un examen humain étaient nécessaires car un agent pouvait produire une preuve d'apparence valide qui ne parvenait pas à contraindre le comportement du logiciel que les chercheurs voulaient réellement tester.

L'expérience de la Fondation a été décrite comme un problème de triage : l'IA pouvait générer un grand nombre de vulnérabilités candidates, mais les chercheurs devaient encore déterminer si chaque problème était accessible et significatif en production.

La vérification formelle entre dans la feuille de route du protocole Ethereum

L'Ethereum Foundation a par ailleurs intégré la vérification formelle à son programme de recherche actuel sur le protocole. Dans sa mise à jour des priorités du protocole du 7 septembre, la Fondation a déclaré que la vérification formelle servirait d'outillage transversal dans ses domaines de recherche pluriannuels restants. Le document couvre les travaux sur la confidentialité, l'état, le développement de la zkEVM, la sécurité post-quantique et d'autres composants du protocole jusqu'en 2029.

La même feuille de route indique que le développement d'une zkEVM de couche 1 devrait faire progresser les outils de vérification formelle, les flux de travail et les composants cryptographiques vérifiés. Les chercheurs d'Ethereum travaillent à un système où les validateurs vérifient à terme des preuves d'exécution succinctes au lieu de réexécuter indépendamment chaque bloc.

Un autre projet de l'Ethereum Foundation lancé en août combine déjà des agents d'IA avec des preuves vérifiées par machine. Le projet better.codes permet aux chercheurs de diriger des systèmes d'IA vers un problème de solidité cryptographique formalisé dans Lean, tandis que le noyau Lean vérifie si les preuves soumises satisfont un énoncé de théorème fixe.

Le rapport de financement du deuxième trimestre de la Fondation répertorie d'autres travaux combinant de grands modèles de langage avec des méthodes formelles. Les projets incluent ETHeorem pour vérifier les implémentations du client Ethereum par rapport aux spécifications, SPECA et LeanAgent pour les travaux automatisés de conformité au protocole, et la vérification formelle impliquant l'infrastructure zkVM RISC-V.

La feuille de route technique mise à jour d'Ethereum donne à la vérification formelle un rôle aux côtés de la confidentialité, des preuves à divulgation nulle de connaissance et de la protection post-quantique. Les commentaires de Buterin du 17 septembre poursuivent donc une direction de recherche existante au lieu d'annoncer une nouvelle mise à niveau ou un fork planifié. Son message ne nommait pas de nouvel EIP, de date de déploiement ou de règle obligatoire exigeant que chaque programme Ethereum subisse une vérification formelle.

Les preuves actuelles de l'IA montrent également une capacité offensive plus forte

Des recherches récentes en cybersécurité soutiennent l'inquiétude selon laquelle l'IA rend les attaquants plus capables, même si l'utilisation défensive se développe. Anthropic a déclaré dans son rapport de renseignement sur les menaces de septembre qu'elle avait observé des acteurs malveillants utilisant l'IA pour automatiser la recherche de vulnérabilités, le développement d'exploits et les campagnes multi-cibles. L'entreprise a indiqué que certains opérateurs maintenaient des flux de travail automatisés capables de mener des recherches de vulnérabilités en continu.

Des recherches antérieures d'Anthropic ont trouvé des preuves similaires à grande échelle. Son tableau de bord de divulgation coordonnée indiquait qu'au 26 août, l'entreprise avait divulgué 2 300 vulnérabilités découvertes par l'IA dans 392 projets open source, dont 421 corrigées en amont à ce moment-là.

Anthropic a décrit la même technologie comme utile pour la défense. Son initiative Project Glasswing a rapporté l'utilisation de modèles de pointe avec des entreprises de sécurité et des éditeurs de logiciels pour localiser les failles de gravité élevée et critique avant que les acteurs malveillants ne puissent les exploiter.

Le côté offensif reste mesurable. L'étude de juin d'Anthropic a examiné 832 comptes associés à une activité cybernétique malveillante de mars 2025 à mars 2026 et a constaté que les acteurs de la menace utilisaient l'IA à plusieurs étapes des opérations cybernétiques. Buterin avait déjà rejeté un argument distinct selon lequel les risques de sécurité liés à l'IA pourraient gravement nuire à la confiance dans le Bitcoin. Il a déclaré que les problèmes de couche réseau pouvaient souvent être résolus par des mises à niveau logicielles et de l'infrastructure minière, tout en décrivant les ruptures réelles des hachages de Bitcoin ou de son mécanisme de preuve de travail comme hautement improbables.

Le rapport de septembre d'Anthropic indiquait que ses enquêteurs avaient identifié des opérateurs utilisant des pipelines d'exploitation construits par l'IA contre des appliances de sécurité et des cibles gouvernementales, certaines campagnes produisant des vulnérabilités inconnues auparavant que les attaquants validaient dans leurs propres environnements de test.