當行覆蓋率說謊時

這篇筆記是寫來讀兩遍的。前兩節不假設任何約束系統的先備知識，從頭把機制建立起來。其餘部分是寫給那些建構並審計這些電路的人的，直指確切的程式碼、exploit 的代數，以及一個設計成無法自我逢迎的驗證。

約束系統到底檢查了什麼

一個計算的零知識證明立足於一個想法。驗證者不重跑那份工作，而是檢查一張填好的表格（稱為 trace）是否服從一組固定的代數規則。每一行是計算的一個步驟，每一列是一個暫存器或中間值。形式上 trace 是 $T\in {\mathbb{F}}^{n\times w}$，一個在有限域上、有 $n$ 行 $w$ 列的矩陣。

每條規則都是一個必須求值為零的多項式。一條作用於單一行的規則要求某個多項式 $C$ 在每一行上都消失：

一條把某一步綁到下一步的規則作用於一對相鄰的行，$C({\mathbf{t}}_i,{\mathbf{t}}_{i+1})=0$。證明者送出一條 trace，驗證者檢查每條規則是否都消失。若全都消失，驗證者就確信計算被正確地執行了。

健全性是讓這一切值得信賴的性質。規則必須把 trace 釘死，使得對於給定的公開輸入，除了誠實的那條之外沒有別的有效 trace。當規則太弱時，另一條不同的 trace 也能滿足全部規則，系統就是約束不足的。

一個想作弊的證明者就填入那另一條 trace，每條規則仍然消失，結果是一個對於假命題的有效證明。約束不足不是理論上的顧慮。它是生產級零知識系統中最主要的健全性 bug 類別，而且已經捲走過真金白銀。

這裡要緊的是條件性。大多數規則只在某些時候適用。一條邊界規則只在第一行適用，一條轉移規則在相鄰的行之間適用、但不跨越尾端繞回的接縫，一條指令規則只在某個特定 opcode 旗標被設起的那些行上適用。框架不寫 if。它把規則乘上一個選擇子多項式 $s$，這個多項式在規則該適用之處為一、其餘為零，然後要求乘積消失：

一切都由這條方程式而來。在 $s=1$ 之處這一行必須滿足 $C$。在 $s=0$ 之處，無論 $C$ 是什麼，乘積都是零，所以在那些行上約束什麼都不強制。它是惰性的。

盲點

電路就是程式碼，團隊也像測程式碼那樣測它。慣常的反射動作是行覆蓋率：跑測試，確認約束定義的每一行都執行過，把綠當成安全。

行覆蓋率回答的是一個與健全性所需不同的問題。它問的是那條斷言語句有沒有跑，而它跑了。求值器走過 trace 的每一行並在每一行上呼叫該約束，所以那一行在全部的行上都被覆蓋，連選擇子為零、約束什麼都不強制的那些行也是。語句執行了，而約束卻未受測試。

上方是覆蓋率工具所報告的，百分之百：斷言在全部八行上都跑了。下方那條帶子是實際發生的事，約束只在其中三行上被強制。一個行工具無法把接線正確的守衛和壞掉的守衛分開，因為兩者跑同一行、跑同樣的次數。那個綠色勾把執行量測出來，卻報告成安全。

這不是罕見的角落。條件式約束是這些系統裡的預設形狀，也就是幾乎全部的約束。

這道縫隙藏起來的 bug

有一族 bug 就住在這道縫隙裡，而且陳述起來很簡單：一條正確的約束被接到了錯誤的選擇子上。它會跑、會顯示綠、卻沒能約束那些要緊的行。

拿一個累加器來說。反覆平方求冪建構出一個滾動的值，每一步都把前一步平方，並乘進一個依賴於位元的因子：

其中最後一行上的值 $a_{n-1}$ 就是所宣稱的結果 $r$。這條遞迴關係必須在第一行之後的每一行上成立，因為第零行沒有前驅。若守衛正確，用一個除第一行外處處為一的選擇子，它就在第 $1$ 到第 $n-1$ 行上被強制並抵達最後一行，於是結果被綁到了計算上。

若用錯誤的選擇子來守衛，一個在最後一行而非第一行為零的選擇子，它就在第 $0$ 到第 $n-2$ 行上被強制、卻從不碰到輸出行。一條誠實的 trace 看起來沒問題，因為誠實的 trace 反正處處都滿足遞迴關係。結果如今是自由的。

