在之前的文章中，我們討論了零知識(shí)證明的先進(jìn)形式化驗(yàn)證：如何驗(yàn)證一條 ZK 指令。通過形式化驗(yàn)證每條 zkWasm 指令，我們能夠完全驗(yàn)證整個(gè) zkWasm 電路的技術(shù)安全性和正確性。在本文中，我們將關(guān)注發(fā)現(xiàn)漏洞的視角，分析在審計(jì)和驗(yàn)證過程中發(fā)現(xiàn)的具體漏洞，以及從中得到的經(jīng)驗(yàn)和教訓(xùn)。如要了解有關(guān)零知識(shí)證明（ZKP）區(qū)塊鏈的先進(jìn)形式化驗(yàn)證的一般討論，請(qǐng)參見零知識(shí)證明區(qū)塊鏈的先進(jìn)形式化驗(yàn)證一文。

在討論 ZK 漏洞之前，讓我們先來了解 CertiK 是如何進(jìn)行 ZK 形式化驗(yàn)證的。對(duì)于像 ZK 虛擬機(jī)（zkVM）這樣的復(fù)雜系統(tǒng)，形式化驗(yàn)證（FV）的第一步是明確需要驗(yàn)證的內(nèi)容及其性質(zhì)。這需要對(duì) ZK 系統(tǒng)的設(shè)計(jì)、代碼實(shí)現(xiàn)和測(cè)試設(shè)置進(jìn)行全面的審查。這個(gè)過程與常規(guī)的審計(jì)有所重合，但不同之處在于，審查后需要確立驗(yàn)證的目標(biāo)和性質(zhì)。在 CertiK，我們稱其為面向驗(yàn)證的審計(jì)。審計(jì)和驗(yàn)證工作通常是一個(gè)整體。對(duì)于 zkWasm，我們對(duì)其同時(shí)進(jìn)行了審計(jì)和形式化驗(yàn)證。

什么是 ZK 漏洞?

零知識(shí)證明系統(tǒng)的核心特征在于允許將離線或私密執(zhí)行的計(jì)算（例如區(qū)塊鏈交易）的簡短加密證明傳遞給零知識(shí)證明驗(yàn)證器，并由其檢查和確認(rèn)，以確信該計(jì)算確已按聲明的情況發(fā)生過。就此而言，ZK 漏洞將使得黑客可以提交用于證明虛假交易的偽造 ZK 證明，并讓 ZK 證明檢查器接受。

對(duì)于 zkVM 的證明器而言，ZK 證明過程涉及運(yùn)行程序、生成每一步的執(zhí)行記錄，并把執(zhí)行記錄的數(shù)據(jù)轉(zhuǎn)換成一組數(shù)字表格（該過程稱為「算術(shù)化」）。這些數(shù)字之間必須滿足一組約束（即「電路」），其中包括了具體表單元格之間的聯(lián)系方程、固定的常數(shù)、表間的數(shù)據(jù)庫查找約束，以及每對(duì)相鄰表行間所需要滿足的多項(xiàng)式方程（亦即「門」）。鏈上驗(yàn)證可以由此確認(rèn)的確存在某張能滿足所有約束的表，同時(shí)又保證不會(huì)看到表中的具體數(shù)字。

zkWasm 算術(shù)化表

每一個(gè)約束的準(zhǔn)確性都至關(guān)重要。任何約束中的一個(gè)錯(cuò)誤，無論是偏弱或是缺失，都可能使得黑客能夠提交一個(gè)誤導(dǎo)性的證明，這些表格看似代表了智能合約的一次有效運(yùn)行，但實(shí)際并非如此。與傳統(tǒng) VM 相比，zkVM 交易的不透明性放大了這些漏洞。在非 ZK 鏈中，交易的計(jì)算細(xì)節(jié)是公開記錄在區(qū)塊之上的；而 zkVM 則不將這些細(xì)節(jié)存儲(chǔ)于鏈上。透明度的缺失使得攻擊的具體情況很難被確定，甚至連攻擊是否已發(fā)生都很難確定。

執(zhí)行 zkVM 指令規(guī)則的 ZK 電路極其復(fù)雜。對(duì)于 zkWasm 來說，其 ZK 電路的實(shí)現(xiàn)涉及超過 6,000 行的 Rust 代碼和數(shù)百個(gè)約束。這種復(fù)雜性通常意味著可能存在多個(gè)漏洞正等待著被發(fā)現(xiàn)。

zkWasm 電路架構(gòu)

