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