一個證明者把 $a_{n-1}$ 設成任何選定的值，每一條被強制的行仍然成立，那條把輸出列綁到公開宣稱的邊界規則依構造被滿足，於是驗證者接受了一個假指數的證明。這是一個來自某生產級零知識虛擬機公開審計的真實發現，而整個缺陷就是一個錯誤的選擇子。

一個衡量強制、而非執行的指標

這篇筆記的其餘部分是給那些在這些系統上工作的人的。

修法不是一個更好的行覆蓋率工具，而是一種不同的量測。對每一個約束位點，在一條有效 trace 上，記錄守衛實際上在哪裡是作用的，而不是那條語句有沒有跑。把這份記錄稱為它的啟動剖面：

struct ConstraintCov {
    active_rows: usize,             // 守衛非零
    inactive_rows: usize,          // 守衛為零
    min_active_row: Option<usize>, // 抵達的第一行
    max_active_row: Option<usize>, // 抵達的最後一行
    // ... 外加 active_zero / active_nonzero
}

有一個設計點事先並不明顯。一個布林值，「這條約束曾經作用過嗎」，抓不到真正的 bug。在上面的累加器裡，壞掉的守衛在八行中的七行上作用，而正確的守衛也在八行中的七行上作用，所以兩者都報告「曾經作用」。訊號不在於有多少行，而在於是哪些行：正確的守衛抵達最後一行，壞掉的沒有。啟動剖面帶著這個區別，而布林值把它丟掉了。

這份儀器化很小，而這正是重點。在一個 Plonky3 風格的 builder 裡，守衛的乘法恰好活在一個地方，也就是那個把條件摺進斷言的過濾式 builder：

// FilteredAirBuilder::assert_zero
fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
    self.inner.assert_zero(self.condition() * x.into());
}

整個系統裡的每一條受守衛的約束都會經過那一次乘法。所以在那裡放一個 hook、由具體 trace 的求值器餵入，就能看見它們全部：

fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
    // 在守衛被摺進該項之前先回報它。乘法之後，
    // 守衛與被約束的表達式就無從區分了。
    self.inner.aircov_note_guard(&self.condition);
    self.inner.assert_zero(self.condition() * x.into());
}

那個 recorder 被一個 feature flag 擋著，除非有一個工作階段開啟，否則保持惰性，所以一般的 build 什麼都不用付出。這個指標是從一條有效 trace 讀出來的：把約束跑過求值器，輸出的不是通過或失敗，而是每個守衛在其上為活的那組行。

這個 exploit，攤在啟動剖面上

累加器的 bug 如今在任何人跑 exploit 之前就看得見了。切換下面的守衛，並盯著最後一行，也就是承載結果的那一行。

在正確的守衛之下，遞迴關係抵達輸出行，於是錯誤的結果無法通過。壞掉的守衛讓輸出行不受約束，而那正是偽造所利用的自由。兩個剖面，一個不同的選擇子，相同的程式碼、相同的被執行的行。出貨的那個 bug 長這樣：

// 強制累加的遞迴關係。
builder
    .when(local.is_real)
    .when_not(local.is_last)   // 出貨的守衛；修正是 is_first
    .assert_eq(local.accum, local.prev_accum_squared_times_multiplier);

那條斷言的行覆蓋率在任何誠實的測試下都是百分之百，因為斷言在每一行上都跑。啟動剖面是唯一一個能在一條有效 trace 上把它與正確版本分開的廉價訊號，而不需要任何人先想到那個偽造。

一個建成無法自我逢迎的驗證

有一個明顯的反對意見。那些行位置欄位是在盯著一個行守衛 bug 時加上的，所以拿同一個 bug 來驗證這個指標什麼都證明不了，因為一個指標總會抓到它被塑造來對付的那個情形。

為了把預測與擬合分開，這個指標被以書面凍結，而預測被事先登記。判準在任何保留的 bug 被造出來之前就固定了：當那個凍結的、逐位點的剖面在一條有效 trace 上計算，在正確電路與壞掉電路之間至少有一個共有位點不同時，AIRCov 就分辨出一個 bug。接著四個 bug 類別被重建為最小的、手寫的電路，每一個都是對一個有文件記載的模式的忠實重建，而非在野外抓到的 bug，且每一個都被確認為真正可利用，意即有一條偽造的 trace 是壞掉電路接受、正確電路拒絕的。

四個預測全都成立。看錯誤選擇子那一行，它扛著份量。它與這個指標被塑造來對付的那個行守衛 bug 是不同的機制，所以在那裡抓到就是證據，說明這個剖面能推廣到一個它並非為之設計的 bug，而不是它背下了一個情形的證據。那三個沒抓到是事先預測好的，標記出這個方法誠實的邊界。

