「blockchain security」タグの記事が 8 件 件あります

GitHub 史上最速で成長したリポジトリが、82 カ国にわたる 135,000 以上の脆弱な AI エージェントを露呈させました。そして、暗号資産ユーザーがその主な標的となっています。OpenClaw セキュリティ危機へようこそ。ここでは、AI ゲートウェイの導入を競う中国のテック巨人と、ブロックチェーンセキュリティのルールを書き換えつつある大規模なサプライチェーン攻撃が衝突しました。

セキュリティの悪夢と化したバイラル現象​

2026 年 1 月下旬、OpenClaw は前例のない快挙を成し遂げました。1 日で 20,000 以上の GitHub スターを獲得し、プラットフォーム史上最速で成長したオープンソースプロジェクトとなったのです。2026 年 3 月までに、この AI アシスタントは 250,000 以上のスターを集め、世界中のテック愛好家が個人用 AI の未来と思われたものをこぞってインストールしました。

クラウドベースの AI アシスタントとは異なり、OpenClaw はファイル、メール、アプリケーションへのフルアクセス権限を持ち、ユーザーのコンピュータ上で完全に動作します。WhatsApp、Telegram、Discord を通じてメッセージを送信でき、24 時間 365 日稼働します。携帯電話からの何気ないメッセージをトリガーに、シェルコマンドの実行、ウェブ閲覧、メール送信、カレンダー管理、さらにはデジタルライフ全般にわたるアクションを実行します。

その売り文句は抗いがたいものでした。ローカルで動作し、常に利用可能で、無限の能力を持つ自分専用の AI エージェント。しかし、その現実ははるかに危険なものでした。

135,000 件の露出：セキュリティ災害の規模​

2026 年 2 月までに、セキュリティ研究者は衝撃的な事実を発見しました。82 カ国で 135,000 以上の OpenClaw インスタンスがパブリックインターネット上に露出しており、そのうち 50,000 以上がリモートコード実行に対して脆弱だったのです。その原因は、OpenClaw のデフォルト設定における根本的なセキュリティ上の欠陥でした。

OpenClaw はデフォルトで 0.0.0.0:18789 にバインドされます。つまり、セキュリティのベストプラクティスが要求する 127.0.0.1（ローカルホストのみ）ではなく、パブリックインターネットを含むすべてのネットワークインターフェースでリスニングします。これを例えるなら、玄関のドアを全開にして「ご自由にどうぞ」という看板を立てているようなものです。しかも、そのドアはあなたのデジタルライフ全体につながっています。

「ClawJacked」脆弱性は状況をさらに悪化させました。攻撃者は、ユーザーに悪意のあるウェブサイトを訪問させるだけで、AI アシスタントを乗っ取ることができました。一度侵害されると、攻撃者は AI エージェント自身と同じレベルのアクセス権、つまりファイル、認証情報、ブラウザデータ、そして暗号資産ウォレットへのアクセス権を手に入れます。

カスペルスキー、Bitsight、Oasis Security などのセキュリティ企業は一斉に緊急警告を発しました。共通の認識は明確でした。OpenClaw は、重大なリモートコード実行の脆弱性、アーキテクチャ上の弱点、そして最も憂慮すべきことに、プラグインマーケットプレイスにおける大規模なサプライチェーン汚染キャンペーンを含む「セキュリティの悪夢」を象徴していたのです。

ClawHavoc：暗号資産ユーザーを狙ったサプライチェーン攻撃​

研究者が OpenClaw 本体の脆弱性に焦点を当てている間、より狡猾な脅威が ClawHub で展開されていました。ClawHub は、ユーザーが AI エージェント用のサードパーティ製「スキル」（プラグイン）を簡単に見つけてインストールできるように設計されたマーケットプレイスです。

2026 年 2 月、ClawHavoc と名付けられたセキュリティ調査により、ClawHub で監査された 2,857 のスキルのうち、341 が悪意のあるものであることが判明しました。2 月中旬にマーケットプレイスが 10,700 以上のスキルに拡大すると、悪意のあるスキルの数は 2 倍以上の 824 に増え、一部の報告では 1,184 個の悪意のあるスキルに達したとされています。

その攻撃メカニズムは驚くほど巧妙でした。

1. 偽の前提条件: 335 のスキルが偽のインストール要件を使用して、ユーザーに Atomic macOS Stealer (AMOS) マルウェアをダウンロードさせようとしました。
2. プラットフォーム固有のペイロード: Windows では、侵害された GitHub リポジトリから「openclaw-agent.zip」をダウンロードさせました。macOS では、glot.io にホストされたインストールスクリプトをターミナルに直接コピーさせました。
3. 高度なソーシャルエンジニアリング: ドキュメントを用いて、正当なセットアップ手順を装いながら、悪意のあるコマンドを実行するようユーザーを説得しました。
4. 統合されたインフラ: すべての悪意のあるスキルが同じコマンド＆コントロール（C2）インフラを共有しており、組織的なキャンペーンであることを示していました。

主な標的は暗号資産ユーザーでした。

このマルウェアは、以下の情報を盗むように設計されていました。

• 取引所の API キー
• ウォレットの秘密鍵
• SSH 認証情報
• ブラウザのパスワード
• Solana ウォレットやウォレットトラッカーからの暗号資産固有のデータ

悪意のあるスキルのうち、111 個は Solana ウォレットの統合や暗号資産トラッカーなど、明確に暗号資産に特化したツールでした。攻撃者は、ブラウザ拡張機能やウォレットツールのインストールに慣れている暗号資産ユーザーが、AI エージェントのサプライチェーン攻撃において最も収益性の高い標的であることを理解していました。

中国テック巨人による導入競争​

セキュリティ研究者が警告を発する一方で、中国のテック巨人はこれを好機と捉えました。2026 年 3 月初旬、テンセント、アリババ、バイトダンス、JD.com、百度は、競い合うように OpenClaw の無料インストールキャンペーンを開始しました。通常は数ヶ月かかる競争のスクランブルを、わずか数日に凝縮したのです。

戦略は明確でした。商用 AI プロジェクトが拡大する前に、無料導入を顧客獲得の手段として利用し、ユーザーを囲い込むことです。各社は「次世代の AI 開発者にとって最初のインフラ接点」になることを目指して競い合いました。

• テンセントは QClaw を発表し、OpenClaw を WeChat と統合することで、ユーザーがスマートフォンからコマンドを送信してノートパソコンをリモート制御できるようにしました。
• アリババクラウドは、自社の AI モデル Qwen シリーズと接続し、プラットフォーム全体で OpenClaw のサポートを展開しました。
• **バイトダンスの火山引擎（Volcano Engine）**は、OpenClaw の「すぐに使える」バージョンである ArkClaw を発表しました。

皮肉なことに、セキュリティ研究者が 135,000 件の露出インスタンスと大規模なサプライチェーン攻撃を警告している最中に、中国最大級のテック企業各社は、何百万人ものユーザーに向けて積極的な大規模導入を推進していたのです。技術的な熱狂とセキュリティの現実との衝突が、これほどまでに浮き彫りになったことはありません。

Web3 の AI エージェント問題：MCP が仮想通貨ウォレットと出会うとき​

OpenClaw の危機は、Web3 ビルダーがもはや無視できない深刻な問題を露呈しました： AI エージェントによるオンチェーン資産の管理が増加している一方で、そのセキュリティ モデルは危険なほど未熟である という点です。

Model Context Protocol (MCP) — AI エージェントを外部システムに接続するための新しい標準 — は、AI がブロックチェーンと対話するためのゲートウェイになりつつあります。MCP サーバーは、フルスタックの Web3 への統合 API ゲートウェイとして機能し、AI エージェントがブロックチェーン データの読み取り、トランザクションの準備、およびオンチェーン アクションの実行を可能にします。

現在、ほとんどの仮想通貨 MCP サーバーは 秘密鍵 による設定を必要としており、これが単一障害点（SPOF）となっています。もし AI エージェントが侵害された場合 — 数万の OpenClaw インスタンスがそうであったように — 攻撃者は資金に直接アクセスできてしまいます。

現在、2 つの競合するセキュリティ モデルが登場しています：

1. 署名の委任（ユーザー制御）​

AI エージェントがトランザクションを準備しますが、署名に関する独占的な制御権はユーザーが保持します。秘密鍵が ユーザーのデバイスから離れることはありません。これは最も安全なアプローチですが、エージェントの自律性は制限されます。

2. エージェント制御のアロワンス​

エージェントは独自の鍵を持ち、ユーザーに代わって支出するためのアロワンス（許容額）を受け取ります。秘密鍵はエージェント ホストによって安全に管理され、支出額には上限が設定されます。これにより自律的な運用が可能になりますが、ホストのセキュリティに対する信頼が必要になります。

どちらのモデルもまだ広く普及していません。ほとんどの仮想通貨 MCP 実装は、依然として「エージェントに秘密鍵を渡す」という危険な手法を使用しており、これはまさに ClawHavoc 攻撃者が予期していたシナリオそのものです。

2026 年の予測では、仮想通貨ウォレットの 60% がエージェント型 AI を使用して ポートフォリオの管理、トランザクションの追跡、セキュリティの向上を行うようになるとされています。業界では、これらのやり取りを保護するために、マルチパーティ計算 (MPC)、アカウント抽象化 (Account Abstraction)、生体認証、および暗号化されたローカル ストレージの実装が進められています。ERC-8004 (Ethereum Foundation、MetaMask、Google が共同主導) などの標準規格は、オンチェーンでの AI エージェントに対する検証可能なアイデンティティと信用履歴の作成を試みています。

しかし、OpenClaw はこれらのセーフガードがまだ整っていないことを証明しました。そして攻撃者はすでにその隙を突いています。

NVIDIA によるエンタープライズ向けの回答：GTC 2026 での NemoClaw​

OpenClaw のセキュリティ危機が拡大する中、NVIDIA は好機を見出しました。3 月中旬の GTC 2026 において、同社は NemoClaw を発表しました。これは、当初からセキュリティとプライバシーを考慮して設計された、エンタープライズ オートメーション 専用のオープンソース AI エージェント プラットフォームです。

コンシューマー優先でどこにでもインストールできる OpenClaw のアプローチとは異なり、NemoClaw は以下のような特徴で企業をターゲットにしています：

• 組み込みのセキュリティおよびプライバシー ツール：OpenClaw を悩ませた脆弱性に対処
• エンタープライズ認証とアクセス制御：デフォルト設定が「インターネットに公開」されていることによる惨事を防止
• マルチプラットフォーム サポート：NVIDIA の NeMo、Nemotron、Cosmos AI フレームワークを活用し、NVIDIA チップ以外でも動作
• パートナー エコシステム：Salesforce、Google、Cisco、Adobe、CrowdStrike との提携に向けた協議

このタイミングはこれ以上ないほど戦略的です。OpenClaw の「ロブスター熱（Lobster Fever）」がコンシューマー向け AI エージェントの危険性を露呈させた直後、NVIDIA は NemoClaw を安全なエンタープライズ グレードの代替案として位置づけ、ビジネス AI エージェント市場において OpenAI に挑戦しようとしています。

AI 統合インフラを構築している Web3 企業にとって、NemoClaw は OpenClaw が露呈させたセキュリティ問題に対する潜在的な解決策となります。つまり、高価値のブロックチェーン資産と安全に対話できる、専門的に管理・監査・保護された AI エージェントのデプロイメントです。

Web3 が必要としていた警鐘​

OpenClaw の危機は、単なる AI セキュリティの話ではありません。それは ブロックチェーン インフラストラクチャの物語 です。

以下の影響を考慮してください：

• 135,000 以上の公開された AI エージェント が仮想通貨ウォレットにアクセスできる可能性があった
• 1,184 個の悪意のあるプラグイン が特に仮想通貨ユーザーを標的にしていた
• 中国の 5 大テック企業 が適切なセキュリティ レビューなしに数百万のインストールを推進した
• 仮想通貨ウォレットの 60% が年末までに AI エージェントを使用すると予測されている
• AI とブロックチェーンの相互作用に関する 広く採用されたセキュリティ標準がまだ存在しない

