(P1) イーサリアムの共同創設者であるヴィタリック・ブテリン氏は、AIを活用した形式検証によりコードの脆弱性の大部分を排除できると述べた。この発言は、別のDeFiプロトコルがイーサリアムブリッジの脆弱性により1,160万ドルを失った直後になされた。
(P2) 「エンドツーエンドで形式検証を行うということは、プロトコルの記述が理論的に安全であることを証明するだけでなく、ユーザーが実行する具体的なコードが実際に安全であることを証明することになる」と、ブテリン氏は月曜日に公開されたブログ記事に記した。同氏は、この手法により不備のあるコードによる負の影響を99%以上削減できると主張した。
(P3) コードのセキュリティに関するブテリン氏のコメントは、Verus Protocolのイーサリアムブリッジで報告された脆弱性悪用事件によってその重要性が浮き彫りになった。オンチェーンセキュリティ企業のBlockaidとPeckShieldは、攻撃者が偽造されたクロスチェーン転送メッセージを使用して資産を流出させ、それが後に1,140万ドル以上の価値がある5,402 Etherに変換されたと報告した。
(P4) この事件は、暗号資産エコシステムにおけるソフトウェアバグの経済的リスクを強調している。ブテリン氏は、次世代のイーサリアムインフラ、特に量子耐性署名、STARK、ZK-EVMといった複雑で重要なコンポーネントを保護するために、形式検証が不可欠であると考えている。
Blockaidによると、Verusブリッジの事件はソース金額の検証漏れが原因であり、これは約10行のSolidityコードで特定し修正できたはずの欠陥であった。同セキュリティ企業は、この攻撃の構造が2022年のNomad Bridge（1.9億ドル）やWormhole（3.25億ドル）の脆弱性悪用事件に酷似していると指摘した。これらのケースでは、不正な指示によってブリッジがリザーブから資金を送金するように仕向けられた。
記事の中でブテリン氏は、AIツールが開発者を支援し、高効率なコードとその正当性を検証するための数学的証明の両方を記述する未来を描写した。同氏は、この組み合わせをソフトウェア開発の潜在的な「最終形態」と呼んだ。この手法は、高度なAIが悪用され、かつてない規模でサイバー攻撃が発見・実行される未来に対する強力な防御策と見なされている。
ブテリン氏は強力な推進者である一方で、形式検証は「万能薬ではない」とも警告した。初期設定の誤った仮定やハードウェアの脆弱性に起因するすべてのセキュリティリスクを排除できるわけではないからだ。しかし、イーサリアムの将来のロードマップを支える複雑な暗号システムには非常に適しており、バグがほぼ存在しないコードの実現は現実的な期待であると論じた。
この記事は情報提供のみを目的としており、投資助言を構成するものではありません。
