スマートコントラクトのセキュリティ監査

article technology medium #smart-contract#security-audit#reentrancy#formal-verification#immunefi#bug-bounty#slither#mythril#oracle-manipulation#access-control#integer-overflow
Created: 2026-06-07 Updated:

スマートコントラクトのセキュリティ監査手法・形式検証・脆弱性パターン（reentrancy・オラクル操作・アクセス制御・整数オーバーフロー）・バグバウンティ（Immunefi）・主要ハッキング事例を体系化する。

スマートコントラクトのセキュリティ監査

スマートコントラクトは「デプロイ後の変更が原則不可能」「オープンソースであり攻撃者がコードを解析可能」「資産を直接管理する」という性質から、セキュリティリスクが極めて高い。DeFi ハッキング被害は 2020〜2024 年累計で数百億ドル規模に達し、単一のバグが数千億円規模の損失を生む事例もある。本記事は主要な脆弱性パターン・監査手法・形式検証・バグバウンティの体系的な整理を行う。情報カットオフ ~2025-08、confidence: medium 固定（2026-06 時点での外部再検証は未実施）。

主要な脆弱性パターン

Reentrancy（再入攻撃）

Reentrancy は EVM スマートコントラクトの歴史上最も有名な脆弱性クラスである。攻撃の流れは以下の通りだ。

  1. 被害コントラクトが ETH を外部アドレスに送る（call{value: ...}()）
  2. 受信側コントラクトの fallback/receive 関数が呼ばれる
  3. fallback 関数が被害コントラクトの引き出し関数を再び呼び出す
  4. 被害コントラクトの残高更新がまだ行われていないため、二重引き出しが成立

防止策:

  • Checks-Effects-Interactions パターン: 外部呼び出し前に残高を更新し、呼び出し後に何もしない
  • ReentrancyGuard（OpenZeppelin）: nonReentrant 修飾子でロックする
  • Pull Payment パターン: ETH を「push」せず、ユーザーが「pull」する設計

事例: The DAO（2016 年、360 万 ETH 流出、約 5,000 万ドル。Ethereum のハードフォーク[ETH/ETC 分裂]のきっかけとなった）

オラクル操作（Oracle Manipulation）

フラッシュローンで DEX の価格を一時的に歪め、その歪んだスポット価格を参照するプロトコルを攻撃するパターン（tech-223 参照）。

事例: Mango Markets（2022 年、MNGO トークン価格操作で約 1 億ドル流出）

防止策: TWAP（時間加重平均価格）の使用・複数オラクルの集約・価格急変時のサーキットブレーカー

アクセス制御の欠陥

アクセス制御ミスは「誰でも管理関数を呼べる」「権限チェックが不完全」などの設計ミスから生じる。

典型的なバグ例:

  • initialize() 関数に onlyOwner 修飾子がなく、攻撃者が再初期化できる
  • setOwner() の呼び出し権限が適切に制限されていない
  • マルチシグの署名者を配列から削除せずに「無効化」したつもりになる

防止策: OpenZeppelin AccessControl / Ownable の正しい使用・初期化関数の一度限り実行保証（initializer 修飾子）

事例: Ronin Network（2022 年、9 つのバリデータのうち 5 つの秘密鍵を取得・約 6 億ドル流出）

整数オーバーフロー・アンダーフロー

Solidity v0.8.0 以前では uint256 の加算がオーバーフロー（最大値を超えてゼロに戻る）してもエラーにならなかった。

防止策: Solidity v0.8.0 以降ではデフォルトでチェック済み（checked 演算）。旧コードは SafeMath ライブラリを使用。

フラッシュローン攻撃

フラッシュローンは同一トランザクション内で借入・操作・返済が完結する無担保貸借であり、それ自体は正規の機能だが、他の脆弱性と組み合わせて攻撃の原資として使われる。単独でバグではなく、オラクル操作・価格操作・ガバナンス攻撃の「増幅装置」として機能する。