これは Web3 における「サプライチェーン セキュリティの転換点」であり、伝統的金融（TradFi）における 2020 年の SolarWinds 攻撃や、仮想通貨における 2016 年の DAO ハックに匹敵します。これは根本的な真実を浮き彫りにしています： ブロックチェーン インフラがより強力で自動化されるにつれ、攻撃対象領域は指数関数的に拡大する ということです。

業界の対応によって、AI エージェントが Web3 機能への安全なゲートウェイになるか、あるいはこの分野で史上最大の脆弱性になるかが決まります。署名委任モデル、エージェント アロワンス、MPC ソリューション、アカウント抽象化の間の選択は、単なる技術的な問題ではなく、存亡に関わる問題です。

Web3 ビルダーが今すべきこと​

Web3 で構築を行い、AI エージェントを統合している（または計画している）場合、以下のチェックリストを確認してください：

1. MCP サーバーのセキュリティを監査する：AI エージェントのアクセスに秘密鍵を必要としている場合、ClawHavoc 型の攻撃ベクトルを作成していることになります。
2. 署名の委任を実装する：AI がトランザクションを準備する場合でも、ユーザーが常にトランザクション署名に対する独占的な制御権を保持する必要があります。
3. 自律型エージェントにはアロワンス ベースのモデルを使用する：エージェントが独立して行動する必要がある場合は、厳格な支出制限を設けた専用の鍵を割り当ててください。
4. デフォルトのネットワーク設定で AI エージェントをインストールしない：エンタープライズ グレードの認証がない限り、常にローカルホスト (127.0.0.1) にバインドしてください。
5. AI エージェントのマーケットプレイスをアプリストアのように扱う：サードパーティのスキルを信頼する前に、コード署名、セキュリティ監査、およびレピュテーション システムを要求してください。
6. AI エージェントのリスクについてユーザーを教育する：ほとんどの仮想通貨ユーザーは、AI エージェントを利用することが、誰かにコンピュータへのルート アクセス権を与えることと機能的に同等であることを理解していません。

OpenClaw の危機は、「デフォルトでのセキュリティ（Security-by-default）」が機能よりも重要である ことを教えてくれました。AI エージェントをデプロイする競争が、それらを保護する競争を追い越してはなりません。

AI エージェントに接続するブロックチェーン インフラストラクチャを構築していますか？ BlockEden.xyz は、40 以上のブロックチェーンに対して、高度な統合のために設計されたセキュリティ第一のアーキテクチャを備えたエンタープライズ グレードの API インフラストラクチャを提供しています。当社のサービスを探索して、永続的な基盤の上に構築を開始してください。

---

情報源:

• Meet OpenClaw: The AI assistant that broke every record – and started a security panic
• OpenClaw: GitHub's Fastest-Ever Rising Star Becomes 2026's First Major AI Security Disaster
• New OpenClaw AI agent found unsafe for use | Kaspersky official blog
• OpenClaw Security: Risks of Exposed AI Agents Explained | Bitsight
• ClawJacked: OpenClaw Vulnerability Enables Full Agent Takeover
• Researchers Find 341 Malicious ClawHub Skills Stealing Data from OpenClaw Users
• Malicious OpenClaw Skills Used to Distribute Atomic MacOS Stealer | Trend Micro
• ClawHavoc Poisons OpenClaw's ClawHub With 1,184 Malicious Skills
• Using MCP with Web3: How to secure blockchain-interacting agents | Google Cloud Blog
• How to Build AI-Powered Web3 Crypto Wallets in 2026
• Model Context Protocol (MCP): Bridging AI and Blockchain for Smarter Crypto Projects
• Chinese Tech Giants Race to Adopt OpenClaw AI Gateway
• China's AI Red Packet War: ByteDance, Tencent, Alibaba and Baidu Battle to Become the Default Gateway
• Nvidia targets enterprise AI agents with new open-source NemoClaw platform
• Nvidia Prepares NemoClaw to Power Enterprise AI Agents
• NVIDIA to Launch Open-Source AI Agent "NemoClaw" at GTC 2026: What We Know So Far

わずか 1.22 ドル — コーヒー 1 杯の価格よりも安いコストで、AI エージェントがスマートコントラクトをスキャンし、脆弱性を特定し、実行可能なエクスプロイトを生成できるようになりました。これはセキュリティのホワイトペーパーにある理論上のシナリオではありません。2025 年後半に Anthropic と MATS Fellows の研究者によって公開された、AI エージェントの実際のスマートコントラクトに対する攻撃能力を評価する初のベンチマーク「SCONE-bench」の測定結果です。2020 年から 2025 年の間に実際に攻撃を受けた 405 件のコントラクトにおいて、10 個の最先端 AI モデルが合計で 207 件の即時実行可能なエクスプロイトを生成し、シミュレーション上で 5 億 5,010 万ドルの盗難資金を生み出しました。

この影響は研究室の枠を遥かに超えています。DeFi（分散型金融）プロトコル全体では、1,000 億ドル以上の TVL（預かり資産）が保持されています。もし攻撃能力が 1.3 ヶ月ごとに倍増し続けるならば（Anthropic のデータが示す軌跡）、オンチェーン金融を支えるセキュリティの前提は転換点を迎えようとしています。

1 コントラクトあたり $ 1.22 で、AI エージェントはスマートコントラクトをスキャンして悪用可能な脆弱性を特定できるようになりました。そして、攻撃側のエクスプロイト能力は 1.3 ヶ月ごとに倍増しています。分散型金融（DeFi）における、最も重大な軍拡競争へようこそ。

2026 年 2 月、OpenAI と Paradigm は共同で、AI エージェントがスマートコントラクトの脆弱性をいかに効果的に検出し、修正し、悪用するかを評価するオープンソースのベンチマーク EVMbench をリリースしました。その結果は驚くべきものでした。GPT-5.3-Codex は、既知の脆弱なコントラクトの 72.2 % の悪用に成功しました。これは、わずか 6 ヶ月前の 31.9 % から急上昇しています。一方、特化型の AI セキュリティエージェントは、9,680 万ドル相当の被害を出した 90 の DeFi 攻撃事例のうち 92 % で脆弱性を検出しました。これは、ベースラインとなる GPT-5.1 コーディングエージェントの検出率 34 % の約 3 倍に相当します。

この意味するところは明白です。DeFi セキュリティの戦いは AI 対 AI の戦いとなっており、経済的には圧倒的に攻撃側に有利な状況となっています。少なくとも現時点では。

攻撃者は 8 USDC を担保として預け入れ、187 ETH（約 390,000 ドル）を持ち去りました。スマートコントラクトは設計通りに動作しました。オラクルもその役割を果たしました。しかし、誰かが USDC 用のスロットに BTC/USD の Chainlink 価格フィードを設定してしまったのです。そのたった一行の設定ミスが、正常に機能していたレンディング・プロトコルを「無料の現金自動払い機」に変えてしまいました。

DeFi セキュリティの新たな最前線へようこそ。ここでは、最も致命的な脆弱性は Solidity のバイトコードの中に隠れているのではなく、管理ダッシュボード、デプロイスクリプト、そしてパラメータファイルの中に潜んでいます。

2025 年、DeFi はスマートコントラクトのエクスプロイトにより 33 億ドルを失いました。攻撃を受けたプロトコルのほとんどが監査済みであり、中には複数回監査を受けたものもあったにもかかわらずです。2 月の 15 億ドルの Bybit 流出、4,200 万ドルの GMX エクスプロイト、そして数え切れないほどのリエントランシー攻撃は、不都合な真実を証明しました。従来のセキュリティ監査は必要ですが、十分ではありません。数学的な精度が求められる場合、エッジケースをテストするだけでは不十分です。それらを「証明」する必要があります。

これこそが、Sui Prover のオープンソース化が単なる GitHub のリリース以上の意味を持つ理由です。Asymptotic によって開発され、現在は Sui 開発者コミュニティに無償で提供されている Sui Prover は、飛行制御システムやプロセッサ設計の失敗を防ぐために使用されるのと同じ数学的手法である「形式検証」を、日常のスマートコントラクト開発にもたらします。わずかな見落とされたエッジケースが数億ドルの流出を招く可能性がある現状において、コードが正しく動作することを数学的に証明できる能力は、もはや贅沢品ではなく、必需品となりつつあります。

2025 年 2 月 21 日、北朝鮮のハッカーがドバイを拠点とする取引所 Bybit から、わずか約 30 分間で 15 億ドル の暗号資産を盗み出しました。これは史上最大の暗号資産窃盗事件であるだけでなく、もし Bybit が銀行であったなら、ギネス世界記録に登録されている史上最大の銀行強盗事件として記録される規模のものです。

この攻撃は、スマートコントラクトのバグを悪用したり、プライベートキーを総当たり攻撃（ブルートフォース）したりしたものではありませんでした。その代わりに、ハッカーはサードパーティのウォレットプロバイダーに所属する 1 人の開発者のノート PC を乗っ取り、数週間にわたって辛抱強く待機し、Bybit の従業員が日常的な内部送金に見える操作を承認する瞬間を狙って実行されました。何かがおかしいと誰かが気づいた時には、500,000 ETH が北朝鮮のラザルス・グループ（Lazarus Group）が制御する複雑なウォレットの迷宮へと消え去っていました。

これは、この事件がいかにして起こったのか、なぜ重要なのか、そして 2025 年における暗号資産セキュリティの現状について何を明らかにしているのかという物語です。

攻撃：忍耐と精度のマスタークラス​

Bybit のハッキングは、単なる強行突破ではありませんでした。それは数週間にわたって展開された外科手術のような作戦でした。

フェーズ 1：開発者の侵害​

2025 年 2 月 4 日、Safe{Wallet}（Bybit が多額の送金の安全を確保するために利用していた、広く普及しているマルチシグネチャ・ウォレットプラットフォーム）の開発者が、"MC-Based-Stock-Invest-Simulator-main" という一見正当な Docker プロジェクトをダウンロードしました。このファイルは、おそらく求人の機会や投資ツールを装ったソーシャルエンジニアリング攻撃を通じて届けられたと考えられます。

悪意のある Docker コンテナは直ちに攻撃者が制御するサーバーへの接続を確立しました。そこからハッカーは、開発者のワークステーションから AWS セッショントークン（Safe{Wallet} のクラウドインフラストラクチャへのアクセスを許可する一時的な認証情報）を抽出しました。

これらのトークンを使用することで、攻撃者は多要素認証を完全にバイパスしました。彼らは今、Safe{Wallet} の中核へとアクセスする鍵を手に入れたのです。

フェーズ 2：休止状態のコード​

攻撃者はすぐに動くのではなく、Safe{Wallet} のウェブインターフェースに巧妙な JavaScript コードを注入しました。このコードは Bybit を明確にターゲットとして設計されており、Bybit の従業員が Safe アカウントを開き、トランザクションを承認しようとしていることを検知するまで休止状態を保つようになっていました。

ここでの巧妙さは驚くべきものです。Safe{Wallet} アプリケーション全体は、他のすべてのユーザーに対しては通常通り機能していました。Bybit だけが標的にされていたのです。

フェーズ 3：強奪​

2025 年 2 月 21 日、Bybit の従業員は、コールドウォレット（安全なオフラインストレージ）からウォームウォレット（アクティブな取引のため）への日常的な送金プロセスを開始しました。これには、承認された担当者による複数の署名（マルチシグと呼ばれる標準的なセキュリティ慣行）が必要でした。

署名者がトランザクションを承認するために Safe{Wallet} を開いた際、インターフェースには正しい送金先アドレスが表示されているように見えました。しかし、悪意のあるコードはすでにコマンドを別のものに差し替えていました。従業員たちは知らず知らずのうちに、Bybit のコールドウォレット全体を空にするトランザクションを承認してしまったのです。

