https://softwareengineeringdaily.com/podcasts/security-in-the-age-of-instant-exploits/

MongoDB 那則漏洞報告一公開，丟給 Claude，就能拿回一份完整的 exploit。Alon Schindel 記得另一個速度。他加入 Wiz 之後，最早公開的漏洞裡，有一則 Apache HTTP server 的 critical 漏洞。報告出來，大約還要兩天到三天，才看得到 exploit。

Alon 是 Wiz 的 AI 與威脅研究副總裁。Wiz 做雲端資安平台，2026 年被 Google 買下。公司成立六年，他大約五年半前加入。這一集的主持人是 Gregor van，人在新加坡，自己是 CTO，也是創辦人，做的是溝通、資安和 AI 交界的事。他最近創的公司叫 Wintic AI，在想 AI 時代的 email 可以長成什麼樣子。大約兩年前，Gregor 也請過 Wiz 的 Rami McCarthy 上這個節目。

Alon 做資安超過二十年。三、四年級就在做網站，喜歡把東西做出來，也一直想知道自己的網站會怎麼被打。後來在學校、在工作，只要能選資安，他就往那邊走。帶過他的人裡有業界的前輩。其中一位是兒時朋友，同一間幼稚園，五歲就認識。這位朋友認識 Wiz 的創辦人，是最早進去的工程師之一，差不多第一天就在。公司成立幾個月、想擴大的時候，他傳訊問 Alon 現在在做什麼、有沒有空談一個新機會。Alon 說聽起來有意思。他覺得這種從小開始的關係，值得一直留著。

這六年他覺得什麼都看過。2021 年的 Log4j，是他眼裡最大的漏洞之一。眼下則是供應鏈攻擊，Shai Hulud 這一波，以及其他類似的 GitHub 蠕蟲。可是一扯到 AI 怎麼改資安，他又覺得得重來。挑戰是真的，節奏比以前都快。公司滿六歲，體感卻像去年才開始。

談 AI 跟資安，他要人把兩件事分開。一件是用 AI 做資安。另一件是去保護 AI，以及 AI 一出現，攻擊方多出來的入口。兩邊都得談。他說現在像換了一套物理規則。以前公開、等人寫出 exploit、再被人掃到，這些節奏都在改。

公開到能打，Gregor 看著表一路往下改

Gregor 先轉述 Firefox 團隊的說法。2026 年 4 月，他們修掉的資安 bug，比前一整年還多。原因是 Anthropic 的模型 Mythos。這支模型中間下線過一陣子。以他們錄音時的理解，大約在錄音六天前又回來了。當天談的時候它是開著的。他補了一句，若這集播出時它又下線，先跟聽眾道歉。他還點到 Fable，說是搭配的另一支。

Alon 覺得 Mythos 聲音很大，像把產業叫醒，但不是起點。模型變得擅長找漏洞，他們去年就看到了。去年十二月，Wiz 辦了一場 AI 漏洞競賽，請人來挖軟體、雲端軟體、AI 軟體裡的洞。名次排在前面的隊伍，多數用了 AI。那場競賽比 Mythos 公開早了大約四個月到五個月。他也一直說，Opus 4.6、Gemini，還有 OpenAI 的 GPT-5.5，找漏洞很強，寫軟體一樣強。

Gregor 對照的是 Alon 文章裡提到的 zerodayclock.com。節目開頭先說，漏洞公開到打得動，以前的空檔常常以月計。那張圖則一路往下。2021 年，從發現到被人打進去要一年，當時已經讓人覺得很快。2025 年掉到一個月。錄到 2026 年，Gregor 盯著格子改口。先說一週，又改成這一年也已經到一天。五年裡，從還有一年可以補，變成能有一整天就算幸運。他當時還估，下一格就是一小時，所以也許已經低於二十四小時，大概二十小時。網站自己估，2027 年可能到一小時，甚至一分鐘。

Alon 同意這個壓縮。他負責找洞，也負責洞公開之後怎麼回應。過去這一年幾乎是一則接一則在處理。洞變多，exploit 出現得更快，回應就得更快。

節目後段，Gregor 再看一次那張表。2026 年實際落到兩小時。一小時那格還沒勾，因為還沒到一小時。

一個人在家，就能掃整片網路

Alon 把眼下叫成：找洞變得人人做得起，打網站更容易。他假設自己十歲就有 Opus，還不必是 Mythos，已經夠拿去掃網路上露在外面的資料，或是那些一觸發就把 secret 交出來的 Lambda 函式。門檻一直在降。基本功還在，你得懂自己在講的東西。模型是來幫忙的。

