審 Miden 挖得深，是因為審之前先花六個月讓 agent 做工具跟 Lean 模型

https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/

Fredrik Dahlgren 2026 年 9 月 18 日在 Trail of Bits 的部落格寫這次怎麼審 Miden。2025 年底，Miden 團隊找他們，要在上線前看過 zkVM 的一部分。這是一台新的零知識虛擬機，組語是自己的，叫 Miden assembly，簡稱 MASM。範圍裡有 core library：一小撮密碼元件，用 MASM 寫成。

機器是 stack machine。指令不把運算元寫在旁邊，要的值從堆疊拿，結果再壓回堆疊頂端。同一件 XOR，Dahlgren 放了兩欄。左邊是 MASM，把兩個 128-bit 的值做互斥或，每個值拆成 32-bit limb，也就是大數切出來的一塊。右邊是同一件事的 32-bit x86。x86 那欄看得到暫存器寫在指令上。MASM 那欄要審的人自己數：這兩個 128-bit 的值在堆疊上佔了哪些 32-bit 槽、算完之後頂端又是什麼。架構又新，IDE、LSP、linter 幾乎都還沒有。

這份 core library 是高保證場景下的複雜密碼程式，寫在他們之前沒看過的低階組語上。實作當時還沒把功能做完，所以審核之前有六個月可以準備，工具趕得上在審核開始前就位。Dahlgren 寫，他們問自己的是：時間跟 token 要花在哪，審的時候才有辦法在這份程式裡挖出盡可能多的 bug。

許多資安公司最近寫過同一種文章，Trail of Bits 自己也寫過，站內分類掛在 patch-the-planet：把 agent harness 對準一份 codebase，找出數十個 bug。那些文章的重心在 agentic code review，審核已經開始，agent 讀程式、報問題。Dahlgren 把時間軸往前挪。審核開始之前，agent 已經可以幫團隊做出專用工具跟形式模型。Miden 這次就是把六個月花在這裡。從零做出四樣：LSP server，repo 是 masm-lsp；decompiler，repo 是 masm-decompiler；靜態分析引擎，pass 放在 masm-lsp 裡的 masm-analysis；還有一份用 Lean 寫的 VM executor 模型，repo 是 masm-lean。

VS Code 得先看懂堆疊上的每一條指令

開工前他們先問，專案真正開始審的時候，手上想要哪些工具。平常用 VS Code。語法上色跟程式導覽是基本盤，沒有這兩樣，資料流追不下去，一段密碼元件的呼叫關係也跳不過去。MASM 當時沒有 LSP，也沒有對應的 VS Code 擴充。

幾天之內，Claude 做出 masm-lsp 的可用原型：語法上色、跳到定義、找出引用，滑鼠停在 procedure 上會顯示說明。Procedure 是 MASM 裡一段可呼叫的程序。基本功能就位之後，又加上這種語言才需要的兩樣：指令的行內文件，以及單一指令的 stack effect。Stack effect 就是這條指令從堆疊拿走幾個值、放回幾個值。

圖上，文件跟 stack effect 貼在指令旁邊。看的人不必切去另一份文件查這條指令的語意。下一條指令吃到什麼，全看堆疊此刻的形狀。形狀若只存在讀碼的人腦袋裡，審 core library 會一路在重數堆疊。

看得到指令之後，下一個問題是高階的控制流跟資料流。他們想在 VS Code 裡對 MASM procedure 做忠實的反組譯。忠實，指的是翻出來的流程要跟原本那段 MASM 對得上，讓審的人不用自己把一串堆疊操作還原成比較高的結構。這份語意資訊同時要給手動審，也要給後來的 agent 審。

手寫 MASM 有四種對不齊，所以反組譯只保一個子集

堆疊機怎麼還原、怎麼反組譯，文獻裡研究過。手寫的 MASM 仍然難，難在四種堆疊對不齊。每一種都會讓「翻出來還保證正確」失敗。

Core library 裡大多數 procedure 沒有宣告簽名。輸入幾個、輸出幾個，得從上下文推。推錯一個，後面每條指令的運算元都錯位，反組譯會把隔壁槽的值當成這次的參數。