数分のうちに、約 15 億ドル 相当の 500,000 ETH が攻撃者の制御下にあるアドレスに流れ込みました。

技術的な悪用：Delegatecall​

鍵となった脆弱性は、Ethereum の delegatecall 関数でした。これは、あるスマートコントラクトが別のコントラクトのコードを自身のストレージコンテキスト内で実行することを可能にするものです。攻撃者は Bybit の署名者を騙して、ウォレットのコントラクトロジックを悪意のあるバージョンに変更させ、事実上ハッカーに完全な制御権を与えてしまいました。

これは Ethereum や Safe{Wallet} のコアプロトコルのバグではありませんでした。信頼された従業員がトランザクションを検証・承認する瞬間、つまり「人間レイヤー」に対する攻撃だったのです。

北朝鮮のラザルス・グループ：世界で最も収益を上げるハッカー集団​

攻撃から 24 時間以内に、ブロックチェーン調査員の ZachXBT は、このハッキングを北朝鮮のラザルス・グループに断定する証拠を Arkham Intelligence に提出しました。FBI は 2025 年 2 月 26 日にこの帰属を裏付けました。

ラザルス・グループ（TraderTraitor や APT38 としても知られる）は、北朝鮮の偵察総局の傘下で活動しています。彼らは個人の利益を求める犯罪集団ではありません。その収益が北朝鮮の核兵器や弾道ミサイル計画の資金源となる、国家が支援する活動です。

その数字は驚愕に値します：

• 2025 年だけで：北朝鮮のハッカーは 20.2 億ドル の暗号資産を窃盗
• Bybit の割合：15 億ドル（北朝鮮による 2025 年の全窃盗額の 74% がこの単一の攻撃によるもの）
• 2017 年以降：北朝鮮は 67.5 億ドル 以上の暗号資産を窃盗
• 2024 年対比：盗まれた金額は前年比 51% 増加

北朝鮮は、2025 年に世界中で盗まれた全暗号資産の 59% 、および全取引所侵害事件の 76% を占めています。他の追随を許さない圧倒的な脅威となっています。

暗号資産窃盗の産業化​

北朝鮮を際立たせているのは、その規模だけではなく、作戦の巧妙さです。

技術的悪用を凌駕するソーシャルエンジニアリング​

2025 年の主要なハッキング事件の大部分は、技術的な脆弱性ではなく、ソーシャルエンジニアリングを通じて実行されました。これは根本的な変化を表しています。ハッカーはもはや、主にスマートコントラクトのバグや暗号技術的な弱点を探しているわけではありません。彼らは「人」をターゲットにしています。

ラザルス・グループの工作員は、暗号資産企業の内部に IT 労働者として入り込んでいます。幹部になりすますこともあります。開発者にマルウェアを含む求人の案内を送ることもあります。Bybit への攻撃は、開発者が偽の株式投資シミュレーターをダウンロードしたことから始まりました。これは典型的なソーシャルエンジニアリングの手法です。

中国のランドリーネットワーク（The Chinese Laundromat）​

暗号資産を盗み出すことは、課題の半分に過ぎません。発覚することなく、それを使用可能な資金に換金することは、同じくらい複雑です。

北朝鮮は直接キャッシュアウトするのではなく、捜査官が「中国系コインランドリー（Chinese Laundromat）」と呼ぶ、地下銀行、OTC ブローカー、貿易ベースの洗浄仲介者からなる広大なネットワークにマネーロンダリングを外部委託しています。これらの主体は、複数のチェーン、法域、決済ルートにわたって盗まれた資産を洗浄します。

Bybit のハッキングから 1 か月も経たない 2025 年 3 月 20 日までに、CEO の Ben Zhou 氏は、ハッカーがすでに盗まれた ETH の 86.29% を、複数の仲介ウォレット、分散型取引所（DEX）、クロスチェーンブリッジを通じてビットコインに変換したと報告しました。大規模な盗難に続く 45 日間の洗浄サイクルは、予測可能なパターンとなっています。

こうした努力にもかかわらず、Zhou 氏は盗まれた資産の 88.87% が追跡可能であると指摘しました。しかし、「追跡可能」であることは「回収可能」であることを意味しません。資金は、米国や国際的な法執行機関と協力関係にない法域へと流れています。

Bybit の対応：攻撃下での危機管理​

侵害の発見から 30 分以内に、CEO の Ben Zhou 氏が指揮を執り、X（旧 Twitter）でリアルタイムの状況報告を開始しました。彼のメッセージは率直なものでした。「Bybit はソルベント（支払能力がある）です。今回のハッキングによる損失が回収できなくても、すべての顧客資産は 1 対 1 で裏付けられており、損失をカバーできます」

同取引所は 12 時間以内に 35 万件以上の出金リクエストを処理しました。これは、壊滅的な損失にもかかわらず、業務が通常通り継続されることをユーザーに示すシグナルとなりました。

緊急資金調達​

72 時間以内に、Bybit は Galaxy Digital、FalconX、Wintermute などのパートナーから緊急資金調達を行い、447,000 ETH を確保して予備資金を補充しました。Bitget は出金を滞りなく継続させるために 40,000 ETH を貸し付け、Bybit はこれを 3 日以内に返済しました。

サイバーセキュリティ企業の Hacken はプルーフ・オブ・リザーブ（準備金証明）の監査を実施し、Bybit の主要資産が 100% 以上の担保で裏付けられていることを確認しました。この透明性は、この規模の危機においては前例のないものでした。

バウンティプログラム（賞金制度）​

Zhou 氏は「Lazarus に対する宣戦布告」を表明し、凍結資産につながる情報に対して最大 10% の報酬を提供するグローバルなバウンティプログラムを開始しました。年末までに、Bybit は資金の追跡や回収に協力した貢献者に対し、218 万 USDT を支払いました。

市場の下した評価​

2025 年末までに、Bybit の世界的なユーザー数は 8,000 万人を超え、1 日あたりの取引高は 71 億ドルを記録し、暗号資産現物取引所で第 5 位にランクされました。この危機対応は、壊滅的なハッキングをいかに生き残るかというケーススタディとなりました。

2025 年：暗号資産の盗難額が 34 億ドルに達した年​

Bybit のハッキングは大きく報じられましたが、それはより広範なパターンの一部に過ぎませんでした。2025 年の暗号資産の総盗難額は 34 億ドルに達し、過去最高を記録、3 年連続の増加となりました。

主要な統計：

• 2023 年：20 億ドルの盗難
• 2024 年：22 億ドルの盗難
• 2025 年：34 億ドルの盗難

北朝鮮のシェアは、全暗号資産盗難の約半分から 60% 近くまで拡大しました。北朝鮮（DPRK）は、より少ないインシデントでより大きな盗難を成功させており、その効率性と巧妙さが増していることを示しています。

教訓：セキュリティはどこで失敗したのか​

Bybit のハッキングは、単一の取引所をはるかに超える重大な脆弱性を浮き彫りにしました。

サードパーティのリスクは死活問題​

Bybit 自体にセキュリティの不備があったわけではありません。不備があったのは Safe{Wallet} です。しかし、その結果を被ったのは Bybit でした。

暗号資産業界は複雑な依存チェーンの上に構築されています。取引所はウォレットプロバイダーに依存し、ウォレットプロバイダーはクラウドインフラに依存し、クラウドインフラは個々の開発者のワークステーションに依存しています。このチェーンのどこか一箇所でも侵害されれば、壊滅的な連鎖反応を引き起こす可能性があります。

コールドストレージだけでは不十分​

業界では長年、コールドウォレットがセキュリティの黄金基準とされてきました。しかし、Bybit の資金は盗まれた当時、コールドストレージに保管されていました。脆弱性は、資金を移動させるプロセス、つまりマルチシグが保護するために設計された「人間による承認ステップ」にありました。

送金がルーチン化すると、署名者は誤った安心感を抱き、承認を重要なセキュリティ上の決定ではなく、単なる形式的な手続きとして扱うようになります。Bybit への攻撃は、まさにこの行動パターンを突いたものでした。

UI（ユーザーインターフェース）は単一障害点​

マルチシグのセキュリティは、署名者が承認内容を検証できることを前提としています。しかし、取引の詳細を表示するインターフェースが改ざんされていれば、検証は無意味になります。攻撃者は署名者に一つのことを見せながら、別のことを実行させました。

署名前にシミュレーションを行い、従業員が承認前に実際の送金先をプレビューできるようにしていれば、この攻撃を防げた可能性があります。また、多額の出金に対して遅延を設定し、追加のレビュー時間を設けることも有効だったでしょう。

ソーシャルエンジニアリングは技術的セキュリティを凌駕する​

世界で最も洗練された暗号技術によるセキュリティを備えていても、たった一人の従業員が誤ったファイルをダウンロードするだけで、そのすべてをバイパスできてしまいます。暗号資産セキュリティの弱点は、技術的なものではなく、ますます人間的なものになっています。

規制および業界への影響​

Bybit のハッキングは、すでに規制の枠組みを再構築しつつあります。

以下の項目が義務化されることが予想されます：

• 鍵管理のためのハードウェアセキュリティモジュール（HSM）
• リアルタイムの取引監視と異常検知
• 定期的な第三者機関によるセキュリティ監査
• 強化された AML（マネーロンダリング防止）フレームワークと、多額送金時の取引遅延

セキュリティとコンプライアンスは、市場へのアクセスのための必須条件になりつつあります。強力な鍵管理、権限設計、信頼できるセキュリティフレームワークを実証できないプロジェクトは、銀行パートナーや機関投資家から遮断されることになるでしょう。

業界にとっての意味​

Bybit のハッキングは、不都合な真実を浮き彫りにしました。つまり、暗号資産のセキュリティモデルの強度は、その運用における最も弱いリンクと同じでしかないということです。

業界は、ゼロ知識証明、しきい値署名、セキュアエンクレーブといった暗号技術によるセキュリティに多額の投資を行ってきました。しかし、攻撃者が人間を騙して悪意のあるトランザクションを承認させることができれば、どれほど洗練された暗号技術も無意味になります。

取引所にとって、メッセージは明確です。セキュリティの革新は、テクノロジーの枠を超え、運用プロセス、サードパーティのリスク管理、継続的な従業員トレーニングにまで及ぶ必要があります。定期的な監査、共同の脅威インテリジェンスの共有、およびインシデント対応計画は、もはやオプションではありません。

ユーザーにとっても、教訓は同様に厳しいものです。最も洗練されたセキュリティを備えた最大の取引所でさえ、侵害される可能性があるということです。セルフカストディ、ハードウェアウォレット、分散型の資産保管は、利便性は劣るものの、依然として最も安全な長期戦略です。

結論​

北朝鮮の Lazarus Group は、暗号資産の窃盗を産業化しました。彼らは 2017 年以来 67 億 5,000 万ドル以上を盗み出しており、2025 年はこれまでで最も成功した年となっています。Bybit のハッキングだけで、1 回のオペレーションで 15 億ドルを奪ったことは、あらゆる諜報機関が羨むような能力を示しています。

暗号資産業界は、無限の忍耐力、高度な技術力、そして報復を恐れない国家支援のハッカーとの軍拡競争の真っ只中にあります。Bybit への攻撃が成功したのは、斬新なエクスプロイトによるものではなく、攻撃者がコードではなく人間こそが最も弱いリンクであることを理解していたためです。

業界が運用のセキュリティを暗号技術のセキュリティと同じ厳格さで扱うようにならない限り、これらの攻撃は続くでしょう。問題は、再び 10 億ドル規模のハッキングが起こるかどうかではなく、「いつ」起こるか、そして標的となった組織が Bybit と同じくらい効果的に対応できるかどうかです。

---

この記事は教育目的のみであり、財務アドバイスと見なされるべきではありません。暗号資産取引所やウォレットを利用する際は、常に自身で調査を行い、セキュリティを最優先してください。