有一個附帶說明就坐在判準之內。它問的是剖面在正確電路與壞掉電路之間是否不同，而這預設了有一個已知正確的參照可拿來做差異比對。真實的審計沒有這樣的參照。那份缺席正是整個問題所在。在部署中這個指標吐出單一一個剖面，而一位審閱者就這麼獨自地評判它，一條從不抵達輸出行的遞迴關係讀起來就是錯的，沒有任何手足可供比對。那個四中四是在那個更有利的神諭之下量出來的。部署中的訊號是同一枚指紋較弱的讀法，這也是為什麼收尾的框架把它稱作一位審閱者的指紋，而非一則裁決。

凍結指標，先把預測寫下來，然後再重建那些 bug。只有在事後被擬合了才成立的結果，量到的是後見之明。

它抓不到什麼

這條邊界很銳利，而把它坦白說清楚，正是一個值得信賴的指標的重點所在。

AIRCov 抓得到那些啟動剖面在有效 trace 上會不同的守衛與選擇子 bug。有三樣東西仍在觸及範圍之外：

• 缺失的約束。 沒有位點，就沒有東西可量。一個涵蓋既有約束的指標看不見那條不存在的約束。
• 過窄表達式的 bug。 一條該檢查一個字的全部 limb、卻只檢查其中一個的規則，擁有與正確版本相同的位點、相同的守衛、相同的啟動剖面。沒有差異可偵測，因為差異坐落在表達式內部，而非它何時觸發。
• 在有效 trace 上不可見的守衛 bug。 一個誠實資料恰好會滿足的多餘假條件，在有效 trace 上量到的覆蓋率裡不留痕跡。這是任何有效 trace 覆蓋率的極限，AIRCov 也不例外，而非一個更銳利的指標所能補上的缺口。

所以這是一個為單一類別而設的工具，帶著一條被刻畫清楚的邊。它讓一枚指紋浮現，一條從不抵達輸出行的遞迴關係、一條在它的手足所跳過的行上觸發的約束，接著由一位審閱者或一條下游規則去詮釋。它不下達裁決。

在真實的技術棧上，以及這件事的定位

以上沒有一樣是依賴於某個玩具的。這份儀器化跑在生產級的技術棧上。當前的 SP1 透過對已發布的 p3-air crate 的再匯出來對它的 chip 求值，所以同一個一行的 hook，內嵌進那個 crate 並打上 patch，就流經真實的約束 builder。覆蓋率是在一個隨 SP1 出貨的 chip 上、跑過它自己的求值器所蒐集的。這個 exploit 是在一個用 SP1 真實的 trait 與約束 builder 所建、帶著同一個錯誤選擇子類別的 chip 上跑的，儘管不是那些既有的生產 chip 之一，例如算術單元。在那條活的路徑上，這個缺陷同時是可利用的，一條偽造的 trace 以零條失敗的行被接受、對行覆蓋率不可見、在承載它的那條約束上量到百分之百、並在啟動剖面上可見。把有文件記載的模式注入生產 chip 本身，是剩下的工作。

說一句先前的工作。一個針對零知識虛擬機的變形模糊測試器已經能找到健全性與完備性的 bug，已經使用輕量的指令覆蓋率回饋，並把為約束量身打造的覆蓋率點名為未來工作。它既是基準線，也是這個方向值得走下去的獨立證據。這些工作各不相同。那條工作線生成測試並找出 bug，而 AIRCov 衡量的是一套已在手上的測試對於單一 bug 類別是否足夠、邊界已畫定。這裡不主張在這個領域率先做變異測試。所主張的更為狹窄：一個基於行位置啟動剖面的充分性指標，附有預先登記的保留證據，證明它能分辨出一個行覆蓋率看不見的真實 bug 類別。

那些被儀器化的 fork 與上面每一項測試都是公開的，從可行性案例，經過偽造證明的 exploit 與重建的審計發現，直到那個凍結的、預先登記的驗證，所以這裡的數字可以被重跑，而不必憑信心接受。

自己重現

兩個 fork 承載著儀器化與測試。

• Plonky3 fork：那個 recorder、一行的守衛 hook，以及四項測試，可行性、偽造證明的 exploit、重建的審計發現，以及那個凍結的、預先登記的驗證。細節在它的 AIRCOV.md 裡。
• SP1 fork：同一個 hook，跑在生產級技術棧上，透過一份內嵌的 p3-air 副本與 SP1 自己的約束 builder 接線，覆蓋率是在一個真實的 chip 上跑的。細節在它的 AIRCOV.md 裡。