第一次認真進行審計時，我打開儲存庫中最大的合約，開始從第一行閱讀。兩小時後我頭痛欲裂，卻沒有任何發現。我記住了程式碼的運作方式，卻從未詢問它應該保證什麼。這是本末倒置，花了我一段時間才改掉這個習慣。

現在我不再先讀 Solidity。我會先讀範圍，在查看任何函式主體之前，寫下哪些條件必須始終成立。Bug 就是這些條件的違反。如果你不知道這些條件，你只是在欣賞程式碼。

第一步：在閱讀前寫下不變量

不變量是協議聲稱無論誰以何種順序呼叫，始終成立的屬性。對於競賽，我從資金和控制權開始，因為這是嚴重性所在。

兩個問題涵蓋了大部分內容：

  • 誰可以在什麼條件下移動資金？
  • 關於會計記錄，哪些條件必須始終成立？

對於借貸池類型的協議，我的初始不變量清單如下，以白話寫下，暫不考慮任何實作：

  • 所有使用者存款總額減去所有借款，應等於池子的可用流動性加上未償債務。會計必須一致。
  • 使用者只能提取自己的餘額，不能提取更多，也不能提取他人的。
  • 只有在部位確實低於健康門檻時，才能被清算。
  • 利息單調累積，不會倒退導致有人償還少於所欠金額。
  • 只有借款人，或清算人對不健康部位，才能減少債務。
  • 除治理機制外，任何人不得更改利率參數或預言機。

注意，上述清單未提及任何函式名稱。這些是協議的承諾。我在競賽中剩餘的工作很簡單：找出呼叫順序以打破其中一項。

第二步：映射外部入口點

資金不會憑空轉移。狀態改變必須由外部呼叫觸發。因此我列出所有可從外部到達的函式，因為攻擊面正是這組函式，別無其他。

我先用 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 威脅會計一致性；withdraw 威脅「只能提取自己的餘額」規則；liquidate 威脅「僅在不健康時」規則；設定器威脅「僅治理可執行」規則。此時我擁有一個矩陣：入口點在左，右側是不變量，相交處就是我將深入搜尋的區域。

第三步：繪製信任邊界

大多數真實發現都存在於協議信任了不該完全信任的交界處。在閱讀邏輯前，我標記每一處邊界：

  • 預言機。價格來源是什麼？是否可在單一交易內被操縱（AMM 的即時價格是經典陷阱）？若回傳過時、零值或 revert，會發生什麼？
  • 管理員與角色。特權角色可以做什麼？特權路徑是否可透過 proxy 或 delegatecall 意外被觸達？「管理員可以 rug」通常不在範圍內，但「非管理員可觸及管理員功能」屬 High。
  • 跨合約呼叫。每一次外部呼叫都是控制權離開合約、可能返回（重入），或被呼叫者惡意行為（惡意代幣、轉帳收費、回溯代幣）的機會。
  • 代幣假設。程式碼是否假設 18 位小數？假設 transfer 回傳 bool？假設轉帳無手續費？每項假設都是敵對代幣可跨越的邊界。

對借貸池而言，我會先查看預言機邊界，因為「操縱價格、以膨脹抵押品借款、離開」是許多 High 級漏洞的典型形態。

第四步：現在閱讀程式碼，尋找違規

直到現在我才打開函式主體。而且我不是在讀「這做了什麼」，而是「這觸及哪項不變量，我能在這裡打破它嗎」。

以下是一個簡短範例。借貸池形態的偽碼，故意包含錯誤：

// 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

以不變量優先的思維，我不會問「這是否轉移代幣」，而是問「這是否強制只能提取自己的餘額」。答案是否定的，減法前沒有邊界檢查。在舊版 Solidity 會 underflow 成巨額餘額；在 0.8+ 會 revert，因此可能安全……除非 amountToShares 的取整讓 shares 變成零而 amount 不為零，此時你能提取代幣卻扣除零。這就是漏洞所在。我會用 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 即時價格。資金充足的攻擊者可用閃電貸在單一交易內推高價格，讓健康部位看起來不健康，進而清算獲利。問題不在算術，而在信任可操縱的來源。不變量優先的思維能找到它，因為我在第三步就已標記預言機為邊界，遠在閱讀此函式之前。

為什麼這個順序重要

如果你先讀程式碼，會被「它如何運作」所錨定，開始相信它。作者的思維模型會滲透到你的思維。你最終檢查的是「程式碼是否做了它看起來想做的」，這與審計相反。審計是檢查「程式碼能否被讓去做它絕不該做的」。

不變量優先翻轉了框架。你先獨立於實作，決定協議承諾了什麼。然後每個函式都成為對照這些承諾的嫌疑犯。當我建立 spectr-ai 時，就是試圖把這個結構嵌入它的推理方式：先陳述屬性，再對照它們檢查程式碼，而不是漫無目的地聯想「漏洞」。

這樣也更快。在我這週挑選的競賽中，寫不變量清單花了約 40 分鐘，卻把 2,000 行程式碼縮短成「這裡有六件值得打破的事，以及三個最可能打破的交界處」。這是一張地圖。從第一行讀到第二千行，只是漫無目的的遊走。

當你面對不熟悉的程式碼庫時，你會先寫下哪些條件必須始終成立，再閱讀，還是直接鑽進程式碼，邊讀邊重建規則？