T30 · Audit
監査は何を調べるのか？
- 練習する能力
- Builder
- 実践
- 自分のプロトコルの不変条件を 5 つ書き、ファジングで自動検証する。
- AI Lab
- AI にコードから不変条件を推測させ、本当の安全性の性質と単なる実装詳細を自分で見分ける。
現実の問題
公開を控えたteamが、少なくない費用で監査を依頼しました。
三週間後の報告には17件、重大2件、中程度5件、軽微と情報10件がありました。全17件を修正し、再確認も通過しました。最終pageは全件解決と記し、teamはPDFを公式siteへ置き、監査済みと発表して公開しました。
三か月後、protocolが空になりました。
振り返りで最も痛かったのは金額より、攻撃経路が報告に一言もなかったことです。 一行の見落としではなく、コードの脆弱性を全く使いませんでした。外部市場で担保価格を上げ、真の価値以上の資産を借り、全callは合法でした。
監査側の回答も正当でした。範囲は実装の正しさであり、極端な市場での経済的仮定は含まないと、第二pageに明記していました。teamは読んでいませんでした。
費用で何を買ったのか？ 全17件を直しても資金を失うなら、監査の価値はどこにあるのでしょうか？
思考実験
投資者として、二protocolの監査報告を比べます。
Aの報告：58page、23件で、分類、コード位置、再現手順、修正案、解決済み表示が揃い、専門的です。
Bの報告：19page、6件で重大問題はありませんが、Aにないものが前半に二つあります。
第一は脅威モデルです。一般利用者、大口、無限資金を借りられる裁定者、ガバナンスtoken保有者、依存先protocolなどの攻撃者と能力、明確に防がない状況を記します。例えば、一blockの価格操作は5%以内と仮定し、超えると不良債権が出ると認めています。
第二は不変条件一覧です。何が起きても成立する11断言に、それぞれ自動テストがあります。例えば、全預金合計は実際の保有資産以下です。
どちらなら、より安心して投資できますか？
発見が多く詳細に見えるAを最初に選びがちですが、もう一段考えます。
- Aの23件は、過去の誤りを修正したという過去の説明です。
- Bの脅威モデルは、危険だと考える対象と、防がない範囲という境界です。
- Bの11不変条件は、今後一行変えるたび自動確認する未来の説明です。
Aは交付時から古くなり、公開後の変更は対象外です。Bの11条件はrepositoryと共に生き続けます。
あなたが決める
公開まで二か月、予算でもう一つだけできるなら、何を選びますか？
結果を観察する
本来は組み合わせる四手段を、カバーする時間で比べます。
| 手段 | 時間 | 発見対象 | 交付後の失効 |
|---|---|---|---|
| 監査 | 公開前のsnapshot | 人が考え、範囲に入る問題 | 次のコード変更は対象外 |
| 不変条件とFuzzing | 今から継続 | 宣言した性質を破る状態 | repositoryと共に生きる |
| monitoring | 公開後の毎瞬間 | 発生済みの異常 | 継続するが実際に見る人が必要 |
| bug bounty | 公開後に継続 | 他人が考えた、自分の未知の問題 | 報酬と攻撃利益の比率による |
最も重要な結論です。
監査は一snapshotですが、protocolは何年も生きます。
交付時が最高価値で、コード、依存、市場が変わるたび報告は変わらず価値が減ります。
では、本当に価値が減らない部分は何か？
Bの価値を守るのは六発見でなく、脅威モデルと不変条件です。前者が危険を定義し、後者が自動実行するコードにします。副産物ですが、発見一覧より長く残ります。
監査は何を調べるのかへの答えです。
真の成果はPDFだけでなく、脅威モデルと不変条件です。
発見だけなら一度のbug修正を、両方を作る監査なら継続する安全能力を買います。価格は同じかもしれません。
モデルを作る
脅威モデルの四問、不変条件の三種類、四層のtoolの能力境界を持ち帰ります。
一、脅威モデル：必須の四問
文章ではなく四つの答えです。書けなければ、防ぐものを理解していません。
| 問い | 書くもの | 書けない場合 |
|---|---|---|
| 誰が攻撃するか？ | 一般利用者、大口、無限借入の裁定者、ガバナンス保有者、外部protocol、自分のmultisig保有者 | 特に最後二種類を丸ごと見逃す |
| 何を取るか？ | 預金、金庫、LP流動性、ガバナンス権、または停止 | 資金だけ守り、可用性を忘れる |
| 何ができるか？ | 呼べる関数、資金、取引順序支配、待機block数 | T29の無限借入能力を過小評価する |
| 明確に防がないものは？ | 捨てる仮定を、ないふりせず記す | 最も重要なので次で扱う |
第四問が専門的な判断を分けます。
鍵漏えい、oracle全体の故障、一blockの一定幅以上の価格操作、底層資産の規制凍結など、各protocolに防がないものがあります。全てを防ぐと何もできないため、放棄自体は合理的です。
不合理なのは記さないことです。team内の境界理解がずれ、統合先は防ぐと誤解し、事故時に設計なのか脆弱性なのか分からなくなります。
一条件を一文で記します。
仮定：価格sourceの一blockの偏差はX%以下。
超過時：不良債権を保険基金が負担し、残りはLPで比例分担。
防がないもの：長期の価格source全体の操作。heartbeat確認と偏差circuit breakerで緩和。第三問がT29の費用表の入力です。 各役割の能力を、資金と時間の値に対応させます。
二、不変条件：三種類の書き方
常に成立する断言の良い特徴は、手順でなく状態で表し、一行で確認でき、違反は必ず問題を意味することです。
有用なものの大半は三種類です。
第一：会計の不変条件。 資金の保存で、書きやすく価値も高いです。
全利用者の残高合計 <= 実際の保有資産
総供給量 == 全保有者の残高合計
融資総額 + pool残高 == 入金総額 + 累積利息
share単価は単調非減少（清算や不良債権を除く）第一は等号でなく以下です。手数料と丸め残余を残すためです。丸めは常にprotocolに有利な方向です。T28の規則を自動断言へ変えました。
第二：権限の不変条件。 誰が何をできるかです。
管理者だけがparameterを変えられる
parameterは宣言した範囲内
pause中は残高を変える全関数が失敗する
清算人以外が他人の担保を移す経路はない第三：状態機械の不変条件。 正当な状態遷移です。
positionは健全か清算可能で、第三状態はない
閉じたpositionは操作不可
各orderは一回だけ約定
健全度が閾値以下なら、追加借入不可よくある誤りは、実装詳細を条件にすることです。内部array長が人数と同じという事実は、実装を変えると消えても安全性は変わりません。
破られると、誰かが損失か支配権喪失を受けるか？受けなければ安全不変条件ではありません。
三、四層のtoolの発見能力
発見と自分の労力で比べます。
| 層 | 発見できるもの | できないもの | 必要な労力 |
|---|---|---|---|
| compilerと型system | 構文、型、明白な未初期化 | ロジック全般 | ほぼなし |
| 静的解析 | 再入、戻り値未確認、危険な低水準callの既知pattern | 固有のロジック | 導入と誤検知の除去 |
| Fuzzing | 宣言した不変条件を破る状態 | 書かなかった性質 | 不変条件の記述 |
| 形式検証 | 所定modelで性質が必ず成立するか | model自体の誤り | 高く、通常は核心関数だけ |
Fuzzingの費用対効果が高いです。労力の大半は不変条件を書くことにあり、成果自体が文書、回帰テスト、統合先への安全声明になります。
静的解析は判決でなくfilterです。誤検知が多いので、各項を論争せず素早く除きます。
形式検証は最初から使わず、重要で短く、性質が厳密に書ける関数へ使います。例えば、資産とshareの変換がどの入力でも先の預金者を不利にしないことです。
四、発見は重大度以外の三種類に分ける
報告は重大度で分けますが、AIやtoolの大量の発見には別の分類が有用です。
- 真の問題
- 誤検知
- 見逃し
- 真の問題：実在し、修正します。
- 誤検知：toolが疑うが実在せず、素早く判定し論争しません。
- 見逃し：実在するが誰も見つけません。直接数えられず、脅威モデルで攻撃者一種類を丸ごと忘れていないかから推測します。
冒頭は典型的な見逃しです。17件は全て真、誤検知ゼロでも、無限借入の裁定者が範囲外でした。
何と呼ぶか
攻撃者、目標、能力、明確に防がないものを記す文書です。
監査の入力です。これがない監査は、防ぐ相手を知らずに鍵を確認することです。
何が起きても成立し、状態で表して自動検証できる断言です。
破られたら損失や支配権喪失があるかが、安全不変条件の基準です。
実行せずsourceやbytecodeを既知patternでscanし、再入、戻り値未確認、低水準callなど固定した形を発見します。
誤検知が多いので、判決でなくfilterに使います。
大量のランダム入力とcall列で、不変条件を破る状態を探します。
連続callで状態を保つstateful方式が強く、真の脆弱性は単一callよりcall列にあります。
所定modelで性質が必ず成立すると、数学で証明します。
テストより強い結論でも、modelが誤れば証明も誤ります。狭い範囲の重要関数へ使います。
公開後のオンチェーン状態を観察し、異常を人へ通知します。
攻撃阻止より発生から発見への時間を減らします。pause可能なら、その時間がほぼ損失額です。
脆弱性を責任ある方法で報告した人へ報酬を約束します。
上限が攻撃利益と比較でき、迅速な修正能力があることが前提です。
実践
T22またはT19の自作protocolを使います。なければT7の入出金契約でも構いません。
四問を先に書きます。 不変条件は脅威モデルから生まれるため、省きません。
各問を三～五行で書き、第四の防がないものは少なくとも二項目です。
三種類から五条件を選びます。 会計二、権限二、状態機械一を推奨します。
断言と違反の結果を書き、結果を書けなければ、実装詳細の可能性が高いので書き直します。
五つをassert関数にします。 各一関数で、状態は変えず確認だけします。
会計は手数料や丸め残余によって、以下か等号かを注意します。逆ならFuzzingが直ちに失敗して教えます。それは良いことです。
stateful Fuzzingを接続します。 連続で複数関数を呼び、状態を保つことが重要です。毎回初期化するとcall列の脆弱性を見つけません。
短く実行し、call数を出して実際の関数呼び出しを確認してから、長く実行します。
意図して一条件を破り、検知を確認します。 省けません。
丸め方向を逆にするか権限確認を外し、再実行します。まだ全て緑なら、条件は機能していません。assertに到達せず、またはFuzzingが経路を通っていないかもしれません。
戻す前に失敗call列を保存し、そのまま回帰テストにします。
三数値を記録します。実行round数、対象関数、最短失敗列の段数です。
失敗列が短いほど、実際の攻撃者が遭遇しやすい問題です。 最後の数が最も情報を持ちます。
repositoryと共に残る安全資産で、卒業制作 の第五段階の成果物です。
AI Lab
コードを渡し、二段階で行います。
最初に推定させます。
この契約の暗黙の不変条件、何が起きても成立すべき性質を推定してください。
各項を四fieldで：
- 状態で表す断言（手順で表さない）
- 依存するコードの場所（関数と行）
- 違反の結果
- 安全性か、現在の実装だけの事実かという判定
不明は不明と記し、推測しないでください。次に、自分の出力を批判させます。
一覧に戻り、安全性でなく実装詳細の項目を指摘し、理由を説明してください。第二段階の方が価値があることが多いです。 array長と人数の一致、mapping keyが非ゼロなど、現在の事実を条件にしがちです。成立しても資金を守りません。
自分で各項を確認し、本当の安全性の比率を数えます。今後どこまで補助できるかの目安として記録します。
最後の検証が最重要です。無限借入の裁定者が脅威モデルにいるのに、極端な一取引状態の条件がないなら見逃しです。モデルはコードを見ても、あなたの脅威モデルは見えません。
AI の回答後、自分で必ず検証すること
- 安全不変条件の全項目で、違反すると誰が損失や支配権喪失を受けるか言える
- 実装詳細は実装変更で成立しなくなり、安全性は変わらないと確認する
- 関数名と変数名は実際のコードにあり、捏造でない
- 会計の等号と以下が、手数料と丸め残余の実態に合う
- 現在そうであるだけの事実を、常に必要な性質としていないか
- 自分の脅威モデルの攻撃者一種類を、全く覆わない一覧になっていないか
実例
監査発見を全修正して公開しても、価格操作で大きな損失を受けました。コードの脆弱性はなく、全callは合法でした。
論点は経済的仮定を範囲に含めたかです。多くは報告前半に答えがあり、teamが読んでいませんでした。
監査範囲が能力境界で、依頼側と一緒に決めます。 脅威モデルを渡さなければ、実装だけが既定の範囲になります。
金庫の単体テストと高coverageでも、stateful Fuzzingは七段階でshare単価の単調非減少を破る列を見つけました。
各関数は正しくても、特定順序の丸め累積で先の預金者が不利になりました。
同じ人がコードとテストを書くので、思いつかない順序はテストにも入れません。 そのため単体テストでは見つかりにくい問題です。
異常時のalertは動きましたが、noiseの多いchannelへ送られ、深夜に担当がいませんでした。
pauseが使えるのに、発見まで数時間過ぎました。
有効性は導入したかでなく、誰がいつ見るかです。 重大度分類と、重大alertの担当者・応答期限が必要です。
固定上限に対し、対象資金がはるかに大きいprotocolがあります。
発見者の単純な計算を、報告を選ぶ答えにするため、回避損失の割合を上限にする方式が増えています。
T29と同じ表の報告利益を調整して、攻撃利益より高くしています。
変数を一つ変える
実装の正しさという既定値ではなく、範囲を自ら定義します。
宣言した能力を確認し、防がないものへ疑問を出します。仮定への疑問が報告で最も価値ある部分の場合があります。
本来書くべき文書だけなので、追加費用はほぼゼロです。
テストからruntime強制へ変わり、違反取引をrevertしてオンチェーンで止めます。
毎取引の全体確認のGasが代償です。最重要の一、二会計条件をruntimeに、残りをFuzzingへ置く層構造が普通です。
T8のstorage費用と同様に、安全性は通常Gasで買います。
自分のコードは同じでも、interface意味、手数料、再入防御が変わり、仮定も変わり得ます。
報告は当時の依存版へのsnapshotです。
重要な依存仮定も不変条件へ書き、実装アドレス変更のalertを加えます。
全権accountは不変条件、Fuzzing、監査の全てを迂回できます。
第一問で忘れやすい攻撃者は自分自身です。 multisig、timelock、最小権限は、この層で再監査より安いことが多いです。
持ち帰る問い
報告は通常損失への免責を記します。リスクはprotocolと利用者に残り、監査は確率を下げるだけです。監査済みを保証と読む誤りは高く付きます。
Blockchainではコードと状態が公開され、誰でも不変条件を検証できます。誰でも実行できる公開検証にすれば、PDFより信頼できます。これは圧力であり機会です。
補助金停止後の利用者という問いを、安全性では、teamが解散しても安全か？ と置き換えます。人の監視だけに頼れば否定的ですが、不変条件と権限設計なら肯定できるかもしれません。
章末チェック
脅威モデルと不変条件一覧です。
発見は過去を記し、変更は対象外です。脅威モデルは境界を定義し、不変条件はrepositoryと共に自動実行します。
違反したら損失や支配権喪失があるかを問います。
利用者残高合計が保有資産以下なら、違反で引き出せない人が出るので安全性です。 array長が人数と同じなら、実装変更だけかもしれず、安全性は変わりません。
本当の脆弱性は単一callの引数より、call列にあります。
個別関数は正しくても特定順序で丸めが累積し、不正な状態の組み合わせへ入ります。毎回初期化するstateless方式では届きません。
失敗しない確認は確認がないのと同じで、偽の安心を与えます。
assertに到達せず、Fuzzingが経路を通っていないかもしれません。実際に赤にして初めて、生きていると分かります。
T12の失敗例を先に書く原則と同じです。
標準解答はありません。三点を確認します。
- ないふりをせず、実際に書いたか。
- 発生時の負担者を全項目で示したか。
- 自分自身の管理鍵、multisig、upgrade権限を含めたか。
第三は忘れやすく、全ての仕事を迂回する経路です。
要点
監査の真の成果は PDF ではなく、脅威モデルと不変条件だ。