MASM 的 procedure 沒有一套定義清楚的呼叫慣例。一次呼叫對堆疊的淨效果，通常無法靜態決定。有簽名的呼叫，分析器知道淨高度差，呼叫回來可以把堆疊地圖接上。這裡多數沒有那張簽名。分析器看到 call，不知道它吃掉幾個、吐回幾個，呼叫點之後的地圖就斷了。某一層失敗，失敗會沿著呼叫鏈往上傳。上面的 procedure 就算自己長得規矩，底下有一個算不準，整條鏈的形狀都不可信。

While 迴圈不必維持堆疊平衡。條件每一輪可以佔在不同的 stack slot。迴圈若維持平衡，條件可以留在同一個槽。這裡沒有這條義務。例如本體多推了一個值，下一輪的條件就挪到旁邊的槽。反組譯若還把「條件」綁在舊槽，看的是另一個值，後面的指令也沒辦法把輸入對回固定位置。這是「全部都翻、又要翻對」做不到的原因之一。

條件分支的兩邊可以有不同的 stack effect。例如一邊離開時堆疊少了一格，另一邊沒有，兩邊高度就不一樣。簽名要的是一個固定的輸入輸出個數，高度不一樣就沒有那個數。硬給一個，其中一邊會用錯槽。堆疊追蹤也在這裡斷掉。

全部都翻、又要每一段都翻對，兩件事一起做不到。範圍收成一個定義清楚的子集，只對這個子集保證反組譯正確。

開發時兩種模型輪替。Claude 做規劃跟開發，Codex 做 code review。一個功能做完，就讓 agent 從 core library 隨機抽一批 procedure，反組譯，再跟原本的 MASM 比對。比對要找的是回歸：這次改動有沒有把已經翻對的 procedure 弄壞。對不上的例子寫進回歸測試，交給模型修。抽樣抓的是 decompiler 自己有沒有退步。Miden 的密碼算得對不對，要看中間表示式上的分析，以及後來的 Lean。

Decompiler 是這次工具開發裡最大的一塊，跨了好幾個月，超過一百筆由 AI 產生的 commit。

事後被重複拿去用的，是 decompiler 內部的分析框架跟中間表示式。中間表示式裡，每條指令的輸入跟輸出已經填成運算式。堆疊上那些隱含的讀寫，到了這裡變成可以指稱的式子。後面的靜態分析吃的是這份式子。完整反組譯管線印出來的偽碼留在 VS Code 裡，給人看控制流。

Dahlgren 附了一段對照，讓人看見子集裡翻得出來的樣子。Procedure eqz 檢查一個 256-bit 整數是不是零，這個整數表示成八個 32-bit limb。圖的上方是 MASM，下方是對應的反組譯偽碼。它是一個翻成功的例子。手寫 MASM 那四種對不齊還在，這個例子沒有把保證擴大成全部 procedure。

中間表示式上，只問三件查得到的事

有了中間表示式，資料流這類標準做法就能用在 MASM 上。他們在表示式上建了多個 analysis pass。Pass 問的事情就三件，三件都對得回程式裡的一個位置。

Prover 提供的 advice 值有沒有被驗證。Advice 是預先算好的輸入，例如餘數、模反元素。它不走程式運算的那條堆疊，而走 prover 另開的 advice stack。證明者先把值放好，MASM 再讀。讀進來的當下，這段 procedure 還沒有自己算過這個數。Pass 要問的是：使用之前，有沒有檢查把它收成該有的型別或範圍。沒有這次檢查，後面的指令用到的就是證明者給的原值。

型別限制有沒有被執行。例如某個輸入必須是 32-bit 整數，或必須是布林。限制靠檢查才存在。檢查沒做，後面的指令還是可以把那個值照這種型別拿去算。

區域變數在所有執行路徑上有沒有初始化。有路徑沒寫入就讀，分析要能指出那條路徑。