スマートコントラクト監査における形式的検証​

形式的検証とは、数学的および論理ベースの技術を用いて、スマートコントラクトの正確性とセキュリティを証明することを指します。実際には、これにはプロパティベースのファズテストやシンボリック実行から、厳密な定理証明やモデル検査まで、さまざまな方法論が含まれます。その目的は、コントラクトが仕様を満たし、考えられるすべての入力と状態において悪用可能なバグを含まないことを保証することです。DeFi プロトコルには数十億ドルがロックされているという高いリスクを考慮すると、形式的手法はイーサリアムやその他のブロックチェーンプラットフォームにとってますます重要になっています。

従来のアプローチ: イーサリアムにおける初期の形式的手法には、Oyente や Mythril のようなシンボリック実行ツールや、Slither や Securify のような静的アナライザーが含まれていました。シンボリック実行は、シンボリックな入力を用いてプログラムのパスを探索し、問題 (例: リエントラシー、整数オーバーフロー) を検出します。一方、静的分析はルールベースのパターンマッチングを使用します。これらのツールは成功を収めてきましたが、限界もありました。例えば、Oyente は単純なコントラクトでさえ多くの誤報を出し、Slither のパターンベースの検出器はいくつかの偽陽性を生み出す可能性がありました。さらに、2023 年の研究では、現在のツールでは悪用可能なコントラクトのバグの 80% 以上 (特に複雑な「ビジネスロジック」のバグ) が見逃されていることが判明し、より堅牢な検証技術の必要性が浮き彫りになりました。

完全検証の可能性と課題: 理論上、形式的検証はすべての状態に対して不変条件を網羅的にチェックすることで、バグの不在を証明できます。Certora Prover や Ethereum Foundation の KEVM フレームワークのようなツールは、形式的仕様に対してスマートコントラクトを数学的に検証することを目指しています。例えば、Certora の「自動化された数学的監査人」は、仕様言語 (CVL) を使用して、ユーザー定義のルールを証明または反証します。しかし実際には、現実世界のコントラクトでプロパティを完全に証明することは、しばしば達成不可能であるか、非常に手間がかかります。検証のためにコードを単純化された形式に書き直す必要があったり、カスタム仕様を作成する必要があったり、ループや複雑な算術には手動で境界や抽象化が必要だったり、SMT ソルバーが複雑なロジックで頻繁にタイムアウトしたりします。Trail of Bits のエンジニアが指摘したように、「バグがないことを証明することは、通常、些細でないコードベースでは達成不可能です」。そして、それを達成するには、多くの場合、ユーザーの多大な介入と専門知識が必要です。このため、形式的検証ツールは伝統的に、コントラクト全体をエンドツーエンドで検証するのではなく、重要なコードの一部 (例: トークンの不変条件やコンセンサスアルゴリズムの検証) に限定的に使用されてきました。

Foundry のファズテストと不変条件テスト​

近年、完全な形式的証明に代わる実用的な代替手段として、プロパティベースのテストが登場しました。イーサリアムの人気開発フレームワークである Foundry は、ファズテストと不変条件テストを組み込みでサポートしています。これらの技術はテストカバレッジを大幅に向上させ、軽量な形式的検証と見なすことができます。Foundry のファズテストは、指定されたプロパティに違反しようと多数の入力を自動的に生成し、不変条件テストはこれを状態変化を伴う一連の操作に拡張します。

• ファズテスト: 特定の入力に対する単体テストを作成する代わりに、開発者は任意の入力に対して成立すべきプロパティや不変条件を指定します。その後、Foundry は何百、何千ものランダムな入力を生成して関数をテストし、プロパティが常に成立することを確認します。これにより、開発者が手動でテストしようと考えつかないようなエッジケースを捉えることができます。例えば、ファズテストでは、関数の戻り値が常に非負であることや、入力に関わらず特定の事後条件が真であることを表明 (assert) するかもしれません。Foundry のエンジンは、関数のシグネチャを分析し、エッジケースの値 (0, max uint など) を導入することで、プロパティを破る可能性のあるコーナーケースを突くインテリジェントなヒューリスティクスを使用します。アサーションが失敗した場合、Foundry はプロパティに違反する反例入力を報告します。

• 不変条件テスト: Foundry の不変条件テスト (別名ステートフルファジング) はさらに進んで、複数の関数呼び出しと状態遷移を連続して実行します。開発者は、コントラクトのライフタイムを通じて真であるべき不変条件関数 (例: 総資産 = ユーザー残高の合計) を記述します。Foundry はその後、ランダムな呼び出しシーケンス (ランダムな入力付き) を生成して多くの可能な使用シナリオをシミュレートし、不変条件が真であり続けることを定期的にチェックします。これにより、特定の操作シーケンスの後にのみ現れる複雑なバグを発見できます。本質的に、不変条件テストはコントラクトの状態空間をより徹底的に探索し、有効なトランザクションのいかなるシーケンスも、述べられたプロパティに違反できないことを保証します。

Foundry が重要な理由: Foundry はこれらの高度なテスト技術をアクセスしやすくしました。ファジングと不変条件の機能は開発者のワークフローにネイティブであり、特別なハーネスや外部ツールは不要で、テストは単体テストと並行して Solidity で記述されます。Rust ベースのエンジンのおかげで、Foundry は何千ものテストを迅速に (並列化して) 実行し、不変条件違反に対する詳細な失敗トレースを提供できます。開発者からは、Foundry のファザーは使いやすく高性能であり、わずかな設定 (例: 反復回数の設定や入力を制約するための仮定の追加) しか必要ないと報告されています。Foundry のドキュメントにある簡単な例は、divide(a,b) 関数のファズテストで、vm.assume(b != 0) を使用して自明な無効入力を避け、result * b <= a のような数学的な事後条件を表明します。このようなテストを何千ものランダムな (a,b) ペアで実行することで、Foundry は手動の推論では見つけるのが難しいエッジケース (オーバーフローの境界など) を迅速に発見するかもしれません。

比較: Foundry のアプローチは、コミュニティにおける先行研究に基づいています。Trail of Bits の Echidna ファザーは、イーサリアム向けの初期のプロパティベースのテストツールでした。Echidna も同様に、ブール値を返す Solidity 関数として表現された不変条件の違反を見つけるためにランダムなトランザクションを生成します。これは「インテリジェントな」入力生成 (カバレッジガイド付きファジングを組み込む) で知られており、多くのバグを発見するために使用されてきました。実際、セキュリティ研究者は Echidna のエンジンが非常に効果的であると指摘しています – 「Trail of Bits の Echidna は、そのインテリジェントな乱数選択により、最高のファザーです」 – ただし、Foundry の統合されたワークフローは、開発者にとってテストの記述をよりシンプルにします。実際には、Foundry のファズテストは、従来の単体テストを補完するものとして、安全な Solidity 開発のための新しい**「最低限の基準」**と見なされることがよくあります。これは (ランダム化されており網羅的ではないため) バグの不在を証明することはできませんが、広範な入力と状態の組み合わせをカバーすることで、信頼性を大幅に向上させます。

ファジングを超えて: 形式的証明と高度なツール​

ファジングと不変条件は多くの問題を捉えますが、より強力な形式的手法が使用されるケースもあります。モデル検査と定理証明は、望ましいプロパティを形式論理で指定し、自動化された証明器を使用してコントラクトコードに対してそれらをチェックすることを含みます。Certora Prover (最近オープンソース化) は、このカテゴリの著名なツールです。これにより、開発者はドメイン固有言語 (CVL) でルールを記述し、コントラクトがそれらのルールに違反していないかを自動的にチェックできます。Certora は、MakerDAO や Compound のようなプロトコルで重要な不変条件を検証するために使用されてきました。例えば、MakerDAO の「DAI 債務不変条件」バグ (4 年間気づかれなかった微妙な会計上の不整合) を特定しました。特筆すべきは、Certora のエンジンが現在複数のプラットフォーム (EVM, Solana の VM, eWASM) をサポートしており、2025 年にオープンソース化することで、イーサリアム、Solana、Stellar で産業グレードの形式的検証を無料で利用可能にしたことです。この動きは、形式的証明が資金力のあるチームだけの贅沢であってはならないという認識を示しています。

その他の形式的ツールには、ランタイム検証アプローチ (例: イーサリアムの KEVM セマンティクス、または Move ベースのチェーン用の Move Prover) があります。特に Move Prover は、Move 言語 (Aptos および Sui ブロックチェーンで使用) に組み込まれています。これにより、コードと並行して形式的仕様を記述でき、リンターや型チェッカーと同様のユーザーエクスペリエンスで特定のプロパティを自動的に証明できます。この緊密な統合により、これらのプラットフォームの開発者が開発の一部として形式的検証を使用する際の障壁が低くなります。

まとめ: 今日のスマートコントラクト監査は、これらの方法論を融合させています。ファジングと不変条件テスト (Foundry と Echidna が代表例) は、使いやすさと一般的なバグの捕捉における有効性から広く採用されています。シンボリック実行と静的アナライザーは、既知の脆弱性パターンを迅速にスキャンするために依然として役立っています (Slither のようなツールはしばしば CI パイプラインに統合されます)。一方、形式的検証ツールは成熟し、チェーンを越えて拡大していますが、その複雑さから、通常は特定の重要なプロパティや専門の監査会社によって使用されます。実際には、多くの監査はこれらのアプローチを組み合わせています。例えば、ファザーを使用してランタイムエラーを見つけ、静的ツールで明らかな間違いを指摘し、形式的仕様チェックで「トークン残高が総供給量を超えない」といった主要な不変条件を確認します。

大規模言語モデルによる AI 支援監査​

OpenAI の GPT-3/4 (ChatGPT) や Codex のような大規模言語モデル (LLM) の登場は、スマートコントラクト分析に新しいパラダイムをもたらしました。これらのモデルは、膨大な量のコードと自然言語でトレーニングされており、プログラムの振る舞いについて推論し、コードを説明し、パターン認識と「常識」的な知識によって特定の脆弱性を検出することさえできます。問題は、AI がスマートコントラクト監査を補強、あるいは自動化できるかということです。

LLM ベースの脆弱性分析ツール​

LLM をスマートコントラクト監査に適用するいくつかの研究努力とプロトタイプツールが登場しています。

• OpenAI Codex / ChatGPT (汎用モデル): 初期の実験では、単に GPT-3 や Codex にコントラクトコードをプロンプト入力し、潜在的なバグを尋ねるだけでした。開発者たちは、ChatGPT がいくつかのよく知られた脆弱性パターンを特定し、修正案を提案することさえできることを見出しました。しかし、応答は当たり外れがあり、信頼できるほど包括的ではありませんでした。最近の学術評価では、脆弱性検出のために ChatGPT に単純なプロンプトを入力することは、ベンチマークデータセットにおいて*「ランダムな予測と比較して有意に良い結果をもたらさなかった」*と指摘されています。つまり、モデルが適切に誘導されない場合、存在しない問題を幻覚 (hallucinate) したり、実際の脆弱性を見逃したりする可能性があります。これは、有用な結果を得るためには、慎重に設計されたプロンプトやファインチューニングが必要であることを浮き彫りにしました。

• AuditGPT (2024): これは、イーサリアムコントラクトの ERC 標準準拠をチェックするために ChatGPT (GPT-3.5/4) を特別に活用した学術ツールです。研究者たちは、多くの ERC20/ERC721 トークンコントラクトが標準の微妙なルールに違反していること (これがセキュリティや互換性の問題につながる可能性がある) を観察しました。AuditGPT は、監査を小さなタスクに分割し、各ルールタイプに特化したプロンプトを設計することで機能します。その結果は印象的でした。実際のコントラクトでのテストで、AuditGPT は*「418 件の ERC ルール違反を成功裏に特定し、偽陽性は 18 件しか報告しなかった」*とされ、高い精度を示しました。実際、この論文は、AuditGPT が ERC 準拠のバグを見つける上で、専門の監査サービスを上回り、より低コストであったと主張しています。これは、(標準ルールのリストを強制するような) よく定義された狭いドメインでは、優れたプロンプトを持つ LLM が驚くほど効果的かつ正確であり得ることを示唆しています。

