ヴィタリック・ブテリン、AIによるサイバーセキュリティ終焉論を否定

ブテリン氏は9月17日のXへの投稿で、「AIハッキングによってサイバーセキュリティは終わる」という見方が広がっていることに同意しないと述べた。同氏は、暗号資産を保有し続ける人々は、より強力な自動攻撃にも耐えうる安全なデジタルシステムが生き残ることに暗黙のうちに賭けていると指摘し、自身の純資産の約90％が依然として暗号資産であると付け加えた。

同氏の主張の中心は形式検証であり、これは数学的仕様と証明を用いて、ソフトウェアが事前に定義された特性に従って動作するかどうかを判断する手法である。ブテリン氏は高度な数学的定理証明を例えに用い、十分に有能なAIがあれば、ソフトウェア自体が複雑であっても「このプログラムは安全である」ことを証明できると述べた。

ブテリン氏、形式検証は防御側に有利に働くと主張

ブテリン氏の主張は、AIセキュリティを、防御側の研究者が攻撃者よりも先にバグを見つけるだけの競争とは見なしていない。同氏の投稿は、開発者がシステムが満たすべき特性を定義し、自動証明ツールを用いて実装がそれに従っていることを立証するモデルを説明している。

イーサリアム自身の形式検証に関する文書では、この手法をより限定的に説明している。形式検証は、スマートコントラクトが形式的仕様に準拠していることを数学的に証明でき、その仕様に含まれる特性については通常のテストよりも強力な保証を提供するとしている。

同じイーサリアムの文書は、ブテリン氏のコメントの背景にある重要な限界も指摘している。証明は、ソフトウェアがチェック対象の仕様を満たしていることを立証するが、開発者がすべてのセキュリティ特性を正しく定義したことを自動的に証明するわけではない。仕様の選択が不適切または不完全な場合、証明の範囲外の動作が残る可能性がある。

ブテリン氏も投稿で同じ区別を行った。同氏は、「セキュリティ」を狭く定義しすぎると、プロトコル、サーバー、データベース、ネットワーク層、キャッシュ、その他の支援コンポーネントを含む領域での攻撃経路を見落とす可能性があると論じた。そのため同氏が提案する方向性は、少数のモジュールをセキュリティ上重要とラベル付けするのではなく、システム全体のより多くを検証することである。

ブテリン氏は以前から、AI支援による形式検証をソフトウェア開発の「最終形態」の可能性があると述べていた。同氏の以前のコメントでは、このアプローチをイーサリアムのコンセンサス、ゼロ知識システム、量子耐性暗号などの分野に適用していた。

イーサリアムはすでにAI支援セキュリティをテスト中

イーサリアムの研究者はすでにセキュリティ業務でAIを活用しているが、現行システムはシステム全体のセキュリティを自動証明するにはほど遠い。

イーサリアム財団プロトコルセキュリティチームは7月、協調型AIエージェントがイーサリアムで使用されているシステムに実際の欠陥を発見したと報告した。確認された発見の1つは、Rust libp2pのGossipsubネットワーク実装におけるリモートから到達可能なクラッシュだった。

この欠陥はCVE-2026-34219となった。米国国立脆弱性データベースの記録によると、0.49.4より前のバージョンは、細工されたPRUNEメッセージによってGossipsubのバックオフ処理中に算術オーバーフローが発生し、リモートからクラッシュする可能性があった。バージョン0.49.4でこの問題は修正された。

財団のセキュリティチームは、脆弱性の発見はAIワークフローの中で最も難しい部分ではないと述べた。研究者らは、AIエージェントが、到達不可能な実行パス、デバッグ専用の失敗、または意図したよりも弱い特性を証明しながら技術的には合格する形式的証明を含む、一見もっともらしいレポートを頻繁に生成することを発見した。

チームが発見を受け入れる前には、独立した再現が依然として必要だった。財団は、エージェントが、研究者が実際にテストしたいソフトウェアの動作を制約しない、有効に見える証明を生成する可能性があるため、自動チェックと人間によるレビューが必要だと述べた。