Wiz 比較早拿 AI 做的一件事，是 red agent，自動化的攻擊方。功能做得很快，也很快開給幾千個客戶。他覺得這大概是他們看過採用最快的功能之一，因為有效。掃網頁，掃 HTML，掃 JavaScript，AI 會用駭客的方式讀，把暴露找出來。以前看過很強的駭客，也看過 APT、國家級的隊伍。那些要時間、要功夫、要技術。現在一個人待在家裡，就能跑大規模掃描，把暴露找出來。

換到藍隊，也就是防守這側，他覺得同時出現機會。事情在變，不表示長期一定變得更糟。

防守方看得到家裡什麼重要

他樂觀，是因為 context。五年前他們做產品，已經靠 context 排優先順序。現在模型沒有 context 就做不好。context 愈準，掃出來的結果愈準。

Wiz 的掃法是內外一起。從裡面看環境，知道哪些資源重要、敏感資料在哪、一家組織最不能被帶走的東西在哪。用這些線索把掃描變聰明，依敏感程度、依對系統有多關鍵來排。手上有「這個資源裡大概是什麼」的提示，再從外面像攻擊方一樣掃那個頁面，掃描時帶著提示。他說這樣很有效。他們在外面找到幾千則漏洞和嚴重暴露。若不是他們先找到，就可能是攻擊方。資料本來就露在那裡。

掃的時候讀 HTML、讀 JavaScript，看什麼露在外面。有時是 token，GitHub PAT 或其他 token，不小心嵌在網頁裡。誰都讀得到，拿去登進那家公司的系統，攻擊就從那裡開始。接下來可以把資料帶走。若是 GitHub 的 token，也可以往產品或那家公司做的套件裡加一段惡意 script，感染下游客戶。供應鏈攻擊可以從這裡開始。

攻擊方會怎麼用 AI，防守方就照同一個用法去做。他先把一個假設擺上桌：雙方用得到同一等級的模型。這個假設成不成立，可以再爭。在這個假設下，防守方知道家裡有什麼、什麼重要。攻擊方做得到的是硬試和廣掃。真正進來之前，不知道什麼才重要。他認為優勢在防守方。

Gregor 補的是，AI 出現之前，這些 context 住在寫過程式的人身上。這段怎麼拼起來的，哪一段是趕工推出去、自己也不太有信心的，哪一段資安工程師沒看夠久，哪一段有更多人看過。GitHub 上的歷史也算。某個 pull request 底下有人寫，先上線吧，可是他不太放心。這些都可以放進防守用的 context。

開源維護者一週要看幾十則、上百則

負責任揭露，Alon 說原則是遵守各平台不同的規則。他講的幾千則發現，是 Wiz 產品裡看得到的那些。系統標成非常嚴重、可能真有暴露的，他們會試著用資安信箱，或直接聯絡那家公司，走跟其他報告一樣的路。若是客戶，就直接找資安團隊。

規模一大，壓力換到開源和小型維護者身上。上週他看到一個例子。一個開源專案揭露了一則漏洞，來報的公司或研究人員，他記得大概十五個。原因是大家都在用 AI 掃這些專案。他說，小型維護者一週可能收到幾十則、上百則，來自不同公司。哪一則先看，變成難事。有些維護者已經講明，AI 生成的報告他們不回。裡面還有 AI slop，也就是垃圾報告。要看的資料變多，是 AI 另外造出來的負擔。

Wiz 自己人夠，報告送得到該去的地方。多數問題在產品裡報給客戶，客戶的資安團隊有流程可以接。開源不是這種條件。有人用業餘時間做了一件對大家都好的事，現在卻因為回得不夠快而被羞辱。他們沒有那些資源。這就是他們的生活。

他因此覺得 Firefox、Mozilla 那個方向重要。眼下該做的，是前沿實驗室跟這些構成網路骨幹的關鍵開源專案一起掃，幫他們在攻擊方之前把洞找出來。他知道 Google、OpenAI、Anthropic 都在這件事上花力氣。他認為得現在做，趁這些能力還沒擴散到攻擊方手上。

沒有人有一套完美的自動修復

時間若只剩一天，甚至更短，Gregor 把修補講成得變成持續、自動、中間沒有人。他說這一直是大家想摸到的那個終點。漏洞一宣布，就有 agent 去處理。Wiz 攻擊那側有 red agent，回應那側有 green agent。

Alon 把全自動想成一圈：找到暴露，分析，再自動修。他直接說，這件事不容易。他不覺得今天有誰握著完美解。聽這集的人，手上很多系統已經放了很多年，裡面有舊程式。他不想讓人以為世上有個完美做法，自己沒採用，就該覺得差勁。

先持續掃。第一層掃得寬、掃得淺，就像 red agent 那樣，一直看自己的攻擊面，弄清楚什麼暴露在外。攻擊面不只有網站。GitHub 專案要掃。最近這波供應鏈攻擊就是從那邊來的。CI/CD 管線要掃。任何可能被打的資源都要掃，用 AI 持續掃，想在攻擊方之前找到。