• LLM-SmartAudit (2024): 別の研究プロジェクトである LLM-SmartAudit は、Solidity コードを監査するためにマルチエージェント対話システムを使用するという、より広範なアプローチを取っています。これは、複数の特化した GPT-3.5/GPT-4 エージェント (例: 正確性に焦点を当てる「監査人」、悪用方法を考える「攻撃者」) を設定し、互いに対話させてコントラクトを分析します。彼らの評価では、LLM-SmartAudit は広範な脆弱性を検出することができました。特筆すべきは、従来のツールとの比較テストで、GPT-3.5 ベースのシステムが最高の総合再現率 (74%) を達成し、テストしたすべての従来の静的およびシンボリックアナライザーを上回ったことです (次点は Mythril の 54% の再現率でした)。また、テストスイートに含まれる 10 種類の脆弱性をすべて見つけることができました (一方、各従来ツールはいくつかのカテゴリで苦戦しました)。さらに、GPT-4 に切り替えて分析を集中させる (彼らがターゲット分析モードと呼ぶもの) ことで、Slither や Mythril のようなツールが完全に見逃した複雑な論理的欠陥を検出できました。例えば、現実世界の DeFi コントラクトのセットに対して、LLM ベースのアプローチは何百ものロジックバグを発見しましたが、静的ツールはそれらの問題を*「検出する上で効果を示さなかった」*とされています。これらの結果は、LLM が従来のアナライザーのパターンマッチングの範囲を超える微妙なバグを捉える可能性を示しています。

• Prometheus (PromFuzz) (2023): ハイブリッドなアプローチは、LLM を使用して他の技術を誘導することです。一つの例は PromFuzz で、GPT ベースの「監査人エージェント」を使用してコードの疑わしい領域を特定し、その後、不変条件チェッカーを自動的に生成してファジングエンジンに供給します。本質的に、LLM は一次分析 (良性および攻撃者の両方の視点から) を行い、ファズテストを脆弱性の可能性が高い箇所に集中させます。評価では、このアプローチは非常に高いバグ発見率を達成しました – 例えば、特定のベンチマークセットで偽陽性ゼロで 86% 以上の再現率 – これは、スタンドアロンのファザーや以前のツールを大幅に上回ります。これは有望な方向性です。AI を使用してファジングのような古典的な技術をオーケストレーションし、強化することで、両方の長所を組み合わせることです。

• その他の AI ツール: コミュニティでは、他にもさまざまな AI 支援監査のコンセプトが見られます。例えば、Trail of Bits の「Toucan」プロジェクトは、OpenAI Codex を監査ワークフローに統合しました (その発見については後述)。一部のセキュリティスタートアップも AI 監査人を宣伝しており (例: 「ChainGPT Audit」サービス)、通常は GPT-4 をカスタムプロンプトでラップしてコントラクトをレビューします。オープンソースの愛好家は、Solidity のスニペットを受け取って潜在的な問題をアウトプットする ChatGPT ベースの監査ボットをフォーラムで作成しています。これらの多くは実験的なものですが、一般的な傾向は明らかです。AI は、自動化されたコードの説明やドキュメント生成から、脆弱性の検出、さらには修正案の提案まで、セキュリティレビュープロセスのあらゆるレベルで探求されています。

LLM 監査人の能力と限界​

LLM は、スマートコントラクト監査において注目すべき能力を示しています。

• 広範な知識: GPT-4 のような LLM は、無数のコードと脆弱性についてトレーニングされています。一般的なセキュリティの落とし穴 (リエントラシー、整数オーバーフローなど) や、過去のいくつかのエクスプロイトについても「知って」います。これにより、バグを示す可能性のあるパターンを認識し、ドキュメントからベストプラクティスを思い出すことができます。例えば、ERC-20 の transferFrom がアローワンスをチェックすべきことを覚えており (そのようなチェックがないことを違反としてフラグ付けするかもしれません)。既知のパターンのみをフラグ付けする静的ツールとは異なり、LLM は新しいコードに推論を適用し、ツール開発者によって明示的にコーディングされていない問題を推測できます。

• 自然な説明: AI 監査人は、潜在的な問題について人間が読める説明を提供できます。これは開発者体験にとって非常に価値があります。従来のツールはしばしば解読に専門知識を要する不可解な警告を出力しますが、GPT ベースのツールは平易な英語でバグを説明し、修正案を提案することさえできる段落を生成できます。例えば、AuditGPT は ERC ルール違反をフラグ付けするだけでなく、なぜコードがルールに違反したのか、そしてその影響が何であるかを説明しました。これは、経験の浅い開発者をセキュリティコンセプトに慣れさせるのに役立ちます。

• 柔軟性: プロンプトエンジニアリングにより、LLM は異なる側面に焦点を当てたり、カスタムのセキュリティポリシーに従うように指示されたりすることができます。固定されたルールのセットに限定されません – プロパティやパターンを言葉で説明できれば、LLM はそれをチェックしようと試みることができます。これにより、独自の不変条件やロジックを持つ可能性のある新しいプロトコルの監査に魅力的になります (カスタムの静的分析をゼロから書くのは非現実的でしょう)。

しかし、重大な課題と信頼性の問題も観察されています。

• 推論の限界: 現在の LLM は、セキュリティ分析に必要な複雑な論理的推論に苦労することがあります。Trail of Bits は、*「モデルは、コントラクトの所有権、リエントラシー、関数間の関係など、特定の高レベルの概念についてうまく推論することができません」*と報告しました。例えば、GPT-3.5/4 はリエントラシーが理論上何かを理解しているかもしれませんが (そしてそれを説明することさえできるかもしれませんが)、関数をまたいだ呼び出しシーケンスと状態変化を理解する必要がある場合、リエントラシーの脆弱性を認識できないかもしれません。モデルはまた、複数コントラクト間の相互作用や時間依存のロジックを含む脆弱性を見逃す可能性もあります。なぜなら、それらは単一のコードスニペット分析の範囲を超えるからです。

• 偽陽性とハルシネーション: 大きな懸念は、LLM が自信に満ちたように聞こえるが、誤った結論を出す可能性があることです。監査において、「ハルシネーション」とは、実際には存在しない脆弱性をフラグ付けしたり、コードを誤解したりすることかもしれません。Trail of Bits の Codex (GPT) を用いた実験では、より大規模な現実世界のコントラクトにスケールアップするにつれて、「偽陽性とハルシネーションの率が非常に高くなり」、監査人をあまりにも多くの偽の報告で遅らせるほどになったことがわかりました。この予測不可能性は問題です – あまりにも頻繁にオオカミ少年を叫ぶツールは、開発者に信頼されません。AuditGPT が偽陽性を低く抑えることに成功したこと (何百もの発見のうち 18 件のみ) は心強いですが、それは制約されたドメインでのことでした。汎用的な使用では、AI の発見をフィルタリングするために、慎重なプロンプト設計や、おそらく人間のレビューのループが必要です。

• コンテキストの限界: LLM にはコンテキストウィンドウの制限があり、一度に「見える」コードの量に限りがあります。複雑なコントラクトはしばしば複数のファイルと何千行にも及びます。AI がコードベース全体を取り込めない場合、重要な関連性を見逃す可能性があります。コードスライシング (コントラクトをチャンクで供給する) のような技術が使用されますが、それらはより広い視野を失うリスクがあります。LLM-SmartAudit チームは、GPT-3.5 の 4k トークン制限では、より大きなコンテキストを持つ GPT-4 に切り替えるまで、いくつかの大規模な現実世界のコントラクトを分析できなかったと指摘しました。それでも、分析を部分に分けることは、システム全体を考慮した場合にのみ現れるバグを見落とす原因となる可能性があります。これにより、(複数の相互作用するコントラクトを持つ) プロトコル全体の AI 分析は、現時点では真の課題となっています。

• 統合とツール: AI 監査人を取り巻く堅牢な開発者向けツールが不足しています。LLM 分析を実行することは、リンターを実行するほど簡単ではありません。モデルへの API 呼び出し、プロンプトエンジニアリングの処理、レート制限、AI の応答の解析などが含まれます。ある監査チームが述べたように、「LLM を従来のソフトウェアと統合するためのソフトウェアエコシステムはあまりにも未熟で、すべてが面倒です」。AI 監査人を CI パイプラインに継続的にデプロイし、その不確実性を管理するための既製のフレームワークは事実上存在しません。これは徐々に改善されていますが (一部のプロジェクトでは、コードレビューに GPT-4 を使用する CI ボットを模索しています)、まだ初期段階です。さらに、AI が特定の結果を出した理由をデバッグすることは困難です – 決定論的なツールとは異なり、モデルが何かをフラグ付けしたり見逃したりするに至ったロジックを簡単に追跡することはできません。

• コストとパフォーマンス: GPT-4 のような大規模モデルの使用は高価であり、遅くなる可能性があります。AI 監査を CI/CD パイプラインに組み込みたい場合、コントラクトごとに数分が追加され、大規模なコードに対してはかなりの API コストが発生する可能性があります。ファインチューニングされたモデルやオープンソースの LLM はコストを軽減できますが、GPT-4 ほど高性能ではない傾向があります。コードセキュリティのためのより小規模で特化したモデルに関する研究が進行中ですが、現在のところ、最高の結果は大規模なプロプライエタリモデルから得られています。

要約すると、LLM 支援監査は有望ですが、万能薬ではありません。 AI がテストを生成したり、特定の側面を分析したりするのを助けるハイブリッドなアプローチが見られますが、監査全体をエンドツーエンドで行うわけではありません。例えば、AI が潜在的な不変条件やリスクのある領域を提案し、それを人間や別のツールが調査するかもしれません。あるセキュリティエンジニアが述べたように、推論のギャップや統合のハードルを考えると、この技術はまだ重要なタスクで人間の監査人を置き換える準備ができていません。しかし、それはすでに有用なアシスタントになることができます – 従来のツールが及ばない場合に*「不完全なものが何もないよりはるかに良いかもしれない」*のです。

さまざまなツールチェーンの精度と信頼性​

議論されたさまざまな監査アプローチの精度、カバレッジ、信頼性を比較することは有益です。以下は、研究および業界の評価からの知見の要約です。

• 静的分析ツール: Slither のような静的アナライザーは、迅速なフィードバックと使いやすさで評価されています。これらは通常、高い適合率を持ちますが、再現率は中程度です – つまり、報告される問題のほとんどは真の問題ですが (設計上、偽陽性は少ない)、特定のクラスの脆弱性しか検出しません。2024 年のベンチマーク研究 (LLM-SmartAudit の RQ1) では、Slither がテストスイート内の既知の脆弱性の約 46% を捕捉したことがわかりました。Mythril (シンボリック実行) はわずかに優れており、54% の再現率でした。各ツールは特定のバグタイプに強みを持っていましたが (例: Slither は算術問題や tx.origin の使用を見つけるのが非常に得意で、シンボリックツールは単純なリエントラシーシナリオを見つけるのに優れています)、どれも包括的なカバレッジを持っていませんでした。Slither のような成熟したツールの偽陽性は比較的低く、開発者は*「最小限の誤報と迅速な実行 (コントラクトあたり 1 秒未満)」*を宣伝しており、CI での使用に適しています。それでも、静的ツールはコードが複雑なパターンを使用している場合に誤動作する可能性があり、実際には処理されているエッジケースをフラグ付けしたり、既知のアンチパターンに一致しない深いロジックバグを見逃したりすることがあります。

