Modeling State Transitions to Find Unique Bugs
三句話摘要
Smart contract 審計師 Phil 分享如何用 Excel 試算表對狀態轉換建模，並以此發現一個會在第六年將整個協議「磚化」的整數下溢漏洞。 把合約狀態轉換搬到 Excel 試算表，讓你能模擬不同時間戳與參數，是在 400 人競賽中唯一發現「第六年磚化漏洞」的關鍵方法論。 狀態轉換是漏洞的溫床：所有漏洞幾乎都藏在改變合約狀態的函數裡，因此審計時必須徹底理解每個函數的讀寫順序與合法輸入範圍，單憑程式碼瀏覽或流程圖難以窮舉邊界條件。
重點整理
重點- 1
狀態轉換是漏洞的溫床：所有漏洞幾乎都藏在改變合約狀態的函數裡，因此審計時必須徹底理解每個函數的讀寫順序與合法輸入範圍，單憑程式碼瀏覽或流程圖難以窮舉邊界條件。
- 2
試算表讓「輸入測試」成為可能：流程圖可視化邏輯，但無法動態模擬不同參數。Excel 模型可以逐列填入不同時間戳或數值，直接觀察狀態如何演變，等同於手動 fuzzing。
- 3
時間戳邊界是關鍵問題域：以年為週期的 halving faucet，若在預期時間點之外被呼叫（例如跳過一年或延遲一個區塊），其週期計算邏輯並不健全，是此類合約最常被忽略的風險面。
- 4
「唯一發現」驗證方法價值：在 400+ 研究員的競賽環境下，這個 bug 只有 Phil 一人找到，說明結構化建模帶來的視角優勢，而非單靠程式碼直覺。
實用技巧與重點
乾貨- 工具：Microsoft Excel（試算表建模狀態轉換）
- 建模結構：橫軸 = 函數呼叫前後狀態快照；縱軸 = 各次函數呼叫；底部輔助區 = 函數逐步邏輯拆解
- 漏洞類型：整數下溢（underflow）
- 觸發條件：halving faucet 分發函數在最後一次分發時，若比預期時間戳晚 12 秒（主網 1 個區塊）呼叫即觸發
- 後果：協議在第 6 年若函數未精確命中時間戳，整個協議永久磚化（bricked）
- 競賽規模：400+ 名研究員參與，此為 unique bug（唯一發現）
- 適用場景：任何帶有時間週期邏輯的代幣分發、減半、歸屬合約
結論
結論“把合約狀態轉換搬到 Excel 試算表，讓你能模擬不同時間戳與參數，是在 400 人競賽中唯一發現「第六年磚化漏洞」的關鍵方法論。”
完整解析
詳細審計智能合約時，最危險的地方不是靜態變數，而是那些改變合約狀態的函數。Phil 在這場分享中指出，要真正掌握一個狀態轉換函數的風險，必須同時理解它的執行步驟、讀寫了哪些狀態、以及所有可能的輸入參數——而光靠閱讀程式碼或畫流程圖，很難涵蓋這些維度。流程圖的致命缺點在於它是靜態的，你無法在上面「輸入不同的參數」來觀察會發生什麼。
Phil 的解決方案是把狀態轉換移到 Excel 試算表上建模。他的設計很直覺：橫軸記錄每次函數呼叫前後的狀態快照，縱軸對應各次呼叫，底部再拆解函數的逐步邏輯。這樣一來，審計師可以像填財務預測表一樣，逐列輸入不同的時間戳或數值，直接看到狀態如何演變，本質上是一種手動的邊界條件測試。
他示範了一個真實世界案例：一個每年減半分發代幣的 halving faucet 合約。在建模過程中，他自問了兩個問題：減半邊界是否被正確處理？如果函數沒有在某一年的預期時間點被呼叫，隔年會發生什麼？他把整個代幣分發時程全部列入試算表，最終發現：在最後一輪分發時，若呼叫時間比預期時間戳晚了 12 秒——也就是以太坊主網上晚一個區塊——運算就會發生整數下溢，直接讓合約無法再運作。
這個漏洞的嚴重性在於它的時間性：不是立即崩潰，而是會在第六年、當協議已運行多年之後，因為一次稍微不準時的呼叫而永久停擺。這個 bug 出現在一場超過 400 名研究員參與的公開競賽中，而且是唯一一個人發現的，對 Phil 來說，這正是試算表建模法真實價值的最佳證明。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