的確，我們通過對(duì)于 zkWasm 審計(jì)和形式化驗(yàn)證發(fā)現(xiàn)了多個(gè)這樣的漏洞。下面，我們將討論兩個(gè)具有代表性的例子，并討論它們之間的差異。

代碼漏洞：Load8 數(shù)據(jù)注入攻擊

第一個(gè)漏洞涉及 zkWasm 的 Load8 指令。在 zkWasm 中，堆內(nèi)存的讀取是通過一組 LoadN 指令來完成的，其中 N 是要加載的數(shù)據(jù)的大小。例如，Load64 應(yīng)該從 zkWasm 內(nèi)存地址讀出 64 位的數(shù)據(jù)。Load8 應(yīng)該從內(nèi)存中讀出 8 位的數(shù)據(jù)（即一個(gè)字節(jié)），并用 0 前綴填充以創(chuàng)建一個(gè) 64 位的值。zkWasm 內(nèi)部將內(nèi)存表示為 64 位字節(jié)的數(shù)組，因此其需要「選取」內(nèi)存數(shù)組的一部分。為此使用了四個(gè)中間變量（u16_cells），這些變量合起來構(gòu)成了完整的 64 位加載值。

這些 LoadN 指令的約束定義如下：

這個(gè)約束分為 Load32、Load16 和 Load8 這三種情況。Load64 沒有任何約束，因?yàn)閮?nèi)存單元正好就是 64 位的。對(duì)于 Load32 的情況，代碼確保了內(nèi)存單元中的高 4 個(gè)字節(jié)（32 位）必須為零。

對(duì)于 Load16 的情況，內(nèi)存單元中的高 6 個(gè)字節(jié)（48 位）必須為零。

對(duì)于 Load8 的情況，應(yīng)該要求內(nèi)存單元中的高 7 個(gè)字節(jié)（56 位）為零。遺憾的是，在代碼中并非如此。

正如你所見，只有高 9 至 16 位被限制為零。其他的高 48 位可以是任意值，卻仍然可以偽裝成「從內(nèi)存中讀取的」。

通過利用這個(gè)漏洞，黑客可以篡改一個(gè)合法執(zhí)行序列的 ZK 證明，使得 Load8 指令的運(yùn)行加載這些意外的字節(jié)，從而導(dǎo)致數(shù)據(jù)損壞。并且，通過精心安排周邊的代碼和數(shù)據(jù)，可能會(huì)觸發(fā)虛假的運(yùn)行和轉(zhuǎn)賬，從而竊取數(shù)據(jù)和資產(chǎn)。這種偽造的交易可以通過 zkWasm 檢查器的檢查，并被區(qū)塊鏈錯(cuò)誤地認(rèn)定為真實(shí)交易。

修復(fù)這個(gè)漏洞實(shí)際上相當(dāng)簡單。

該漏洞代表了一類被稱為「代碼漏洞」的 ZK 漏洞，因?yàn)樗鼈冊(cè)从诖a的編寫，并可以通過較小的局部代碼修改來輕松修復(fù)。正如你可能會(huì)同意的那樣，這些漏洞也相對(duì)更容易被人看出來。

設(shè)計(jì)漏洞：偽造返回攻擊

讓我們來看看另一個(gè)漏洞，這次是關(guān)于 zkWasm 的調(diào)用和返回。調(diào)用和返回是基本的 VM 指令，它們?cè)试S一個(gè)運(yùn)行的上下文（例如函數(shù)）去調(diào)用另一個(gè)，并在被調(diào)用者完成其執(zhí)行后，恢復(fù)調(diào)用者上下文的執(zhí)行。每次調(diào)用都預(yù)期稍后會(huì)返回一次。zkWasm 在調(diào)用和返回的生命周期中所追蹤的動(dòng)態(tài)數(shù)據(jù)被稱為「調(diào)用幀（call frame）」。由于 zkWasm 按順序執(zhí)行指令，所有調(diào)用幀可以根據(jù)其在運(yùn)行過程中的發(fā)生時(shí)間進(jìn)行排序。下面是一個(gè)在 zkWasm 上運(yùn)行的調(diào)用 / 返回代碼示例。

用戶可以調(diào)用 buy_token() 函數(shù)來購買代幣（可能是通過支付或轉(zhuǎn)移其他有價(jià)值的東西）。它的核心步驟之一是通過調(diào)用 add_token() 函數(shù)，實(shí)際將代幣賬戶余額增加 1。由于 ZK 證明器本身并不支持調(diào)用幀數(shù)據(jù)結(jié)構(gòu)，因此需要使用執(zhí)行表（E-Table）和跳轉(zhuǎn)表（J-Table）來記錄和追蹤這些調(diào)用幀的完整歷史記錄。

