目次
おはようございます。
web3リサーチャーのmitsuiです。
土日のお昼はAIによるレポートを更新します。
普段は最新のトレンドや注目プロジェクトを紹介していますが、ここでは過去からの歴史を振り返る系の記事を投稿していきます。レビューはしていますが、一部内容に間違いがあるかもしれませんので、ご了承ください。
それではどうぞ！
1. はじめに
前編で解説したように、web3 では「自己責任」「自己管理」が原則のため、一度脆弱性が突かれたり秘密鍵を奪われたりすると、資金やトークンが瞬く間に消失してしまいます。
個人ユーザーの場合、基本的なウォレット管理やフィッシング対策を行うだけでも一定の被害を回避できますが、大規模なプロジェクトやプロトコルとなると「数十億〜数千億円規模の資金を取り扱う」ことも珍しくありません。
そこまで膨大な資金を扱う以上、ソフトウェア的な監査やハードウェアレベルのセキュリティ、組織のガバナンス体制、コミュニティとの連携など、多角的かつ高度なセキュリティ対策が必須です。本稿（後編）では、以下のポイントに注目して解説します。
- スマートコントラクト監査とフォーマルベリフィケーション
- DeFi プロトコルにおける安全設計（マルチシグ、Time Lock、オラクルなど）
- クロスチェーンブリッジ設計の進化と新たなアプローチ
- web3 セキュリティサービス・保険・バグバウンティ
- ZK（Zero-Knowledge）技術、DID、規制強化といった今後の展望
それでは順を追って見ていきましょう。
2. スマートコントラクト監査とフォーマルベリフィケーション
2-1. なぜ監査が重要なのか
web3 の中核となるスマートコントラクトは、プロジェクトのルールや資金フローをソフトウェア的に担保する存在です。バグがひとつあれば、資金が無限に増刷されたり、所有権が書き換えられたり、ブリッジからごっそり持ち出されたりするリスクがあり、実際に数百万〜数億ドル単位の被害も起きています。
つまり、「ソフトウェア＝マネー」 という世界であり、コードが完璧に近い安全性を求められるのです。従来の Web2 スタートアップのように「βテストをしながら改善」では済まず、最低限でもローンチ前の厳格な監査が求められています。
2-2. 監査の一般的な流れ
スマートコントラクトの監査は、下記のようなプロセスをたどるのが一般的です。
- 要件ヒアリング・コード提供
- 開発チームと監査チームがプロトコルの設計仕様やトークンエコノミクス、ロジックなどを擦り合わせる。
- スマートコントラクトのコードリポジトリ（GitHub など）を提出し、機能仕様書・テストケースも共有。
- 静的解析 & 手動コードレビュー
- 静的解析ツール（MythX, Slither, Echidna など）を使って典型的な脆弱性（再入攻撃、整数オーバーフロー、アクセスポリシー不備など）を検出。
- その後、監査エンジニアが手動でコードロジックとライブラリの使用方法をチェックし、緊急度別に脆弱性を分類。
- 動的検証・フォーマルテスト
- コンポーネントテストやフォーマルベリフィケーションツール（Certora、VerX など）を活用し、特定の不変条件（Invariant）が破られないか検証。
- Mock 環境やテストネットを活用し、ホワイトハット手法でコントラクトにアタックシナリオを試す。
- レポート作成・修正対応
- 監査結果をレポートにまとめ、発見された脆弱性を「Critical, High, Medium, Low」などのランクで報告。
- 開発チームが該当箇所を修正 → 監査チームが再テスト → 最終レポートが公開される。
- バグバウンティプログラム（継続監査）
- ローンチ後も、ホワイトハットハッカーやコミュニティに脆弱性発見のインセンティブを提供し、プロトコルを継続的に検証。
- バグ報告に応じて報酬を支払う仕組みは、Uniswap, Aave, MakerDAO など大手 DeFi で広く導入されている。
2-3. 代表的な監査機関
- CertiK: 静的解析やフォーマルベリフィケーションツールに強み。大手プロジェクトの監査を多数手掛け、ダッシュボード形式のレポートがわかりやすい。
- OpenZeppelin: スマートコントラクトのライブラリも提供しており、コードベースの設計指針がコミュニティに浸透。ERC スタンダードの提案でも実績あり。
- Trail of Bits: 高度なセキュリティ研究で知られ、ブロックチェーン分野だけでなく幅広いソフトウェアの監査・脆弱性発見を行う。
- PeckShield: 主に中国系の大手監査企業であり、DeFi や GameFi の大規模監査で存在感。攻撃検知・追跡ツールなども開発している。
2-4. フォーマルベリフィケーションの可能性
DEBUNK編集長
