メインコンテンツまでスキップ

スマートコントラクトの形式的検証と AI 支援監査

· 約58分
Dora Noda
Dora Noda
Software Engineer

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

形式的検証とは、数学的および論理ベースの技術を用いて、スマートコントラクトの正確性とセキュリティを証明することを指します。実際には、これにはプロパティベースのファズテストやシンボリック実行から、厳密な定理証明やモデル検査まで、さまざまな方法論が含まれます。その目的は、コントラクトが仕様を満たし、考えられるすべての入力と状態において悪用可能なバグを含まないことを保証することです。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)
Share on Twitter