財団の経験はトリアージの問題として説明された。AIは多数の脆弱性候補を生成できるが、研究者は各問題が本番環境で到達可能かつ意味があるかどうかを判断する必要があった。

形式検証はイーサリアムのプロトコルロードマップに組み込まれる

イーサリアム財団は別途、形式検証を現在のプロトコル研究プログラムの一部としている。9月7日のプロトコル優先事項の更新で、財団は形式検証が、残る複数年にわたる研究領域全体にわたる横断的ツールとして機能すると述べた。この文書は、2029年までのプライバシー、状態、zkEVM開発、ポスト量子セキュリティ、その他のプロトコルコンポーネントに関する作業を対象としている。

同じロードマップでは、L1 zkEVMの開発が形式検証ツール、ワークフロー、検証済み暗号コンポーネントの進歩を促進すると予想されている。イーサリアムの研究者は、バリデータが最終的にすべてのブロックを独立して再実行するのではなく、簡潔な実行証明を検証するシステムを目指している。

8月に開始された別のイーサリアム財団プロジェクトは、すでにAIエージェントと機械チェック証明を組み合わせている。better.codesプロジェクトでは、研究者がLeanで形式化された暗号の健全性問題にAIシステムを向けることができ、Leanカーネルが提出された証明が固定された定理ステートメントを満たすかどうかをチェックする。

財団の第2四半期の資金調達報告書には、大規模言語モデルと形式手法を組み合わせたさらなる作業が記載されている。プロジェクトには、イーサリアムクライアントの実装を仕様に対してチェックするETHeorem、自動プロトコルコンプライアンス作業のためのSPECAとLeanAgent、RISC-V zkVMインフラストラクチャを含む形式検証が含まれる。

イーサリアムの更新された技術ロードマップでは、形式検証はプライバシー、ゼロ知識証明、ポスト量子保護と並ぶ役割を与えられている。したがって、ブテリン氏の9月17日のコメントは、新しいアップグレードや予定されたフォークを発表するものではなく、既存の研究の方向性を継続するものである。同氏の投稿では、新しいEIP、展開日、またはすべてのイーサリアムプログラムに形式検証を義務付ける規則については言及されなかった。

現在のAIの証拠は攻撃能力の強化も示す

最近のサイバーセキュリティ研究は、防御側の利用が拡大している一方で、AIが攻撃者をより有能にしているという懸念を裏付けている。Anthropicは9月の脅威インテリジェンスレポートで、悪意あるアクターがAIを使用して脆弱性調査、エクスプロイト開発、複数ターゲットキャンペーンを自動化しているのを観測したと述べた。同社は、一部のオペレーターが脆弱性調査を継続的に実施できる自動化ワークフローを維持していたと述べた。

Anthropicの以前の研究でも、大規模に同様の証拠が見つかっている。同社の協調的開示ダッシュボードによると、8月26日までに、392のオープンソースプロジェクトでAIが発見した2,300件の脆弱性を開示し、その時点で421件が上流でパッチ適用されていた。

Anthropicは同じ技術が防御に有用であると説明している。同社のProject Glasswingイニシアチブは、フロンティアモデルをセキュリティ企業やソフトウェアベンダーと使用して、悪意あるアクターが悪用する前に高重大度および重大度の欠陥を特定したと報告した。

攻撃側は依然として測定可能である。Anthropicの6月の調査では、2025年3月から2026年3月までの悪意あるサイバー活動に関連する832のアカウントを調査し、脅威アクターがサイバー作戦の複数の段階でAIを使用していることを発見した。ブテリン氏は、AIによるセキュリティリスクがビットコインへの信頼を深刻に損なう可能性があるという別の主張をすでに否定していた。同氏は、ネットワーク層の問題はソフトウェアやマイニングインフラのアップグレードで対処できることが多く、ビットコインのハッシュやプルーフ・オブ・ワークメカニズムの実際の破綻は極めて可能性が低いと述べた。

Anthropicの9月のレポートでは、調査員がセキュリティアプライアンスや政府標的に対してAI構築のエクスプロイトパイプラインを使用するオペレーターを特定し、一部のキャンペーンでは攻撃者が自身のテスト環境で検証した未知の脆弱性を生み出していたと述べた。