看這些問題的做法是抽象詮釋。分析不代入真實的數字。堆疊上每個位置只記可能的型別，像「32-bit 整數」，或「未知」。它把程序走完。若這一輪讓某個位置的型別變得更具體，就再走一輪，直到一整輪下來沒有新資訊。每一種可能的值都被記著，而且記的時候留了一點餘裕，真實執行會碰到的情況不會漏。所以某個檢查在分析裡通過，每一次實際執行也成立。餘裕也表示分析有時比實際情況更寬：一個其實已經是 32-bit 的值，仍可能被標成「未知」。寬，是為了不把真的會發生的情況漏掉。通過是強結論，因為它不會把一個沒有檢查的值標成已經檢查過。標成「未知」的位置，分析沒有給出那句保證，要另外看。

三個 pass 都建在這個引擎上。Advice、型別、初始化，問的都是分析通過之後那句保證還在不在。

Claude 跟 Codex 先做出通用的抽象詮釋引擎，再在上面寫具體的 pass。Agent 同樣在開發跟審碼之間切換，規劃跟開發走 Claude，審碼走 Codex。他們還讓 agent 為 decompiler 跟新的 MASM linter 設計命令列介面。人手在 VS Code 裡看 stack effect 跟反組譯，agent 走 CLI，把同一套分析放進 agent 驅動的審碼流程。

超過四百處是型別，高嚴重度是 mod_12289 的餘數

正式審核時，這些分析找到超過四百處獨特位置，型別驗證還可以加強。每一處都能從函式庫的公開 API 到達。另外有一條高嚴重度。兩邊的嚴重度不在同一級。

超過四百處，多數跟公開 API 有關。Dahlgren 的註腳寫，core library 幾乎每一個 procedure 都在公開 API 上，第三方開發者可能在沒有適當驗證的情況下呼叫它們。這些位置從函式庫外面就到得了，是還能加強的型別驗證。高嚴重度只有下面那一條。

高嚴重度出在 procedure mod_12289。它要做的事很窄：把一個 64-bit 的值對 12289 取模，回傳餘數。商跟餘數不由這段 MASM 自己除出來。Prover 把兩個數當成 advice 放上另一條 advice stack，跟程式運算用的那條堆疊分開，procedure 再讀進來。

商有檢查，必須是合法的 64-bit，表示成兩個 32-bit limb。餘數沒有同等的檢查。它從 advice stack 讀出來，直接送進 32-bit 指令 u32overflowing_sub。圖上記的就是這個缺口：餘數沒被驗證成合法的 64-bit 整數。

以這套型別追蹤的詞彙來說，沒有那次驗證，餘數就不會被收成「合法的 64-bit」，只會留在「未知」。

他們接著調整的是商跟餘數這兩個 advice。兩個值可以一起變，變完之後，u32overflowing_sub 的約束仍然成立，mod_12289 回傳的卻已經不是正確的餘數。減法只看見自己的輸入還滿足約束。它看不見回傳值是不是「這個 64-bit 數對 12289 取模」該得到的那個餘數。惡意 prover 把這組對好的商跟餘數送進來，就可以偽造 Falcon 簽章，並且把任何由 Falcon 金鑰對控制的 Miden 帳戶裡的資金轉走。

這是惡意 prover 做得到的事。Dahlgren 寫的是潛在後果。文章沒有記載已經發生的損失，也沒有寫出已經短少的金額。

寫對的 procedure，用 Lean 把對寫成一句堆疊等式

進審核那天，手動審跟 agent 審都已經有工具：LSP、子集上的反組譯、中間表示式上的那些 pass，加上給 agent 用的命令列。六個月裡他們還留了一個問題。Core library 的 procedure 如果確實寫對、裡面沒有 bug，能不能用證明助理 Lean 把「寫對了」證明出來。

Miden VM 適合做形式模型。指令集小，多數指令沒有副作用，一個最小的 executor 就夠把指令對堆疊的影響寫進 Lean。他們先實作這個 executor，repo 是 masm-lean，再讓 Claude 做一支自動翻譯器，把 MASM procedure 翻進 Lean。六個月的準備包含這份模型。95 條證明是審核期間的產物。那段時間多個 agent 平行跑，能證明多少 procedure 就證明多少。同一段時間裡，還產生了這些證明用到的 Lean 函式庫。