上圖說明了 buy_token() 調(diào)用 add_token() 的運(yùn)行過程，以及從 add_token() 返回到 buy_token() 的過程?？梢钥吹?，代幣賬戶余額增加了 1。在執(zhí)行表中，每個(gè)運(yùn)行步驟占一行，其中包括當(dāng)前執(zhí)行中的調(diào)用幀編號(hào)、當(dāng)前上下文函數(shù)名稱（僅用于此處的說明）、該函數(shù)內(nèi)當(dāng)前運(yùn)行指令的編號(hào)，以及表中所存的當(dāng)前指令（僅用于此處的說明）。在跳轉(zhuǎn)表中，每個(gè)調(diào)用幀占一行，表中存有其調(diào)用者幀的編號(hào)、調(diào)用者函數(shù)上下文名稱（僅用于此處的說明）、調(diào)用者幀的下一條指令位置（以便該幀可以返回）。在這兩個(gè)表中，都有一個(gè) jops 列，它追蹤當(dāng)前指令是否為調(diào)用 / 返回（在執(zhí)行表）以及該幀（在跳轉(zhuǎn)表）發(fā)生的調(diào)用 / 返回指令總數(shù)。

正如人們所預(yù)期的，每次調(diào)用都應(yīng)該有一次相應(yīng)的返回，并且每一幀應(yīng)該只有一次調(diào)用和一次返回。如上圖所示，跳轉(zhuǎn)表中第 1 幀的 jops 值為 2，與執(zhí)行表中的第 1 行和第 3 行相對(duì)應(yīng)，那里的 jops 值為 1。目前看起來一切正常。

但實(shí)際上這里有一個(gè)問題：盡管一次調(diào)用和一次返回將使幀的 jops 計(jì)數(shù)為 2，但兩次調(diào)用或者兩次返回也會(huì)使計(jì)數(shù)為 2。每幀有兩次調(diào)用或兩次返回聽起來可能很荒謬，但要牢記的是，這正是黑客試圖通過打破預(yù)期要做的事情。

你現(xiàn)在可能有點(diǎn)興奮了，但我們真的找到問題了嗎？

結(jié)果表明，兩次調(diào)用并不是問題，因?yàn)閳?zhí)行表和調(diào)用表的約束使得兩個(gè)調(diào)用無法被編碼到同一幀的行中，因?yàn)槊看握{(diào)用都會(huì)產(chǎn)生一個(gè)新的幀編號(hào)，即當(dāng)前調(diào)用幀編號(hào)加 1。

而兩次返回的情況就沒那么幸運(yùn)了：由于在返回時(shí)不會(huì)創(chuàng)建新的幀，黑客確實(shí)有可能獲取合法運(yùn)行序列的執(zhí)行表和調(diào)用表，并注入偽造的返回（以及相應(yīng)的幀）。例如，先前執(zhí)行表和調(diào)用表中 buy_token() 調(diào)用 add_token() 的例子可以被黑客篡改為以下情況：

黑客在執(zhí)行表中原來的調(diào)用和返回之間注入了兩次偽造的返回，并在調(diào)用表中增加了一個(gè)新的偽造的幀行（原來的返回和后續(xù)指令的運(yùn)行步驟編號(hào)在執(zhí)行表中則需要加 4）。由于調(diào)用表中每一行的 jops 計(jì)數(shù)均為 2，因此滿足了約束條件，zkWasm 證明檢查器將接受這個(gè)偽造的執(zhí)行序列的「證明」。從圖中可以看出，代幣賬戶余額增加了 3 次而不是 1 次。因此，黑客能夠以支付 1 個(gè)代幣的價(jià)格獲得 3 個(gè)代幣。

解決這個(gè)問題有多種方法。一個(gè)明顯的方法就是分別單獨(dú)追蹤調(diào)用和返回，并確保每一幀恰好有一次調(diào)用和一次返回。

你可能已經(jīng)注意到，到目前為止我們尚未展示這個(gè)漏洞的哪怕一行代碼。主流的原因是沒有任何一行代碼是有問題的，代碼實(shí)現(xiàn)完全符合表格和約束設(shè)計(jì)。問題在于設(shè)計(jì)本身，而修復(fù)方法也是如此。

你可能認(rèn)為，這個(gè)漏洞應(yīng)該是顯而易見的，但實(shí)際上并非如此。這是因?yàn)椤竷纱握{(diào)用或兩次返回也會(huì)導(dǎo)致 jops 計(jì)數(shù)為 2」與「實(shí)際上兩次返回是可能的」之間存在空白。后者需要對(duì)執(zhí)行表和調(diào)用表中相關(guān)的各種約束進(jìn)行詳細(xì)、完整地分析，很難進(jìn)行完整的非形式化推理。

兩個(gè)漏洞的比較

對(duì)于「Load8 數(shù)據(jù)注入漏洞」和「偽造返回漏洞」，它們都可能導(dǎo)致黑客能夠操縱 ZK 證明、創(chuàng)建虛假交易、騙過證明檢查器，并進(jìn)行竊取或劫持。 但他們的性質(zhì)和被發(fā)現(xiàn)的方式卻截然不同。

「Load8 數(shù)據(jù)注入漏洞」是在對(duì) zkWasm 進(jìn)行審計(jì)時(shí)發(fā)現(xiàn)的。這絕非易事，因?yàn)槲覀儽仨殞彶槌^ 6,000 行的 Rust 代碼和上百條 zkWasm 指令的數(shù)百個(gè)約束。盡管如此，這個(gè)漏洞還是相對(duì)容易發(fā)現(xiàn)和確認(rèn)的。由于這個(gè)漏洞在形式化驗(yàn)證開始之前就已被修復(fù)，所以在驗(yàn)證過程中并未遇到它。如果在審計(jì)過程中未發(fā)現(xiàn)該漏洞，我們可以預(yù)期在對(duì) Load8 指令的驗(yàn)證中會(huì)發(fā)現(xiàn)它。