下一步是看這件事可能有多嚴重。文章裡的 AI threat readiness framework，是要公司、資安團隊和軟體工程團隊重新想怎麼回應漏洞。其中一塊就是把暴露縮小。不該有東西露在外面，這句老話現在變得要緊，因為露在外面的東西，大家找得到，也打得很快。他看到的很多情況，問題不只是漏洞本身，而是那個資源根本不該公開。先把這類收掉。

若一個資源上確實有能被利用的漏洞，可能是設定錯誤，也可能是你自己程式裡的洞，偏 AppSec、應用程式這側，才開始排修復。green agent 從這裡接手。它先追這則問題從哪來，找根因。這一步平常被忽略。外面看到一個暴露，要對回公司裡的負責人，對回那個程式檔，以前非常難，現在仍不容易。AI 若同時看得到暴露的資料和程式庫，就幫得上。他們把這段叫 cloud to code：找出問題的源頭，再排修復步驟。

AI 不只好打，也會寫、會讀軟體。他們在做的 agent，找到問題之後會排出修復做法，有時給出好幾種。還可以加記憶，把指示寫進 agent。你可以要求它一律先修補。也可以要求它優先改 Terraform，把暴露收掉，先動程式以外的東西。

自動修補，產業還在弄懂怎麼做。補完要測。下一階是怎麼自動測新程式，確認這次改動沒有打到系統別的地方。這條自動流程，有些情況跑得起來，剩下的還很多。有時得改架構，才比較容易走完。安全映像檔是其中一條。用比較好的架構，組織可以把從掃到測這整段走得比較快。

Gregor 把安全映像檔說成大家也叫的 hardened image，或 hardened container。他覺得開發者要吞的代價，是工具鏈受限制，或容器得做特別修改。想讓整條供應鏈安全一點，團隊得接受這個交換。

熱門套件若沒人顧，像一顆定時炸彈

外面那些函式庫和套件，風險也在變。有些套件維護得不好。他說他們不去評判維護者，對方的挑戰已經很大。研究裡他們會掃公開的專案、CI/CD、GitHub Actions，並且負責任地跟維護者合作。很多專案有暴露。一個很紅、很多組織在用、又有暴露、安全習慣又不好的套件，他看成定時炸彈。

所以縮小暴露，不只有把公開資源收起來。還有審查你在用的開源程式，從比較安全的 SBOM 開始選。SBOM 是軟體物料清單，也就是這份程式到底裝了哪些套件。他說的把安全往開發更前面挪，還有架構上的改變，不只有安全映像檔。也包括一開始就把這份清單選得安全一點。他不覺得這會容易。軟體開發者大概都不想停用一個熱門函式庫。

不安全的套件用得更多，原因之一也是 AI。用 coding agent 寫程式，很多時候你根本不知道裡面有什麼。相依套件是 agent 加進去的。弄清楚自己程式裡有什麼，把選擇做對，這件事還是重要。他希望 coding agent 以後也會把比較安全的架構、比較安全的 SBOM 排進優先。

靜態分析看圖案，模型開始看懂程式在做什麼

靜態分析在業界叫 SAST。看程式碼，對上已知會出問題的寫法，工具放了很多年。Gregor 理解現在前沿模型找得到的是另一類：複雜的邏輯漏洞、IDOR（insecure direct object reference）、串起來的漏洞，以及整條應用流程寫得不安全。前兩類尤其是以前很難抓的。

Alon 說，看懂程式、看懂這類問題，能力跳了一大步。有些問題，他真的覺得以前沒有任何技術找得到。SAST 這個縮寫不新，產品存在很多年，Wiz 內部也做過一套。目標是在程式裡找洞，偏應用層。大家熟悉的簡單例子是 SQL injection：使用者丟進來的輸入處理得不安全，可能一路變成 SQL injection。

這件事以前是學術上的硬問題：怎麼讓機器看懂語言。領頭的公司多半靠語言處理，試著看懂程式怎麼流，建出一張流程圖，也就是 CFG，弄懂程式的走向。以工程來說，極難。現在的模型、LLM，文字看得懂。程式也是有結構、有規則的文字。他說從十二月起，模型看懂程式的能力跳得很大。寫程式變順，找這類漏洞也變順。

漏洞不是同一種。記憶體漏洞是一類，找的是記憶體洩漏，或能被利用、把程式碼塞進那個 process 的記憶體的問題。應用層是另一類。Wiz 這裡是兩條線。一隊在做很深的漏洞引擎，專看記憶體漏洞。另一個比較像 AI SAST 的 agent，會進產品，找的是程式裡的洞，SQL injection，還有前面講的 IDOR。後者比較像做 code review，只是從資安的角度看：你到底讀不讀得懂這段程式。機會在於，AI 現在真的讀得懂。難還是難。