Lean 的 kernel 會檢查生成出來的證明是否正確。人不用逐行重算推導。要審的是定理敘述：這條定理是不是真的在講對應那個 procedure 的正確性質。敘述若審錯，kernel 仍會接受證明，接受的是另一句話。

為了讓敘述好審，他們為 field element（體裡的元素），以及 core library 實作的整數型別，引進 Lean 的型別。高階的正確性大多寫成同一種句子。輸入堆疊寫成 [x1, x2, ..., xn, ...]，前 n 個是參數，最後那個 ... 是參數底下、呼叫者留下的值。執行 procedure P 之後，堆疊要變成 [P(x1, ..., xn), ...]：參數換成一個結果，呼叫者那一串還在，而且 P 會終止。人對著這句話看參數個數、結果、終止、呼叫者的值還在不在。證明推導對不對，交給 kernel。

這輪做出 95 條機器檢查過的正確性證明，蓋住 core library 全部的二元算術元件。Dahlgren 也把這塊稱為 core library 很大的一塊。95 條的範圍停在二元算術。沒進這 95 條的 procedure，不在這次證明裡。

同一份工作抓到既有單元測試沒抓到的兩個細錯。

第一個在 64-bit 右旋 rotr。行為不正確，是兩個條件同時成立的時候：輸入大於 Goldilocks prime，而且旋轉量是 32 的倍數。既有單元測試沒抓到這個邊界。形式化去做正確性證明時，證明要額外假設 shift mod 32 ≠ 0 才過得去。想讓定理涵蓋每一種 shift，證明站不住。補上那條假設之後，證明過了，「32 的倍數」就留在定理外面。人審敘述時看到的，就是這條多出來的假設。

第二個在 256-bit 乘法 wrapping_mul。它在回傳之前，把呼叫者擁有、還留在堆疊上的值丟掉。依那句高階正確性，呼叫者留在參數底下的值，procedure 結束後應該還在。這裡在回傳前把它們拿掉了。

做不成的 side project，成本落到 token

上線前做出的工具，以及審核期間產生的 Lean 函式庫跟證明，都是 side project。一兩年前，Trail of Bits 不會為這種專案撥時間跟資源。探索性高，最後做得出什麼、報酬在哪，事先很難估。這種專案也很難在開工前賣給客戶。LSP、反組譯、抽象詮釋、一份 Lean 裡的虛擬機，都要等做完才知道報酬在哪。

過去這一年，agent 變得夠用。這類非必要的專案可以在輕度監督下往前做。哪些專案值得開工，這筆帳變了。Dahlgren 的說法是：今天一個做不成的 side project，成本只有 token。

這次的輕度監督有具體的位置。做工具時，Claude 負責規劃跟開發，Codex 負責審碼，回歸測試把 decompiler 的退步留住。做證明時，kernel 檢查推導，人檢查定理敘述。審核沒有交給一段無人看管的 agent 跑完。

對 Miden，準備工作的結果對得回來。LSP 跟靜態分析引擎讓手動審蓋到更多地方，也讓 agent 驅動的審核跑得了同一批工具，並且在程式裡找到真實的安全問題。手動審走 VS Code 裡的跳轉、stack effect 跟子集上的反組譯。Agent 審走 decompiler 跟 linter 的命令列。Dahlgren 寫，這些問題有可能導致數百萬美元的資金損失。有可能，指的是潛在影響。這裡沒有一筆已經發生、可以入帳的金額。

AI 生成的 Lean 正確性證明，把函式庫裡一大塊基礎元件的保證拉高。團隊可以放心地在這塊二元算術上繼續做。Miden 團隊已經採用這次做出的靜態分析引擎。之後 core library 的更新，也會走到這套分析。

Dahlgren 寫，這是他在 Trail of Bits 這些年裡比較有意思的專案之一。做類似事情的人，文章末尾留了聯絡方式。

深度來自律可以重跑的保證。分析通過，就對每一次執行成立。證明由 kernel 驗，敘述由人驗。反組譯的正確性停在定義清楚的子集。成本變成 token 之後，這三條還在。