Magnetar 以零知識證明支援通用計算

概覽

• 一種新型計算方式。零知識證明讓你執行工作負載，並在取得結果的同時，獲得一份簡短證明，證明程式已正確執行。任何人都可以在毫秒內驗證證明，無需重新執行程式、信任執行程式的人，亦無需取得程式執行時所用的資料。
• 要廣泛採用，仍有三大挑戰：令證明的產生速度足夠快；讓一般程式無需密碼學專業知識也能使用；以及以數十年後仍值得信賴的密碼學技術作為基礎。
• Magnetar 在這三方面均取得重大進展。它能為以 Rust、Go 或 C 編寫的程式產生證明，平均速度比此前最快的同類系統快 10 至 39 倍，而且其安全性僅建基於標準雜湊函數。這是 Microsoft Research 十多年來致力令零知識證明切實可用的最新成果。

一種新型計算方式

電腦產生的每項結果，背後都有一個隱含問題：程式是否如聲稱般執行，並產生正確的輸出？今天，要回答這個問題，往往除了驗證之外，還需要一定程度的信任。 我們信任操作人員、供應商、交易對手或 Agent，並依靠合約、審計和日誌來建立這種信任。

零知識證明提供了一種截然不同的信任建立方式。程式執行時，會連同輸出一併產生一份簡短證明；這是一種密碼學憑證，證明該程式在這些輸入資料下產生了這項輸出。證明體積小，驗證速度快。接收者無需重新執行程式，只需毫秒便可確認結果，亦可把證明轉交給任何需要同等保證的人。零知識特性亦確保證明不會披露應予保密的輸入資料。

這會改變現實世界中對正確性的理解。結果不再需要因為產生者是誰而獲得信任；只要檢查隨附的內容，便能加以驗證。代表他人行事的 AI Agent，可以附上證明，確認每項行動均符合其獲提供的政策。受監管的金融機構可以證明交易已獲正確處理，而無需公開交易內容。只要產生證明像執行程式一樣常規，這些事情便能實現。

三大挑戰

零知識證明於 1980 年代發明，而證明程式執行的相關理念亦幾乎同樣歷史悠久。阻礙它們成為通用工具的，是三項一直難以同時解決的挑戰。

效率。過去，產生證明所需的運算量曾達程式本身的數百萬倍。多年來的研究已降低這項額外開銷，但最快的系統是透過在其他方面作出妥協來提升速度。

通用性與易用性。 許多證明系統要求開發人員手動將程式改寫為密碼電路，即針對該項運算編寫固定的算術描述。這需要數月時間。應用程式每次改動都意味著要重新編寫電路，而這種轉換本身亦經常引發安全漏洞。另一種通用方案是證明一般處理器的執行過程，讓任何經編譯的程式都能按原樣獲得證明。直到最近，這種通用性仍要付出速度或安全性大幅下降的代價。 

安全性。 證明的強度取決於其底層密碼學。許多證明系統以橢圓曲線為基礎，而足夠強大的量子電腦可以破解橢圓曲線。Microsoft 正透過其 Quantum Safe Program 處理這個問題，計劃將其產品和服務轉用後量子密碼學；Microsoft 最近已將目標提前至 2029 年。後量子證明系統已經問世，但有些以格假設為基礎，而大多數則依賴新發明的密碼學函數，以降低證明成本。這些新密碼學函數未曾經歷保護現今互聯網的密碼學所接受的數十年檢視；部分函數更以尚未證明的糾錯碼數學猜想為基礎。它們以強假設換取速度。 

十多年的研究

十多年來，Microsoft Research 一直致力於讓零知識證明和可驗證運算變得實用。早期研究採用兩種方法，但兩者只適用於小型程式。第一種方法（在新分頁中開啟） （在新分頁中開啟）讓驗證者透過與證明者進行簡短對話，檢查一項長時間運算；這種方法使用稱為sum-check 協定（在新分頁中開啟）的技術，但只適用於具有特定分層結構的運算。第二種方法（在新分頁中開啟） （在新分頁中開啟）使用橢圓曲線密碼學，為幾乎任何運算建立極小的證明。但這需要進行一次性的可信設定，當中涉及秘密資料；若資料外洩，任何人都可能偽造證明。這種方法亦容易受到量子電腦攻擊。

2019 年，一種名為 Spartan 的新零知識證明系統重新採用 sum-check 方法，並使其適用於無需可信設定的通用程式。Spartan 亦可採用不同的密碼學構件來實作。這種靈活性讓該證明系統其後得以僅以雜湊函數為基礎建構。隨後一系列研究成果補足了其餘部分： 

