初めて本気で監査したとき、私はリポジトリ内で最も大きいコントラクトを開いて1行目から読み始めた。2時間後には頭痛がして、発見ゼロだった。コードがどのように動作するかは暗記していたが、それが何を保証すべきかを一度も問いかけていなかった。これは逆だということに気づくまで時間がかかった。

今はSolidityを最初に読まない。スコープを読み、単一の関数本体を見る前に、何が常に真でなければならないかを書き出す。バグとはこれらの真理の違反である。真理を知らなければ、ただコードを眺めているだけだ。

ステップ1：読む前に不変条件を書き出す

不変条件とは、誰が何をどのような順序で呼び出しても、プロトコルが常に成立すると主張する性質である。コンテストでは、深刻度が高いのは資金と制御権に関する部分なので、そこから始める。

ほとんどの場合、次の2つの質問で十分だ：

  • 誰がどのような条件で資金を移動できるか？
  • 会計について常に成立しなければならないことは何か？

レンディングプール型のプロトコルの場合、最初に挙げる不変条件は次のようになる。実装方法を考える前に、平易な言葉で書く。

  • 全ユーザーの預金合計から全借入合計を引いた値が、プールの利用可能流動性＋未回収債務と等しい。会計は必ず一致しなければならない。
  • ユーザーは自分の残高までしか引き出せず、それ以上引き出したり、他人の残高を引き出したりしてはならない。
  • ポジションは、実際に健全性しきい値を下回った場合にのみ清算可能でなければならない。
  • 利息は単調に増加し、返済額を減らせるような逆戻りは起こらない。
  • 債務を減らせるのは、借り手本人か、不健全なポジションに対する清算人だけである。
  • 金利パラメータやオラクルを変更できるのは、ガバナンスだけである。

ここには関数名が一切出てこない点に注目してほしい。これらは約束である。残りのコンテスト期間中の仕事は単純だ。これらのいずれかを破る呼び出し順序を見つけることである。

ステップ2：外部エントリポイントをマッピングする

資金はテレポートしない。状態を変更するには外部から何かを呼び出す必要がある。そこで、外部から到達可能な関数をすべてリストアップする。攻撃対象領域はまさにその集合であり、それ以外ではない。

これは慎重に読む前にgrepで素早く行う：

# every external / public function in scope
grep -rnE "function .*\b(external|public)\b" src/ \
  | grep -v "view\|pure"

Enter fullscreen mode Exit fullscreen mode

viewとpureは状態を変更できないため除外する。残ったものが攻撃者が操作できるレバーの一覧である。レンディングプールの場合、通常はdeposit、withdraw、borrow、repay、liquidate、そして存在する管理者用セッターである。

次に、それぞれの関数に、それが脅かし得る不変条件を注釈する。depositとwithdrawは会計整合性を脅かし、withdrawは「自分の残高のみ」というルールを脅かす。liquidateは「不健全な場合のみ」というルールを脅かし、セッターは「ガバナンスのみ」というルールを脅かす。ここでグリッドが完成する。一方にエントリポイント、もう一方に不変条件を置き、交差するセルが探索対象となる。

ステップ3：信頼境界を描く

実際のファインディングの多くは、プロトコルが本来完全に信頼すべきでないものを信頼している境界に存在する。ロジックを読む前に、すべての境界をマークする。

  • オラクル。価格はどこから来るのか？単一トランザクションで操作可能か（AMMからのスポット価格は典型的な落とし穴）？古いデータ、ゼロ、またはリバートを返した場合どうなるか？
  • 管理者とロール。特権ロールは何ができ、その特権パスはプロキシやdelegatecallを通じて意図しない形で到達可能か。「管理者がrugできる」はスコープ外であることが多いが、「非管理者が管理者専用効果に到達できる」はHighである。
  • クロスコントラクト呼び出し。すべての外部呼び出しは、制御がコントラクトから離れて戻ってくる場所（再入）や、呼び出し先が敵対的に振る舞える場所（奇妙なtransferを持つ悪意あるトークン、手数料徴収トークン、リベーストークン）である。
  • トークンの前提条件。コードは18桁小数を前提としているか？transferがboolを返すことを前提としているか？transfer時に手数料が発生しないことを前提としているか？各前提は、敵対的トークンが越える境界である。

