(P1) Le co-fondateur d'Ethereum, Vitalik Buterin, a déclaré que la vérification formelle assistée par l'IA pourrait éliminer la grande majorité des vulnérabilités de code, une déclaration qui intervient alors qu'un autre protocole DeFi a perdu 11,6 millions de dollars suite à un exploit sur son pont Ethereum.
(P2) « Si vous effectuez une vérification formelle de bout en bout, vous prouvez non seulement qu'une description du protocole est théoriquement sûre, mais que le morceau de code spécifique que l'utilisateur exécute est sûr en pratique », a écrit Buterin dans un article de blog publié lundi. Il a soutenu que cette approche pourrait supprimer plus de 99 % des conséquences négatives d'un code défectueux.
(P3) Les commentaires de Buterin sur la sécurité du code ont été mis en relief par un exploit signalé sur le pont Ethereum de Verus Protocol. Les sociétés de sécurité on-chain Blockaid et PeckShield ont rapporté qu'un attaquant a utilisé un message de transfert cross-chain falsifié pour drainer des actifs, qui ont ensuite été convertis en 5 402 Ether, d'une valeur de plus de 11,4 millions de dollars.
(P4) L'incident souligne les enjeux financiers des bugs logiciels dans l'écosystème crypto. Buterin estime que la vérification formelle est essentielle pour sécuriser la prochaine génération de l'infrastructure d'Ethereum, en particulier pour les composants complexes et critiques tels que les signatures résistantes au quantique, les STARK et les ZK-EVM.
Selon Blockaid, l'incident du pont Verus a été causé par une validation manquante du montant source, une faille qui aurait pu être identifiée et corrigée avec environ 10 lignes de code Solidity. La société de sécurité a noté que la structure de l'attaque ressemblait aux exploits de 2022 du Nomad Bridge (190 millions de dollars) et de Wormhole (325 millions de dollars), où des instructions frauduleuses ont trompé les ponts pour qu'ils envoient des fonds depuis leurs réserves.
Dans son post, Buterin a décrit un futur où les outils d'IA aident les développeurs à écrire à la fois du code hautement efficace et les preuves mathématiques pour vérifier son exactitude. Il a qualifié cette combinaison de « forme finale potentielle du développement logiciel ». Cette méthode est vue comme une défense puissante contre un futur où l'IA avancée pourrait également être utilisée pour découvrir et exécuter des cyberattaques à une échelle sans précédent.
Bien que fervent défenseur, Buterin a averti que la vérification formelle n'est « pas une panacée », car elle ne peut pas éliminer tous les risques de sécurité, tels que ceux découlant d'hypothèses initiales erronées ou de vulnérabilités matérielles. Cependant, il a soutenu qu'elle est exceptionnellement bien adaptée aux systèmes cryptographiques complexes qui sous-tendront la future feuille de route d'Ethereum, faisant d'un code quasi sans bug une attente réaliste.
Cet article est à titre informatif uniquement et ne constitue pas un conseil en investissement.