「偽造返回漏洞」是在審計(jì)之后的形式化驗(yàn)證中發(fā)現(xiàn)的。我們?cè)趯徲?jì)中未能發(fā)現(xiàn)它的部分原因在于，zkWasm 中有一個(gè)同 jops 非常相似的機(jī)制叫做「mops」，其在 zkWasm 運(yùn)行期間追蹤每個(gè)內(nèi)存單元?dú)v史數(shù)據(jù)對(duì)應(yīng)的內(nèi)存訪問指令。mops 的計(jì)數(shù)約束確實(shí)是正確的，因?yàn)槠渲蛔粉櫫艘环N類型的內(nèi)存指令，即內(nèi)存寫入；而且每個(gè)內(nèi)存單元的歷史數(shù)據(jù)都是不可變的，并只會(huì)寫入一次（mops 計(jì)數(shù)為 1）。但即使我們?cè)趯徲?jì)期間注意到了這個(gè)潛在的漏洞，如果不對(duì)所有的相關(guān)約束進(jìn)行嚴(yán)格的形式化推理，我們將仍然無法輕易地確認(rèn)或排除每一種可能情況，因?yàn)閷?shí)際上沒有任何一行代碼是錯(cuò)誤的。

總結(jié)來說，這兩種漏洞分別屬于「代碼漏洞」和「設(shè)計(jì)漏洞」。代碼漏洞相對(duì)較為淺顯，更容易被發(fā)現(xiàn)（錯(cuò)誤代碼），并且更容易推理和確認(rèn)；設(shè)計(jì)漏洞可能非常隱蔽，更難以發(fā)現(xiàn)（沒有「錯(cuò)誤」代碼），更難以推理和確認(rèn)。

發(fā)現(xiàn) ZK 漏洞的最佳實(shí)踐

根據(jù)我們?cè)趯徲?jì)和形式化驗(yàn)證 zkVM 以及其他 ZK 及非 ZK 鏈的經(jīng)驗(yàn)，下面是關(guān)于如何最好地保護(hù) ZK 系統(tǒng)的一些建議。

檢查代碼以及設(shè)計(jì)

如前所述，ZK 的代碼和設(shè)計(jì)中都可能存在漏洞。這兩種類型的漏洞都可能導(dǎo)致 ZK 系統(tǒng)受到破壞，因此必須在系統(tǒng)投入運(yùn)行之前消除它們。與非 ZK 系統(tǒng)相比，ZK 系統(tǒng)的一個(gè)問題是，任何攻擊都更難揭露和分析，因?yàn)槠溆?jì)算細(xì)節(jié)沒有公開或保留在鏈上。因此人們可能知道發(fā)生了黑客攻擊，但卻無法知道技術(shù)層面上是如何發(fā)生的。這使得任何 ZK 漏洞的成本都非常高。相應(yīng)地，預(yù)先確保 ZK 系統(tǒng)安全性的價(jià)值也非常高。

進(jìn)行審計(jì)以及形式化驗(yàn)證