レンディングプールの場合、まずオラクル境界を調べる。なぜなら「価格を操作し、担保を過大評価して借り入れ、逃げる」というパターンは多くのHighの典型だからだ。

ステップ4：ここでコードを読み、違反を探す

ここで初めて関数本体を開く。そして「これは何をするのか」とは読まない。「これはどの不変条件に触れ、ここでそれを破れるか」と読む。

以下は短い例である。擬似コードで、レンディングプール型、意図的にバグを含む：

// invariant at risk: a user can only withdraw up to their own balance
function withdraw(uint256 amount) external {
    uint256 shares = amountToShares(amount);
    // BUG: no check that balanceOf[msg.sender] >= shares
    balanceOf[msg.sender] -= shares;   // underflows? or does it?
    totalShares -= shares;
    token.transfer(msg.sender, amount);
}

Enter fullscreen mode Exit fullscreen mode

不変条件優先で読むと、「これはトークンを転送するか」とは問わない。「これはあなたが自分の残高までしか引き出せないことを強制しているか」と問う。答えは「No」で、減算前に境界チェックがない。古いSolidityではアンダーフローして巨大な残高になる。0.8以降ではリバートするので安全かもしれない……ただしamountToSharesの丸め方で、amountがゼロでないのにsharesがゼロになる場合、トークンを引き出しつつ何も減算しないという抜け穴が生じる。それが亀裂だ。仮説はテストで失敗するまでファインディングではないので、FoundryのPoCで検証する。

オラクル境界と比較してみよう：

// invariant at risk: only genuinely unhealthy positions can be liquidated
function liquidate(address user) external {
    uint256 price = ammPair.getSpotPrice();   // single-block manipulable
    uint256 collateralValue = collateral[user] * price;
    require(collateralValue < debt[user], "healthy");
    // seize collateral, repay debt
}

Enter fullscreen mode Exit fullscreen mode

不変条件は、ポジションが実際に不健全な場合にのみ清算が発生すると述べている。しかし価格はスポットAMM読み出しから来ており、資金力のある攻撃者はフラッシュローンで単一トランザクション内に価格を操作できる。つまり健全なポジションを不健全に見せかけ、清算して利益を得られる。バグは算術ではなく、操作可能な情報源を信頼している点にある。不変条件優先の思考は、ステップ3でオラクルを境界としてすでにフラグを立てていたため、この関数を読む前にそれを発見できる。

この順序が重要な理由

コードを先に読むと、その動作方法に固定され、信じてしまう。著者のメンタルモデルが自分のものに染み込む。コードが意図した通りに動作しているかを確認することになり、それは監査の逆である。監査とは、コードが絶対にやってはならないことをさせられるかどうかを確認することだ。

不変条件優先はフレームを逆転させる。実装とは独立に、プロトコルが約束したことを決める。そしてすべての関数は、その約束に対する容疑者として測定される。spectr-aiを構築したときも、まさにこの構造を推論方法に組み込もうとした。脆弱性について自由連想するのではなく、まず性質を述べ、それに対してコードをチェックする。

また高速でもある。今週選んだコンテストでは、不変条件リストの作成に40分程度しかかからず、2,000行のコードベースを「ここに破る価値のある6つの事柄があり、それらが破られる可能性が高い3つの境界がある」という短いリストに変換できた。それが地図だ。1行目から2,000行目まで読むのはただの迷子になる。

見慣れないコードベースに向き合うとき、あなたは読む前に「常に真でなければならないこと」を書き出すだろうか、それともコードに飛び込んでその場でルールを再構築するだろうか？