• ファジングとプロパティテスト: Foundry のファズ/不変条件テストや Trail of Bits の Echidna のようなファザーは、ランタイムエラーや不変条件違反を見つけるのに非常に効果的であることが証明されています。これらのツールは、バグが報告された場合 (アサーションが失敗した場合)、それが実際の反例実行であるという意味で、偽陽性がほぼゼロである傾向があります。トレードオフは偽陰性にあります – バグがテストされた入力空間や実行回数内で現れない場合、見過ごされる可能性があります。カバレッジは、ファザーが状態空間をどれだけうまく探索するかに依存します。十分な時間と優れたヒューリスティクスがあれば、ファザーは静的分析が見逃した多くの高深刻度のバグを発見してきました。例えば、Echidna は、形式的検証の努力を要した MakerDAO と Compound のバグを迅速に再現することができました。しかし、ファジングはすべてのロジックミスを見つけることを保証するものではありません。コントラクトがより複雑になるにつれて、ファザーはより深い状態に到達するために追加の不変条件を記述したり、より賢い検索戦略を使用したりする必要があるかもしれません。メトリクスの観点から、ファジングには単一の「再現率」の数値はありませんが、逸話的な証拠によれば、重要な不変条件は、もし破れるのであれば、通常ファザーによって破られることができます。見つかったものに対する信頼性は高いですが (偽の報告に対する手動のトリアージは不要)、ファズテストに合格したことが正確性の証明ではないことを覚えておく必要があります – それは単に信頼性の向上です。

• 形式的検証ツール: 適用可能な場合、形式的検証は最高の保証を提供します – 証明が成功すれば、状態の 100% がプロパティを満たすことを意味します。精度の観点からは、証明できるプロパティに対しては事実上完璧 (健全かつ完全) です。ここでの最大の問題は、結果の精度ではなく、使用の難しさと範囲の狭さです。形式的ツールは、実際には偽陰性を持つこともあります。複雑さのために真のプロパティを証明できない場合があり (結果なしまたはタイムアウトとなり、これは偽陽性ではありませんが、実際には安全なものを検証できないことを意味します)。また、仕様のエラーを持つこともあり、ツールが意図したプロパティではないものを「証明」してしまうことがあります (ユーザーエラー)。実際の監査では、形式的手法はいくつかの重要なバグを捉えてきました (Certora の成功例には、微妙な SushiSwap のバグや PRBMath ライブラリの問題をデプロイ前に捉えたことが含まれます)。しかし、その実績は、それらがどれだけ包括的に適用されるかが稀であることによって制限されています – Trail of Bits が指摘したように、「ファジングによって見つかった多くのバグとは対照的に、形式的検証のみによって発見された公開された問題を見つけるのは困難でした」。したがって、形式的検証は成功した場合は非常に信頼性が高いですが、ツールチェーン全体のカバレッジへの影響は、必要な労力と専門知識によって制約されます。

• LLM ベースの分析: AI 監査人の精度は現在、新しい技術 (および新しいモデル) が急速に限界を押し上げているため、変動する目標です。いくつかのデータポイントを拾うことができます。

• ERC ルールに焦点を当てた AuditGPT システムは、非常に高い適合率 (偽陽性数で約 96%) を達成し、静的ツールや人間が見落とした何百もの問題を発見しました。しかし、これは構造化されたプロンプトを持つ狭いドメインでのことでした。ChatGPT が任意の脆弱性ハンティングで 96% の精度を持つと一般化すべきではありません – 制御された設定の外では、そのパフォーマンスは低くなります。

• より広範な脆弱性検出において、LLM-SmartAudit (GPT-3.5) は、中程度の偽陽性率でベンチマークにおいて約 74% の再現率を示し、これは単一の従来ツールよりも優れていました。特化したプロンプトを持つ GPT-4 (TA モード) にアップグレードすると、大幅に改善されました – 例えば、1,400 の現実世界の脆弱性のセットに対して、GPT-4 エージェントは特定のイシューの約 48% と複雑なロジックイシューの約 47% を発見しましたが、Slither/Mythril/Conkas はそれぞれそれらの特定の複雑なイシューを約 0% (なし) しか見つけませんでした。これは、LLM が静的分析が完全に見逃すタイプのバグにカバレッジを劇的に拡大できることを示しています。一方で、LLM はイシューの半分以上を見つけられなかったため (したがって、かなりの偽陰性もあります)、報告したものの中にどれだけの偽陽性があったかは明らかではありません – この研究は適合率よりも再現率に焦点を当てていました。

• Trail of Bits の Codex/GPT-4 「Toucan」 実験は、信頼性の問題を示しています。当初、小さな例では、Codex は慎重なプロンプトで既知の脆弱性 (所有権の問題、リエントラシー) を特定できました。しかし、スケールアップを試みるとすぐに、一貫性のない誤った結果に遭遇しました。彼らは*「平均的なサイズのコードでさえ失敗の数が多かった」と報告し、予測が困難でした。最終的に、彼らは GPT-4 (2023 年初頭時点) はインクリメンタルな改善に過ぎず、関数間のフローに関する推論のような「重要な機能が欠けている」と結論付けました。その結果、AI は静的ツールからの偽陽性を実質的に減らすことはなく*、監査ワークフローを確実に高速化することもしませんでした。言い換えれば、汎用 LLM の監査人としての現在の信頼性は、その試行においてプロの監査人によって不十分と見なされました。

まとめると、各ツールチェーンには異なる強みがあります。

• 静的ツール: 既知の問題の迅速な検出に信頼性があります。ノイズが少なく、しかしバグの種類は限定的です (ベンチマークでの再現率は中程度で約 40–50%)。
• ファズ/不変条件テスト: 非常に高い適合率 (偽のアラートはほとんどなし) で、機能的および状態依存のバグを見つけるのに強いです。カバレッジは広い可能性がありますが、保証されていません (単純なメトリクスはなく、時間と不変条件の質に依存します)。十分なガイダンスがあれば、形式的証明が見つけるであろう同じバグをしばしば見つけます。
• 形式的検証: 特定のプロパティに対する絶対的な正確性のゴールドスタンダードです。成功裏に適用されれば、それらのプロパティに対しては実質的に 100% の再現率/適合率です。しかし、実際には狭い問題に限定され、かなりの労力を必要とします (まだ完全な監査のためのワンボタンソリューションではありません)。
• AI (LLM) 分析: 潜在的に高いカバレッジ – 他のツールが見逃したカテゴリを含むバグを見つけることができます – しかし、適合率は変動します。特化した設定では、(AuditGPT が ERC チェックで示したように) 適合率と網羅性の両方を兼ね備えることができます。慎重な制約がなければ、広範な網を投げかけ、結果を人間が検証する必要があります。脆弱性検出における ChatGPT の「平均的な」精度は目覚ましいものではありませんが (ある研究では推測に近い)、LLM を使用した最高のエンジニアリングシステムは、従来のツールを超えるパフォーマンスを発揮しています。AI の出力をより信頼できるものにするための活発な研究があります (例: 複数のエージェントに相互検証させる、または LLM と静的推論を組み合わせて AI の結論を再確認する)。

アプローチを組み合わせることで最良の結果が得られることは注目に値します。例えば、Slither を実行し (ノイズなしで手軽な問題を捉えるため)、次に Foundry/Echidna を使用してより深い振る舞いをファズし、おそらく LLM ベースのツールを使用して考慮されていないパターンや不変条件をスキャンするかもしれません。それぞれが他のツールの死角をカバーします。

現実世界での採用における課題と限界​

実際には、形式的検証や AI ツールを開発ワークフローに採用するには、実用的な課題が伴います。いくつかの主要な問題は次のとおりです。

• 開発者体験と専門知識: 従来の形式的検証には急な学習曲線があります。形式的仕様 (CVL, Coq, Move の仕様言語など) を書くことは、コードを書くことよりも数学的な証明を書くことに似ています。多くの開発者はこの背景を欠いており、形式的手法の専門家は不足しています。対照的に、Foundry でのファジングや Solidity での不変条件の記述ははるかにアクセスしやすいです – それは追加のテストを書くように感じられます。これが、イーサリアムコミュニティで形式的証明よりもファズテストが急速に普及した大きな理由です。Trail of Bits チームは、ファジングは多くの場合、形式的手法よりも**「同様の結果を生み出すが、スキルと時間は大幅に少なくて済む」**と明示的に述べています。したがって、形式的検証は異なるバグを捉えることができますが、多くのチームはより少ない労力で十分な結果を得られる簡単なアプローチを選択します。

• 開発ワークフローへの統合: ツールが広く採用されるためには、CI/CD パイプラインや日常のコーディングに適合する必要があります。Slither のようなツールはここで輝きます – それは*「CI/CD セットアップに簡単に統合でき、自動化を合理化し、開発者を支援します。」* 開発者は Slither や Mythril を GitHub Action に追加し、問題が見つかった場合にビルドを失敗させることができます。Foundry のファズテストは、毎回 forge test の一部として実行できます。不変条件テストは、CloudExec のようなツールを使用してクラウドで継続的に実行することもでき、失敗は fuzz-utils を使用して自動的に単体テストに変換できます。これらの統合により、開発者は迅速なフィードバックを得て、反復作業を行うことができます。対照的に、Certora Prover のようなものは、歴史的に別のプロセスとして (または外部の監査チームによって) 実行され、結果を出すのに数時間かかる場合がありました – これは毎回のコミットで実行するようなものではありません。AI ベースのツールも統合のハードルに直面しています。API を呼び出し、その出力を CI で決定論的に処理することは簡単ではありません。また、セキュリティとプライバシーの問題もあります – 多くの組織は、分析のために独自のコントラクトコードをサードパーティの AI サービスに送信することに不安を感じています。セルフホストの LLM ソリューションは、まだ大手クラウド API ほど強力ではないため、これは AI 監査人の CI 採用における難点です。

• 偽陽性とノイズ: 多くの偽陽性や低深刻度の発見を報告するツールは、開発者の信頼を低下させる可能性があります。静的アナライザーは過去にこれで苦労してきました – 例えば、一部のツールの初期バージョンは、ユーザーに警告の洪水をもたらし、その多くは無関係でした。シグナルとノイズのバランスは非常に重要です。Slither は最小限の誤報で賞賛されていますが、Securify のようなツール (その研究形態では) はしばしば手動でのフィルタリングが必要な多くの警告を生成しました。LLM は、議論したように、適切にターゲットを絞らないとノイズを生成する可能性があります。これが、現在 AI の提案が通常、絶対的なものではなく助言として受け取られる理由です。チームは、別のセキュリティチームや監査の文脈で実行される場合に、ノイズの多いツールを採用する可能性が高くなりますが、日常的な使用では、開発者は明確で実行可能な結果を低ノイズで提供するツールを好みます。理想は、仮説ではなく、明確なバグに対してのみ**「ビルドを失敗させる」**ことです。その信頼性を達成することは、特に AI ツールにとって、継続的な課題です。

• スケーラビリティとパフォーマンス: 形式的検証は計算集約的になる可能性があります。前述のように、ソルバーは複雑なコントラクトでタイムアウトする可能性があります。これにより、大規模なシステムへのスケーリングが困難になります。1 つのプロパティを検証するのに数時間かかる場合、コードの変更ごとに数十のプロパティをチェックすることはありません。ファズテストもスケーラビリティの限界に直面します – 巨大な状態空間や多くのメソッドを持つコントラクトを組み合わせ的に探索するのは遅くなる可能性があります (ただし、実際にはファザーはバックグラウンドや夜間に実行して探索を深めることができます)。AI モデルには固定のコンテキストサイズがあり、モデルの容量を増やすのは高価です。GPT-4 の 128k トークンのコンテキストは恩恵ですが、それに数百キロバイトのコントラクトコードを供給するのはコストがかかり、非常に大規模なプロジェクトにはまだ十分ではありません (多くのコントラクトを持つ複雑なプロトコルを想像してみてください – それを超える可能性があります)。また、マルチチェーンのスケーリングもあります。プロジェクトが異なるチェーン上のコントラクト間の相互作用 (イーサリアム ↔ 別のチェーン) を含む場合、そのクロスチェーンロジックを検証または分析することはさらに複雑で、現在のツールの範囲を超える可能性があります。