その他のパターン

  • Front-running / MEV: 未確認トランザクションを監視してより高い gas price で先に処理を差し込む
  • Unchecked Return Values: transfer() の失敗を無視して処理が続く
  • Delegatecall の誤用: 呼び出し先コントラクトが呼び出し元のストレージを変更するリスク

監査手法

自動化ツールによる静的解析

Slither（Trail of Bits）: Python 製の静的解析フレームワークで、80 以上の組み込みディテクタが既知の脆弱性パターンを検出する。CI/CD に組み込んで使うことが多い。

Mythril（ConsenSys）: シンボリック実行エンジンを使って EVM バイトコードレベルで脆弱性を探索する。複雑な実行パスのバグ発見に強い。

4naly3er・aderyn: 近年 Foundry エコシステムと統合が進む軽量な静的解析ツール。

ファジングテスト

Foundry の組み込みファジング（forge test --fuzz-runs N）やエコファジング（Echidna、Trail of Bits）を使い、プロパティ違反（例: 「残高の合計は常に一定以上」）を自動探索する。手動では思いつかない境界値のバグを発見しやすい。

人手による監査

外部監査会社（Trail of Bits・OpenZeppelin Audits・Spearbit・Code4rena コンテスト等）によるコードレビューがデプロイ前の標準的なプロセスとなっている。特に DeFi の大型プロトコルは複数の監査会社に依頼するマルチ監査が推奨される。

Code4rena・Sherlock: セキュリティ研究者コミュニティが参加するコンテスト形式の監査プラットフォーム。多数の眼でコードを検査するため、単一監査会社より見落としが少ない。

形式検証（Formal Verification）

形式検証は数学的手法でコードの正しさを証明する最も厳格な手法だ。

Certora Prover: Solidity コントラクトの「仕様（プロパティ）」を Certora Verification Language（CVL）で記述し、全実行パスで仕様を満たすことを自動証明する。Aave・Compound などの大型プロトコルが採用している。

Move Prover: Move 言語の形式検証ツール。Move の型システムとの統合が深く、リソース型の安全性証明が自動化される。

Halmos（a16z crypto）: Foundry の Solidity テストをシンボリック実行ベースで形式検証する OSS ツール。既存の Foundry テストを活用できる利点がある。

バグバウンティ — Immunefi

Immunefi は DeFi 特化のバグバウンティプラットフォームで、プロトコルが報奨金を設定し、セキュリティ研究者が脆弱性を報告する仕組みを提供する。

報酬規模: クリティカルバグ（資金の不正引き出しを可能にするもの）には数十万〜数百万ドルの報奨金が設定されるケースがある。Immunefi を通じた支払い累計は 2025 年時点で数億ドル規模に達している。

分類: Critical / High / Medium / Low のバグクラスに分け、クリティカルは TVL の一定割合（例: 最大 10%）の報酬が設定されるプロトコルも多い。

主要ハッキング事例（参考）

スマートコントラクトセキュリティの理解のために代表的な事例を参照する。

年プロトコル被害額（概算）攻撃ベクタ
2016The DAO~5,000 万ドルReentrancy
2020bZx~100 万ドル（2 件）フラッシュローン + オラクル操作
2021Poly Network~6 億ドルアクセス制御ミス（クロスチェーン）
2022Ronin Network~6 億ドルバリデータ秘密鍵漏洩
2022Wormhole~3.2 億ドル署名検証バイパス
2022Mango Markets~1 億ドルオラクル価格操作
2023Curve Finance~7,000 万ドルVyper コンパイラバグ（Reentrancy）

各事例の共通した教訓は「監査・ファジング・形式検証の多層防御」「バグバウンティによる継続的な発見奨励」「アップグレード可能コントラクトと緊急停止機構の整備」の重要性である。

Solidity・Move の言語レベルの安全性は tech-221、開発フレームワークの静的解析統合は tech-222 を参照のこと。

Backlinks

Local graph