一家公司常常很多個程式庫，你得把跨庫的參照都找出來。LLM 要的是完整的 context，得看懂整個系統。他們看過有幾百個不同 repo 的組織，專案散在不同環境裡，你得把那條線索接起來。他也提到有些產品非常大，得先把東西寫下來。他們的做法是把不同工作交給不同 agent。比照的是人以前手動找洞的老方法：先找各種線索，再蒐集哪裡引用到這個問題，然後真的試著打，再測、再驗證，甚至再做一次判斷。

有時不同模型一起上。Claude 有 Claude 的長處，Gemini 有 Gemini 的，GPT 又有另一種。一個模型卡住、找不到，就叫另一個來幫。像不同研究員各有擅長。目標是收成一個找得到洞的系統。

還得壓誤報，並且看懂這則問題到底有多嚴重。他看到 LLM 的一個毛病：一找到東西，常常就標成非常嚴重。它說嚴重，不一定嚴重。這跟訓練有關。他們得自己判斷嚴重程度，避免誤報。

還有一件事。不必是 Mythos 或 Fable 那一級。Mythos 很強。以參數數量來說，它是非常大的模型，跟其他模型差了一整個數量級。可是模型外面那層 harness，也就是把多個 agent 分成不同工作、串在同一條找洞流程上的做法，若做得好，結果可以接近在 Mythos 上看到的。找漏洞不能只看模型。今天還不在 Mythos、Fable 那一級的前沿模型，配上好的 harness，一樣做得很好。

同一題跑兩次，答案可以不一樣

Gregor 拿一般的 SaaS 產品對照。那種找到的問題，重現步驟通常寫得很清楚。AI 找到的，往往告訴你找到什麼、影響可能是什麼。要另一個人照著重做，就比較難。

Alon 說，錄音前一通會議剛在談這個。今天要做一個好的 AI 系統，不管哪一種，都得做 eval、評測和 benchmark，弄懂自己哪裡做得好。系統一改，以前看過的過程還重不重現得出來。LLM 有隨機的成分，底子是機率。他們的目標是盡量讓它每次結果一樣。誠實的答案是，還沒到。

harness 要做的，就是在這個機率的底子上，仍讓它能穩定重跑。賣產品的人很難賣一個每次答案不同的東西。他看到的是，大家對這種隨機比以前容忍。四年前，沒有人接受。現在人開始習慣 AI 系統給出不同答案。資安這邊的容忍度比過去高一點。可是資安還是會碰到：不同次執行，結果不同。

他們的引擎會把同一則問題重現很多次。有些漏洞本身也是機率的。記憶體漏洞跑 exploit，平均十次裡大概只有一次成功。兩層都是機率，疊在一起更難跑。前沿實驗室也在花很大力氣，讓模型的結果更穩、更能重複。

Gregor 覺得大家願意忍，是因為換來一批以前完全找不到的東西。要是系統必須每一次都一樣，這些就不會出現。要篩的池子變大。可是裡面有些是嚴重到很離譜的問題，SAST 放了很多年都沒抓到。

多挖出來的洞，多半還打不進去

Gregor 喜歡那篇文章的框架。AI 攻擊方拿得到，防守方也拿得到，而且防守方看起來比較有利。他看利用比例。已公開的 CVE 裡，確認在野外被利用的比例，對上 CVE 的量，其實在掉。2026 年是 0.25%，2021 年是 2.2%。他覺得這跟 Alon 比較樂觀的判斷對得上。AI 人人用得到，情況反而像在變好。

Alon 接的是另一個事實。這集錄完之前，利用時間可能還會再短。可是找到漏洞，不表示就容易利用，也不表示找得到 exploit。他們用 AI 找到的漏洞，多數其實打不進去。模型再好，也許以後打得比較動。找到，不等於攻擊方就能拿它做壞事。

他預期短期內會挖出愈來愈多漏洞，其中多數不能被利用。曲線上某個點，多數開源軟體會被掃過。只要模型這邊沒有再跳一大級，這些問題多數會被修掉。他看明年的資安團隊，會很辛苦地補系統、修漏洞，要補的 CVE 會很多。再往後，公開出來的漏洞數量會開始下降，因為該找到的大多找到了。架構也會改，被利用的機會變低。

這集之後，他們還準備再寫一篇，講用 AI 找漏洞。Alon 帶的團隊平常就被鼓勵把看到的寫出來，文章，或甚至一張圖。他覺得資安有一點不一樣，把看到的分享出去，會影響到別人。他們接觸得到世界各地的資安團隊。

有人把今年叫 vulnerability apocalypse，漏洞末日，也有別的名字。再過一兩年，等這段過去，他覺得可以好過一點。前提是社群現在就一起修，並且比攻擊方先找到。長期可以變成一個更安全的世界，攻擊方很快，防守方更快。

審 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 之後，這三條還在。