我們?cè)谶@里介紹的兩個(gè)漏洞分別是通過審計(jì)和形式化驗(yàn)證發(fā)現(xiàn)的。有人可能會(huì)認(rèn)為，使用了形式化驗(yàn)證就不需要審計(jì)了，因?yàn)樗械穆┒炊紩?huì)被形式化驗(yàn)證發(fā)現(xiàn)。實(shí)際上我們的建議是兩者都要進(jìn)行。正如本文開頭所解釋的，一個(gè)高質(zhì)量的形式化驗(yàn)證工作始于對(duì)代碼和設(shè)計(jì)的徹底審查、檢查和非正式推理；而這項(xiàng)工作本身就與審計(jì)重疊。此外，在審計(jì)期間發(fā)現(xiàn)并排除更簡單的漏洞，將使形式化驗(yàn)證變得更加簡單和高效。

如果要對(duì)一個(gè) ZK 系統(tǒng)既進(jìn)行審計(jì)又進(jìn)行形式化驗(yàn)證，那么最佳時(shí)機(jī)是同時(shí)進(jìn)行這兩項(xiàng)工作，以便審計(jì)師和形式化驗(yàn)證工程師能夠高效地協(xié)作（有可能會(huì)發(fā)現(xiàn)更多的漏洞，因?yàn)樾问交?yàn)證的對(duì)象和目標(biāo)需要高質(zhì)量的審計(jì)輸入）。

如果你的 ZK 項(xiàng)目已經(jīng)進(jìn)行了審計(jì)（贊）或多次審計(jì)（大贊），我們的建議是在此前審計(jì)結(jié)果的基礎(chǔ)上對(duì)電路進(jìn)行形式化驗(yàn)證。我們?cè)?zkVM 以及其他 ZK 和非 ZK 項(xiàng)目的審計(jì)和形式化驗(yàn)證的經(jīng)驗(yàn)一再表明，驗(yàn)證常常能捕捉到審計(jì)中遺漏而不易發(fā)現(xiàn)的漏洞。由于 ZKP 的特性，雖然 ZK 系統(tǒng)應(yīng)該提供比非 ZK 解決方案更好的區(qū)塊鏈安全性和可擴(kuò)展性，但其自身的安全性和正確性的關(guān)鍵程度要遠(yuǎn)高于傳統(tǒng)的非 ZK 系統(tǒng)。因此，對(duì) ZK 系統(tǒng)進(jìn)行高質(zhì)量形式化驗(yàn)證的價(jià)值也遠(yuǎn)高于非 ZK 系統(tǒng)。

確保電路以及智能合約的安全

ZK 應(yīng)用通常包含電路和智能合約兩個(gè)部分。對(duì)于基于 zkVM 的應(yīng)用，有通用的 zkVM 電路和智能合約應(yīng)用。對(duì)于非基于 zkVM 的應(yīng)用，有應(yīng)用特定的 ZK 電路及相應(yīng)部署在 L1 鏈或橋的另一端的智能合約?；?zkVM 非基于 zkVM

我們對(duì) zkWasm 的審計(jì)和形式驗(yàn)證工作只涉及了 zkWasm 電路。從 ZK 應(yīng)用的整體安全性角度來看，對(duì)其智能合約進(jìn)行審計(jì)和形式化驗(yàn)證也非常重要。畢竟，在為了確保電路安全方面投入了大量精力之后，如果在智能合約方面放松警惕，導(dǎo)致應(yīng)用最終受到損害，那將是非常遺憾的。

有兩種類型的智能合約值得特別關(guān)注。第一種是直接處理 ZK 證明的智能合約。盡管它們的規(guī)模可能不是很大，但它們的風(fēng)險(xiǎn)非常高。第二種是運(yùn)行在 zkVM 之上的大中型智能合約。我們知道，它們有時(shí)會(huì)非常復(fù)雜，而其中最有價(jià)值的應(yīng)該進(jìn)行審計(jì)和驗(yàn)證，特別是因?yàn)槿藗儫o法在鏈上看到它們的執(zhí)行細(xì)節(jié)。幸運(yùn)的是，經(jīng)過多年的發(fā)展，智能合約的形式化驗(yàn)證現(xiàn)在已經(jīng)可以實(shí)用，并且為合適的高價(jià)值目標(biāo)做好了準(zhǔn)備。

讓我們通過以下的說明來總結(jié)形式化驗(yàn)證（FV）對(duì) ZK 系統(tǒng)及其組件的影響。

• FV 電路 + 非 FV 智能合約 = 非 FV 零知識(shí)證明
• 非 FV 電路 + FV 智能合約 = 非 FV 零知識(shí)證明
• FV 電路 + FV 智能合約 = FV 零知識(shí)證明