• Phalanx（在新分頁中開啟）於 2021 年展示如何利用重複性——例如處理器在每一步都執行相同的指令週期——以比 Spartan 快一個數量級的速度證明運算。Magnetar 的處理器描述便建基於這個概念。  
• Nova（在新分頁中開啟）、HyperNova（在新分頁中開啟）、NeutronNova（在新分頁中開啟）、Neo 和 SuperNeo（在新分頁中開啟）展示了提早停止 Spartan 的證明流程，再將部分結果折疊在一起，便能以低得多的成本，實際證明任何規模的運算。
• Brakedown（在新分頁開啟）於 2021 年提出一種快速的雜湊式承諾方案，並將其與 Spartan 結合，帶來首個安全性基於標準雜湊函數的 Spartan 變體。 
• Spice（在新分頁開啟）、Lasso（在新分頁開啟）、Nebula（在新分頁開啟），以及其後的 Twist and Shout（在新分頁開啟），令通用處理器核心的記憶體操作能以低成本證明；而 Jolt（在新分頁開啟） 則顯示，將這些技術與 Spartan 結合，便能有效率地證明完整處理器的執行過程。
• 今年稍早，Vega（在新分頁開啟）將這項研究應用於數碼身份，只需不到十分之一秒，便能證明政府憑證中的事實。
• 最近，BinarySpartan（在新分頁開啟）將 Spartan 帶到二元域，處理器邏輯和標準雜湊函數都能在其中有效率地表達。BinarySpartan 亦依賴 Ligerito（在新分頁開啟）——一種採用 Brakedown 類型、證明短得多的承諾方案——以及 環切換（在新分頁開啟），讓對位元向量作出承諾更有效率。 

以上技術各自解決了問題的一部分。Magnetar 將各部分結合起來。

Magnetar

Magnetar 是一種零知識虛擬機（zkVM），並同時在三項挑戰上取得重大進展。

它適用於通用用途。 Magnetar 能證明 RISC-V 的執行過程。RISC-V 是一種開放式處理器架構，主流程式語言均有成熟的編譯器。開發人員以 Rust、Go 或 C 編寫程式，照常編譯，Magnetar 便能證明該程式的執行過程。想想這在實際應用中代表甚麼：商業政策、數據管道，或以太坊虛擬機（EVM）的解譯器，都只是一個程式；負責維護這些程式的工程師，能按原樣證明其執行過程。因此，證明不再是專家的專門工作。 

它比同類的先前系統更快。 Magnetar 在手提電腦上每秒可證明 720 萬至 870 萬條處理器指令。在 15 個基準測試程式中，測試範圍涵蓋加密雜湊至小型 EVM 解譯器內的代幣轉帳；在同一部電腦上，它的平均速度是現有最快 zkVM 的 10 至 39 倍，而在代幣轉帳基準測試中，速度更是另外兩個系統的 300 多倍。經最佳化的 Magnetar 每秒可證明 950 萬至 1,280 萬個週期，令本文報告的各項加速比提高約 1.3×。其證明約需 12 毫秒即可驗證。 

其安全性建基於標準密碼學。Magnetar 採用標準雜湊函數，例如 SHA-256 或 SHA-3；這些正是目前用來保護各機構系統的密碼學基元。它不需要橢圓曲線、格、專用雜湊函數、可信設定，也不依賴任何未經證明的糾錯碼猜想。雜湊函數是密碼學工具箱中經過最深入研究的基元，也是無狀態雜湊式簽章的基礎；NIST 已將這類簽章標準化，作為其保守的後量子選項。對於必須在數十年後仍值得信賴的系統而言，只依賴標準雜湊函數，便可從技術路線圖中免去一次密碼學遷移。 

同一個設計決定還帶來另一項好處。驗證 Magnetar 證明，主要涉及計算標準雜湊函數和二元域算術，而這些正是 Magnetar 能高效產生證明的運算。因此，驗證證明對它而言只是一般的工作負載。這讓 Magnetar 能證明任何規模的計算：先分段證明，再組合各部分。這也讓 Magnetar 能為帳本或區塊鏈等長時間運行的系統提供證明。

技術論文提供完整的設計、安全性分析及測量結果。

展望未來

Magnetar 將零知識證明和可驗證運算推進至一個階段，使它們能以機構已信任的密碼學為基礎，達到實用的速度，並讓編寫一般程式碼的工程師也能使用。Magnetar 讓一個未來成為可能：密碼學證明將成為計算的常規輸出。我們預期，科技領袖將不再問執行證明是否切實可行，而會轉而聚焦於哪些結果 會是 他們寧願驗證、而非直接信任的。

如果你有興趣探索零知識證明如何支援你的應用場景，歡迎與我們聯絡 (在新分頁中開啟)。

在新分頁中開啟

文章以 Magnetar 實現基於證明的通用運算最初刊登於Microsoft Research。