• 人間の監督と検証: 最終的には、ほとんどのチームは最終的な承認のために専門の人間の監査人に依存しています。自動化されたツールは補助であり、代替ではありません。これらのすべてのツールの 1 つの限界は、既知のプロパティやパターンの範囲内で動作することです。まったく新しいタイプのバグや、DeFi プロトコルの設計における微妙な経済的欠陥を見逃す可能性があります。人間の監査人は、直感と経験を用いて、攻撃者がシステムにどのようにアプローチするかを、ツールが明示的にプログラムされていない方法で検討します。コントラクトがすべての自動チェックに合格したが、後で人間がビジネスロジックや創造的な攻撃ベクトルに脆弱性を見つけたケースがありました。したがって、課題は誤った安心感を避けることです – 開発者は形式的ツールと AI の出力を正しく解釈し、「問題は見つかりませんでした」がコードが 100% 安全であることを意味すると思い込んではなりません。

• 仕様とテストの維持: 特に形式的検証において、1 つの実用的な問題は仕様のドリフトです。仕様 (不変条件、ルールなど) は、コードが進化するにつれて古くなる可能性があります。コードとその形式的仕様が同期していることを確認することは、簡単な管理タスクではありません。開発者が注意を怠ると、証明は単にコードの実際の要件にもはや関連しないものを証明しているために「合格」するかもしれません。同様に、不変条件テストは、システムの期待される動作が変化するにつれて更新する必要があります。これには、すべてのチームが持っているわけではない不変条件駆動開発の文化が必要です (ただし、それを奨励する動きはあります)。

要約すると、主な限界は技術の生の能力よりも人とプロセスです。形式的および AI 支援の手法はセキュリティを大幅に向上させることができますが、開発者のワークフローとスキルセットに適合する方法で展開する必要があります。心強いことに、不変条件駆動開発 (初日から重要な不変条件を書き留める) のようなトレンドが勢いを増しており、ツールは高度な分析をよりプラグアンドプレイにするために徐々に改善されています。主要なツール (例: Certora Prover) のオープンソース化や、人気のあるフレームワーク (Foundry) へのファジングの統合は、障壁を下げています。時間とともに、「平均的な開発者」ができることと「博士号を持つ研究者」ができることのギャップは、これらの強力な検証技術を使用する点で狭まると予想されます。

オープンソース vs 商用監査ツール​

スマートコントラクトセキュリティツールの状況には、オープンソースプロジェクトと商用サービスの両方が含まれます。それぞれに役割があり、しばしば互いに補完し合います。

• オープンソースツール: イーサリアムエコシステムで広く使用されている監査ツールの大部分はオープンソースです。これには、Slither (静的アナライザー)、Mythril (シンボリック実行)、Echidna (ファザー)、Manticore (シンボリック/コンコリック実行)、Securify (ETH Zurich のアナライザー)、Solhint/Ethlint (リンター)、そしてもちろん Foundry 自体が含まれます。オープンソースツールが好まれる理由はいくつかあります。(1) 透明性 – 開発者はツールがどのように機能するかを見ることができ、悪意のあるものや隠されたものがないことを信頼できます (オープンなエコシステムでは重要です)。(2) コミュニティの貢献 – ルールや機能は広範なコミュニティによって追加されます (例えば、Slither には多くのコミュニティが貢献した検出器があります)。(3) コスト – 無料で使用できるため、Web3 の多くの小規模プロジェクト/スタートアップにとって重要です。(4) 統合 – オープンツールは通常、法的なハードルなしにローカルまたは CI で実行でき、プロジェクト固有のニーズに合わせてカスタマイズまたはスクリプト化できることが多いです。

オープンソースツールは急速に進化しています。例えば、Slither の新しい Solidity バージョンやパターンへのサポートは、Trail of Bits によって継続的に更新されています。ConsenSys が開発した Mythril は、イーサリアムだけでなく、バイトコード上で動作することで任意の EVM 互換チェーンを分析できます – これは、オープンツールがチェーンを越えて簡単に再利用できることを示しています。オープンツールの欠点は、しばしば*「自己責任で使用」*することであり、公式のサポートや保証がないことです。商用製品の UI のような洗練さやスケーラビリティがないかもしれません。しかし、ブロックチェーンでは、多くの企業でさえ、内部でコアツールとしてオープンソースを使用しています (時にはわずかなカスタム変更を加えて)。

• 商用サービスとツール: いくつかの企業がセキュリティ分析を製品として提供しています。例としては、MythX (ConsenSys Diligence によるクラウドベースのスキャン API)、Certora (オープンソース化する前にプローバーをサービスとして提供)、CertiK と SlowMist (監査で使用したりダッシュボード経由で提供したりする内部スキャナーと AI を持つ企業)、そして Securify from ChainSecurity (会社は買収され、そのツールは内部で使用された) や SolidityScan (監査レポートを出力するクラウドスキャナー) のような新しい参入企業があります。商用ツールは、よりユーザーフレンドリーな体験や統合されたサービスを提供することを目指していることが多いです。例えば、MythX は IDE 拡張機能や CI プラグインと統合されており、開発者はコントラクトを MythX に送信して、脆弱性スコアや問題修正の詳細を含む詳細なレポートを受け取ることができました。これらのサービスは通常、偽陽性を最小限に抑えるように調整された分析技術の組み合わせ (パターンマッチング、シンボリック実行など) を内部で実行します。

商用ツールの価値提案は、通常、利便性とサポートです。脆弱性の知識ベースを継続的に更新し、結果の解釈に関するカスタマーサポートを提供する場合があります。また、クラウドで重い計算を処理することもあります (そのため、ローカルでソルバーを実行する必要がありません)。しかし、コストが要因です – 多くのプロジェクトは、無料の代替手段が利用可能であるため、これらのサービスの料金を支払わないことを選択します。さらに、分散化の精神に基づき、一部の開発者はセキュリティのためにクローズドソースのサービスに依存することに躊躇します (「信頼するな、検証せよ」という精神)。2025 年の Certora Prover のオープンソース化は注目すべき出来事です。それは、ハイエンドの商用ツールだったものをコミュニティリソースに変えました。この動きは、有料ライセンスなしで誰でも自分のコントラクトを形式的に検証しようと試みることができ、コードのオープン性により研究者がツールを改善したり、他のチェーンに適応させたりできるため、採用を加速させると期待されています。

• 人間による監査サービス: ソフトウェアツールだけでなく、多くの監査は専門の会社 (Trail of Bits, OpenZeppelin, Certik, PeckShield など) によって行われていることにも言及する価値があります。これらの会社は、上記のツール (主にオープンソース) と独自のスクリプトを組み合わせて使用します。これらの取り組みの成果物は、しばしば非公開にされるか、監査レポートで要約されるだけです。商用監査会社でさえオープンソースツールに大きく依存しているため、ここには「オープン vs 商用」という二分法は正確にはありません。差別化は、専門知識と手作業の労力にあります。とはいえ、一部の会社は、自社に優位性を与えるために、独自の AI 支援監査プラットフォームを開発しています (例えば、*「ChainGPT」*が内部監査に使用されているという報告や、CertiK がオンチェーン監視のために Skynet という AI を開発しているという報告がありました)。これらは公開ツールではないため、その精度や方法は広く文書化されていません。

実際には、一般的なパターンはオープンソースが第一で、商用は任意です。チームは開発とテスト中にオープンツールを使用します (簡単に統合でき、必要なだけ実行できるため)。その後、デプロイ前に追加のチェックとして 1 つか 2 つの商用サービスを使用するかもしれません – 例えば、MythX スキャンを実行して「セカンドオピニオン」を得たり、Certora のような高度なツールを使用して重要なコンポーネントを形式的に検証する会社を雇ったりします。境界線が曖昧になるにつれて (Certora がオープンソースになり、MythX の結果がオープンツールと重複することが多い)、区別は能力よりもサポートと利便性に関するものになりつつあります。

注目すべきクロスオーバーは、Certora のマルチチェーンサポートです – Solana と Stellar を正式にサポートすることで、オープンな代替手段が少ないプラットフォームに対応しています (例えば、イーサリアムには多くのオープンツールがありますが、Solana には最近までほとんどありませんでした)。セキュリティツールが新しいエコシステムに拡大するにつれて、少なくともオープンソースが追いつくまでは、商用製品がギャップを埋めることが増えるかもしれません。

最後に、オープン vs 商用はここでは敵対的ではないことに注意する価値があります。それらはしばしば互いに学び合います。例えば、学術/商用ツールで開拓された技術 (Securify で使用された抽象解釈など) は、最終的にオープンツールに取り入れられ、逆に、オープンツールの使用から得られたデータは商用ツールの改善を導くことができます。両者が求める最終結果は、エコシステム全体のセキュリティ向上です。

クロスチェーンへの適用性​

イーサリアムはこれらのツールのほとんどの焦点となってきましたが (スマートコントラクト活動におけるその優位性を考えると)、形式的検証と AI 支援監査の概念は他のブロックチェーンプラットフォームにも適用可能です。以下にその適用方法を示します。

• EVM 互換チェーン: BSC, Polygon, Avalanche C-Chain など、イーサリアム仮想マシンを使用するブロックチェーンは、すべての同じツールを直接使用できます。ファズテストや静的分析は、コントラクトがイーサリアムメインネットにデプロイされるか Polygon にデプロイされるかを気にしません – バイトコードとソース言語 (Solidity/Vyper) は同じです。実際、Mythril と Slither は、アドレスからバイトコードを取得することで、任意の EVM チェーンのコントラクトを分析できます (Mythril は RPC エンドポイントさえあればよい)。これらのチェーン上の多くの DeFi プロジェクトは、イーサリアムプロジェクトと同様に Slither と Echidna を実行します。BSC や Avalanche 上のプロトコルの監査は、通常、イーサリアムの監査と同一のツールキットを使用します。したがって、EVM コンテキストでのクロスチェーンは、主にイーサリアムのツールチェーンを再利用することを意味します。

• Solana: Solana のスマートコントラクトは Rust で書かれ (通常は Anchor フレームワーク経由)、BPF 仮想マシン上で実行されます。これはイーサリアムとは非常に異なる環境であるため、イーサリアム固有のツールはそのままでは機能しません。しかし、同じ原則は適用されます。例えば、Rust のネイティブなファジングライブラリや cargo-fuzz のようなツールを使用して、Solana プログラムでファズテストを行うことができます。Solana での形式的検証は、最近までほとんど存在しませんでした。Certora と Solana のエンジニアの協力により、仕様に対して Rust/Anchor コントラクトを証明できるSolana プログラム用の社内検証ツールが生まれました。前述のように、Certora はプローバーを Solana の VM に拡張し、開発者は Solidity と同様に Solana プログラムの振る舞いに関するルールを記述してチェックできるようになりました。これは、Solana の迅速な開発アプローチが、多くのコントラクトがイーサリアムで見られるような厳格なテストなしでローンチされたことを意味するため、重要です。形式的ツールはそれを改善できます。Solana の AI 監査も考えられます – Rust を理解する LLM に、Solana プログラムの脆弱性 (所有権チェックの欠落や算術エラーなど) をチェックするようにプロンプトを入力することができます。Solana 固有のパターンに関するファインチューニングが必要かもしれませんが、Rust の人気を考えると、GPT-4 は Rust コードの読み取りにかなり習熟しています。近いうちに「ChatGPT for Anchor」スタイルのツールも登場するかもしれません。

