ヴィタリック・ブテリンは、artificial intelligence could reshape how crypto systems are attacked と防御されるあり方を変え、インフラを数学的に検証されたソフトウェアへと押し進める可能性があると述べた。
ブテリンのエッセイが示すAIの脅威
イーサリアム共同創設者は、increasingly powerful AI models により、複雑なソフトウェアの脆弱性を発見し悪用することが、これまで以上に容易になると主張した。
ブテリンは、AIツールが脆弱性の自動発見を始めれば、暗号資産インフラに潜むバグは一段と深刻な問題になると指摘し、この懸念はセキュリティ研究コミュニティ全体でも共有されている。
彼は、より強力な防御が優先的に必要な対象として、イーサリアム (ETH) のインフラ、コンセンサスメカニズム、ポスト量子暗号を挙げた。
従来型の監査に頼るのではなく、ブテリンは開発者に対して「形式検証」を採用すべきだと述べた。これは、特定の条件下でコードが意図どおりに振る舞うことを数学的に証明する手法だ。
関連記事: Crypto Funds Bleed $1.07B As Iran Tensions End Six-Week Inflow Run
防御としての形式検証
「AIは、正確性を犠牲にしつつ大量のコードを書く能力を与えてくれる。一方、形式検証はその正確性を取り戻してくれる」とブテリンは記した。
彼は、AI生成ソフトウェアはもはや完全には信頼できないとする研究者たちの見解に反論し、むしろ前向きなシナリオを提示した。
ブテリンは、AI支援コーディングと検証ツールを組み合わせることで、人間だけが作るよりも堅牢なソフトウェアを最終的に生み出せると考えている。
彼はまた、暗号インフラとイーサリアム仮想マシン（EVM）ソフトウェアの保護に焦点を当てる Arklib や evm-asm といった進行中のプロジェクトにも言及した。
しかしこのエッセイは、形式検証が万能薬ではないことも警告した。数学的に証明されたシステムであっても、開発者が誤った前提を検証していたり、攻撃が検証済みコードの経路外に存在する場合には破られうる。
ブテリンのセキュリティ実績
ブテリンは、重要なデジタルインフラがより小さな「セキュアコア」システムに集約される未来像を描いている。そこでは重要度の高い部分が分離され、徹底的に検証される一方で、重要度の低いアプリケーションは制限付き権限で動作する。
イーサリアム共同創設者は、今年に入りAIとセキュリティのテーマに繰り返し言及してきた。2月には、AIによる生産性向上分をスピードとセキュリティの双方に振り分けるべきだと提案し、5月には Lean のような形式検証ツールを高信頼開発向けに支持している。最新の投稿ではこれらの議論をさらに拡張し、数学的証明こそが、ブロックチェーンおよび従来型インターネットシステムの双方におけるAI駆動型攻撃ツールへの最も説得力ある解答だと位置づけている。
次に読む: Iran Settles Hormuz Shipping Cover In Bitcoin, Eyes $10B Haul