• Polkadot および Substrate ベースのチェーン: Polkadot のスマートコントラクトは、ink! フレームワークを使用して Rust で書く (WebAssembly にコンパイルする) か、EVM パレット (Moonbeam が行うように) を実行して Solidity を使用することができます。ink!/Wasm の場合、検証ツールはまだ初期段階です。一般的な Wasm 検証フレームワーク (例えば、Microsoft の Project Verona などが Wasm の安全性を検討しています) を使用して、Wasm コントラクトのプロパティを形式的に検証しようと試みることができます。Certora のオープンソースプローバーは、Stellar の WASM スマートコントラクトのサポートも言及しており、これは Wasm ベースのチェーンの概念と似ています。したがって、Polkadot の Wasm コントラクトにも適用可能である可能性が高いです。ink! コントラクトのファズテストは、Rust テストを書くことで行うことができます (Rust のプロパティテストは同様の役割を果たせます)。ink! コントラクトの AI 監査は、Rust コードの分析を伴いますが、これも LLM が適切なコンテキストで実行できます (ただし、いくつかのヒントなしでは特定の ink! マクロやトレイトについては知らないかもしれません)。

さらに、Polkadot は並列スマートコントラクト開発のために Move 言語を模索しています (一部のコミュニティフォーラムで示唆されています)。Move が Polkadot のパラチェーンで使用されるようになれば、Move Prover が付属し、設計による形式的検証機能がもたらされます。Move の安全性への重点 (リソース指向プログラミング) と組み込みのプローバーは、形式的手法のクロスチェーン伝播を最初から示しています。

• その他のブロックチェーン: Tezos (Michelson スマートコントラクト) や Algorand (TEAL プログラム) のようなプラットフォームは、それぞれ形式的検証の取り組みを行ってきました。例えば、Tezos には Mi-Cho-Coq というツールがあり、Michelson の形式的セマンティクスを提供し、プロパティの証明を可能にします。これらはより学術的な側面が強いですが、明確に定義されたコントラクトセマンティクスを持つブロックチェーンであれば、形式的検証の対象となり得ることを示しています。AI 監査は、原則として、どのプログラミング言語にも適用できます – それは LLM を適切にトレーニングまたはプロンプト入力する問題です。あまり一般的でない言語の場合、LLM は十分な例で事前トレーニングされていない可能性があるため、効果的であるためにはいくつかのファインチューニングが必要かもしれません。

• クロスチェーンインタラクション: 新しい課題は、チェーン間の相互作用 (ブリッジやインターチェーンメッセージングなど) を検証することです。ここでの形式的検証は、複数のチェーンの状態と通信プロトコルをモデル化することを含むかもしれません。これは非常に複雑で、現在ほとんどのツールの範囲を超えていますが、特定のブリッジプロトコルはセキュリティのために手動で分析されています。AI はクロスチェーンコードのレビューに役立つかもしれません (例えば、Cosmos 上の IBC プロトコルと相互作用する Solidity コントラクトをレビューするなど) が、まだ既製のソリューションはありません。

本質的に、イーサリアムのツールが他のチェーンへの道を開きました。多くのオープンソースツールが適応されています。例えば、Solana (Rust) 用の Slither のような静的アナライザーを作成する取り組みがあり、不変条件テストの概念は言語に依存しません (プロパティベースのテストは多くの言語に存在します)。強力なエンジン (Certora の複数の VM 用など) のオープンソース化は、クロスチェーンセキュリティにとって特に有望です – 同じプラットフォームを使用して、Solidity コントラクト、Solana プログラム、Move コントラクトを検証できます。ただし、それぞれに適切な仕様が書かれている必要があります。これにより、業界全体でより均一なセキュリティ体制が促進されます。

また、AI 支援監査はすべてのチェーンに利益をもたらすことにも注目する価値があります。なぜなら、モデルはどのコンテキストの脆弱性についても教えることができるからです。AI に適切な情報 (言語仕様、そのエコシステムでの既知のバグパターン) が提供される限り、同様の推論を適用できます。例えば、ChatGPT には適切なプロンプトで Solidity コントラクトまたは Move モジュールを監査するように依頼でき、両方を行います – それがその概念を持っていれば、*「この Move モジュールはリソース保存に違反する可能性がある」*といったことさえ捉えるかもしれません。限界は、AI がそのチェーンの十分なトレーニングデータに触れていたかどうかです。最も人気のあるイーサリアムは、モデルを Solidity に最も得意になるように偏らせている可能性があります。他のチェーンが成長するにつれて、将来の LLM やファインチューニングされた派生モデルもそれらをカバーできるようになるでしょう。

結論​

スマートコントラクトの形式的検証と AI 支援監査は、急速に進化している分野です。現在、コードの信頼性を向上させる決定論的な静的アナライザーやファジングフレームワークから、人間のようにコードについて推論できる最先端の AI まで、豊富なツールキットがあります。かつてはニッチな学術的追求であった形式的検証は、より良いツールと統合を通じてより実用的になりつつあります。AI は、現在の限界にもかかわらず、セキュリティ分析の自動化において画期的な能力の片鱗を見せています。

まだ万能の解決策はありません – 現実世界の監査は、多層防御を達成するために複数の技術を組み合わせています。Foundry のファズテストと不変条件テストは、デプロイ前に期待される基準をすでに引き上げており (基本的なテストをすり抜ける多くのエラーを捉えています)、AI 支援監査は、慎重に使用すれば、監査人のための強力な補助となり、手動レビューだけでは不可能な規模と速度で問題を指摘し、コンプライアンスを検証できます。しかし、これらのツールを駆動し、その発見を解釈し、チェックすべき適切なプロパティを定義するためには、人間の専門知識が依然として不可欠です。

今後、これらのアプローチのさらなる収束が期待できます。例えば、AI が形式的仕様の記述や不変条件の提案を助けるかもしれません (「AI、この DeFi コントラクトにはどのようなセキュリティプロパティが成立すべきか？」)。ファジングツールは、入力をよりインテリジェントに生成するために AI を組み込むかもしれません (PromFuzz が行うように)。形式的検証エンジンは、どの補題やヒューリスティクスを適用するかを決定するために機械学習を使用するかもしれません。これらすべてが、イーサリアムだけでなく、すべてのブロックチェーンプラットフォームで、より安全なスマートコントラクトに貢献するでしょう。究極のビジョンは、重要なスマートコントラクトがその正確性に高い信頼性を持ってデプロイできる未来です – この目標は、どちらか一方だけではなく、形式的手法と AI 支援の相乗効果によって達成される可能性が高いです。

Sources:

• Foundry fuzzing and invariant testing overview
• Trail of Bits on fuzzing vs formal verification
• Trail of Bits on formal verification limitations
• Patrick Collins on fuzz/invariant vs formal methods
• Trail of Bits on invariants in audits
• Medium (BuildBear) on Slither and Mythril usage
• AuditGPT results (ERC compliance)
• Trail of Bits on LLM (Codex/GPT-4) limitations
• LLM-SmartAudit performance vs traditional tools
• “Detection Made Easy” study on ChatGPT accuracy
• PromFuzz (LLM+fuzz) performance
• Certora open-source announcement (multi-chain)
• Move Prover description (Aptos)
• Static analysis background (Smart contract security literature)

長年にわたり、ブロックチェーン業界では「大きいほど良い」という常識が支配してきました。Ethereum Global Network（EGN）は、Ethereum メインネットから無数のプロジェクトに至るまで数千のサービスを支える広大なピアツーピア（P2P）層であり、この考えに基づいて構築されました[cite: 4, 25]。理論はシンプルです。全員が同じ空間を共有する巨大で混合されたネットワークは、ノードの発見を促進し、エコシステムを攻撃に対してよりレジリエントにすると考えられました[cite: 34, 35]。

しかし、重要な研究論文「A Place for Everyone vs Everyone in its Place: Measuring and Attacking the Ethereum Global Network」は、この根本的な信念に異議を唱えます。研究は、この「誰でも入れる場所」アーキテクチャが、強さの源泉ではなく、深刻な非効率性と危険なセキュリティ脆弱性をもたらし、総市場価値が 5,000 億ドルを超えるサービスに影響を及ぼす可能性があることを明らかにしました[cite: 6, 24]。

非効率の悪夢：群衆に向かって叫ぶ​

EGN の約束は、ノードが同じサービスを提供するピアを簡単に見つけて接続できることでした[cite: 34]。実際は全く逆です。研究は、ノードが広大で騒がしい EGN の海の中で相手ノードを必死に探す様子を示しています[cite: 8]。

非効率性は驚異的です：

• 無駄な接続：ノードの接続試行の 75% 以上が、全く異なるサービスのピアに向けられています[cite: 8]。
• 極端な接続コスト：あるケースでは、ノードが有効な隣接ノードを 1 つ見つけるだけで 45,908 回 の接続試行が必要でした[cite: 9]。これは、Bitcoin の成功率が 4 分の 1 であるという推定と対照的です[cite: 54]。
• 後退：改善を意図した新しいディスカバリープロトコル Discv5 は、むしろ性能が低下しています。12 時間のテストでは、Discv5 を使用したノードは 3 つ以下の接続しか確立できませんでした。これは、サービスを広告するための重要な「トピックディスカバリーメカニズム」が主要クライアントすべてで未実装であるためです[cite: 57, 59]。

根本的な問題は、EGN の大多数のノードが、無関係なピアで埋め尽くされたルーティングテーブル（「アドレスブック」）を持っていることです。研究は、ほとんどの Discv4 ノードが DHT（分散ハッシュテーブル）内に同一サービスのピアを 5% 未満しか保持していないことを示しました[cite: 44]。

セキュリティの錯覚：脆弱な巨人​

「大きいほど安全」という議論の第二の柱は、EGN の規模が攻撃者の影響力を希釈するというものでした[cite: 35]。論文は、DHT 汚染攻撃という基礎的な攻撃をシミュレートすることで、この前提を覆します。悪意あるノードがネットワークのアドレスブックに自らのエントリを大量に流し込む手法です[cite: 61, 62]。

結果は、EGN の混合的性質が防御ではなく重大な脆弱性であることを示しています[cite: 10, 65]：

• 破壊的に効果的：ネットワークの 0.3% 未満に相当する 300 の悪意あるノードだけで、ほとんどのサービスの接続成功率を 1% 未満にまで低下させることができます[cite: 11, 63]。
• 大規模な孤立：わずか 24 時間で、この小規模攻撃はネットワークを分断し、数千の正直なノードをサービスから切り離すことに成功しました[cite: 11, 64]。
• 設計上の問題：この脆弱性はバグによるものではなく、混合アーキテクチャの必然的な結果です[cite: 65]。同様の攻撃を各サービスごとに分離された専用ネットワークでシミュレートしたところ、ルーティングテーブルがクリーンで関連ピアのみで構成されているため「ほぼ無効」でした[cite: 66]。

今後の道筋：「それぞれの場所にいる」こと​

研究は、混合アーキテクチャが特に小規模サービスにとって有害であり、非効率かつ不安全な環境で余波を受けると結論付けています[cite: 37]。解決策は、グローバルネットワークを放棄することではなく、より整理された形にシフトすることです。「誰でも入れる場所」から「誰もが自分の場所にいる」へと変えることが求められます[cite: 522]。

論文は二つの主要な解決策を提案しています：

1. サービス固有の DHT：すべてのノードが自らのサービス情報を Ethereum Node Record（ENR）に直接含めることを義務付けます[cite: 490, 491]。このシンプルな変更により、ノードは同一サービスのピアをフィルタリング・優先でき、発見効率とセキュリティが劇的に向上し、分散性を犠牲にしません[cite: 495]。
2. より信頼性の高いブートノード：シミュレーションは、ブートノードがネットワーク分断に対する最後の防衛線として重要な役割を果たすことを示しました[cite: 496]。論文は、各サービスがブートノードの数を増やし、同一サービスのピアを優先的に保存するよう設定することを推奨しています。これにより、ネットワーク回復のためのレジリエントなバックボーンが構築されます[cite: 499]。

開発者とエコシステム全体の健全性にとって、これらの発見は重要な警鐘です。堅牢で効率的な P2P 層は、あらゆる分散サービスの基盤です。提案された修正を実装することで、コミュニティはより整理され、安全で、真にグローバルなネットワークへと前進できるでしょう。