Binius STARKs原理解析及其優化思考

1 引言

STARKs效率低下的一個主要原因是:實際程序中的大多數數值都較小,如for循環中的索引、真假值、計數器等。然而,爲了確保基於Merkle樹證明的安全性,使用Reed-Solomon編碼對數據進行擴展時,許多額外的冗餘值會佔據整個域,即使原始值本身非常小。爲解決該問題,降低域的大小成爲了關鍵策略。

如表1所示,第1代STARKs編碼位寬爲252bit,第2代STARKs編碼位寬爲64bit,第3代STARKs編碼位寬爲32bit,但32bit編碼位寬仍然存在大量的浪費空間。相較而言,二進制域允許直接對位進行操作,編碼緊湊高效而無任意浪費空間,即第4代STARKs。

表 1: STARKs 衍化路徑

| 代數 | 編碼位寬 | 代表系統 | |------|----------|----------| | 第1代 | 252bit | StarkWare |
| 第2代 | 64bit | Plonky2 | | 第3代 | 32bit | BabyBear | | 第4代 | 二進制域 | Binius |

相比於Goldilocks、BabyBear、Mersenne31等近幾年新研究發現的有限域,二進制域的研究可追溯到上個世紀80年代。當前,二進制域已經廣泛應用於密碼學中,典型例子包括:

• 高級加密標準(AES),基於F28域;

• Galois消息認證碼(GMAC),基於F2128域;

• QR碼,使用基於F28的Reed-Solomon編碼;

• 原始FRI和zk-STARK協議,以及進入SHA-3決賽的Grøstl哈希函數,該函數基於F28域,是一種非常適合遞歸的哈希算法。

當採用較小的域時,擴域操作對於確保安全性愈發重要。而Binius所使用的二進制域,需完全依賴擴域來保證其安全性和實際可用性。大多數Prover計算中涉及的多項式無需進入擴域,而只需在基域下操作,從而在小域中實現了高效率。然而,隨機點檢查和FRI計算仍需深入到更大的擴域中,以確保所需的安全性。

基於二進制域來構建證明系統時,存在2個實際問題:STARKs中計算trace表示時,所用域大小應大於多項式的階;STARKs中Merkle tree承諾時,需做Reed-Solomon編碼,所用域大小應大於編碼擴展後的大小。

Binius提出了一種創新的解決方案,分別處理這兩個問題,並通過兩種不同的方式表示相同的數據來實現:首先,使用多變量(具體是多線性)多項式代替單變量多項式,通過其在"超立方體"(hypercubes)上的取值來表示整個計算軌跡;其次,由於超立方體每個維度的長度均爲2,因此無法像STARKs那樣進行標準的Reed-Solomon擴展,但可以將超立方體視爲方形(square),基於該方形進行Reed-Solomon擴展。這種方法在確保安全性的同時,極大提升了編碼效率與計算性能。

2 原理解析

當前大多數SNARKs系統的構建通常包含以下兩部分:

• 信息理論多項式交互預言機證明(Information-Theoretic Polynomial Interactive Oracle Proof, PIOP):PIOP作爲證明系統的核心,將輸入的計算關係轉化爲可以驗證的多項式等式。不同的PIOP協議通過與驗證者的交互,允許證明者逐步發送多項式,使得驗證者通過查詢少量多項式的評估結果即可驗證計算是否正確。現有的PIOP協議包括:PLONK PIOP、Spartan PIOP 和 HyperPlonk PIOP 等,它們各自對多項式表達式的處理方式有所不同,從而影響整個 SNARK 系統的性能與效率。

• 多項式承諾方案(Polynomial Commitment Scheme, PCS):多項式承諾方案用於證明PIOP生成的多項式等式是否成立。PCS是一種密碼學工具,通過它,證明者可以承諾某個多項式並在稍後驗證該多項式的評估結果,同時隱藏多項式的其他信息。常見的多項式承諾方案有KZG、Bulletproofs、FRI(Fast Reed-Solomon IOPP)和Brakedown等。不同的PCS具有不同的性能、安全性和適用場景。

根據具體需求,選擇不同的PIOP和PCS,並結合合適的有限域或橢圓曲線,可以構建具有不同屬性的證明系統。例如:

• Halo2:由 PLONK PIOP 與 Bulletproofs PCS 結合,並基於Pasta曲線。Halo2設計時,注重於可擴展性,以及移除ZCash協議中的trusted setup。

• Plonky2:採用PLONK PIOP與FRI PCS結合,並基於Goldilocks域。Plonky2是爲了實現高效遞歸的。在設計這些系統時,選擇的PIOP和PCS必須與所使用的有限域或橢圓曲線相匹配,以確保系統的正確性、性能和安全性。這些組合的選擇不僅影響SNARK的證明大小和驗證效率,還決定了系統是否能夠在無需可信設置的前提下實現透明性,是否可以支持遞歸證明或聚合證明等擴展功能。

Binius:HyperPlonk PIOP + Brakedown PCS + 二進制域。具體而言,Binius包括五項關鍵技術,以實現其高效性和安全性。首先,基於塔式二進制域(towers of binary fields)的算術化構成了其計算的基礎,能夠在二進制域內實現簡化的運算。其次,Binius在其交互式Oracle證明協議(PIOP)中,改編了HyperPlonk乘積與置換檢查,確保了變量及其置換之間的安全高效的一致性檢查。第三,協議引入了一個新的多線性移位論證,優化了在小域上驗證多線性關係的效率。第四,Binius採用了改進版的Lasso查找論證,爲查找機制提供了靈活性和強大的安全性。最後,協議使用了小域多項式承諾方案(Small-Field PCS),使其能夠在二進制域上實現高效的證明系統,並減少了通常與大域相關的開銷。

2.1 有限域:基於towers of binary fields的算術化

塔式二進制域是實現快速可驗證計算的關鍵,主要歸因於兩個方面:高效計算和高效算術化。二進制域本質上支持高度高效的算術操作,使其成爲對性能要求敏感的密碼學應用的理想選擇。此外,二進制域結構支持簡化的算術化過程,即在二進制域上執行的運算可以以緊湊且易於驗證的代數形式表示。這些特性,加上能夠通過塔結構充分利用其層次化的特性,使得二進制域特別適合於諸如Binius這樣可擴展的證明系統

其中"canonical"是指在二進制域中元素的唯一且直接的表示方式。例如,在最基本的二進制域F2中,任意k位的字符串都可以直接映射到一個k位的二進制域元素。這與素數域不同,素數域無法在給定位數內提供這種規範的表示。盡管32位的素數域可以包含在32位中,但並非每個32位的字符串都能唯一地對應一個域元素,而二進制域則具備這種一對一映射的便利性。在素數域Fp中,常見的歸約方法包括Barrett歸約、Montgomery歸約,以及針對Mersenne-31或Goldilocks-64等特定有限域的特殊歸約方法。在二進制域F2k中,常用的歸約方法包括特殊歸約(如AES中使用)、Montgomery歸約(如POLYVAL中使用)和遞歸歸約(如Tower)。論文《Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations》指出,二進制域在加法和乘法運算中均無需引入進位,且二進制域的平方運算非常高效,因爲它遵循(X + Y )2 = X2 + Y 2 的簡化規則。

如圖1所示,一個128位字符串:該字符串可以在二進制域的上下文中以多種方式進行解釋。它可以被視爲128位二進制域中的一個獨特元素,或者被解析爲兩個64位塔域元素、四個32位塔域元素、16個8位塔域元素,或128個F2域元素。這種表示的靈活性不需要任何計算開銷,只是對位字符串的類型轉換(typecast),是一個非常有趣且有用的屬性。同時,小域元素可以被打包爲更大的域元素而不需要額外的計算開銷。Binius協議利用了這一特性,以提高計算效率。此外,論文《On Efficient Inversion in Tower Fields of Characteristic Two》探討了在n位塔式二進制域中(可分解爲m位子域)進行乘法、平方和求逆運算的計算復雜度。

2.2 PIOP:改編版HyperPlonk Product和PermutationCheck------適用於二進制域

Binius協議中的PIOP設計借鑑了HyperPlonk,採用了一系列核心檢查機制,用於驗證多項式和多變量集合的正確性。這些核心檢查包括:

1. GateCheck:驗證保密見證ω和公開輸入x是否滿足電路運算關係C(x,ω)=0,以確保電路正確運行。

2. PermutationCheck:驗證兩個多變量多項式f和g在布爾超立方體上的求值結果是否爲置換關係f(x) = f(π(x)),以確保多項式變量之間的排列一致性。

3. LookupCheck:驗證多項式的求值是否在給定的查找表中,即f(Bµ) ⊆ T(Bµ),確保某些值在指定範圍內。

4. MultisetCheck:檢查兩個多變量集合是否相等,即{(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H,保證多個集合間的一致性。

5. ProductCheck:檢測有理多項式在布爾超立方體上的求值是否等於某個聲明的值∏x∈Hµ f(x) = s,以確保多項式乘積的正確性。

6. ZeroCheck:驗證一個多變量多項式在布爾超立方體上的任意點是否爲零∏x∈Hµ f(x) = 0,∀x ∈ Bµ,以確保多項式的零點分布。

7. SumCheck:檢測多變量多項式的求和值是否爲聲明的值∑x∈Hµ f(x) = s。通過將多元多項式的求值問題轉化爲單變量多項式求值,降低驗證方的計算復雜度。此外,SumCheck還允許批處理,通過引入隨機數,構造線性組合實現對多個和校驗實例的批處理。

8. BatchCheck:基於SumCheck,驗證多個多變量多項式求值的正確性,以提高協議效率。

盡管Binius與HyperPlonk在協議設計上有許多相似之處,但Binius在以下3個方面做出改進:

• ProductCheck優化:在HyperPlonk中,ProductCheck要求分母U在超立方體上處處非零,且乘積必須等於一個特定值;Binius通過將該值特化爲1,簡化這一檢查過程,從而降低計算復雜度。

• 除零問題的處理:HyperPlonk未能充分處理除零情況,導致無法斷言U在超立方體上的非零問題;Binius正確地處理了這一問題,即使在分母爲零的情況下,Binius的ProductCheck也能繼續處理,允許推廣到任意乘積值。

• 跨列PermutationCheck:HyperPlonk無此功能;Binius支持在多個列之間進行PermutationCheck,這使得Binius能夠處理更復雜的多項式排列情況。

因此,Binius通過對現有PIOPSumCheck機制的改進,提升了協議的靈活性和效率,尤其在處理更復雜的多變量多項式驗證時,提供了更強的功能支持。這些改進不僅解決了HyperPlonk中的局限性,還爲未來基於二進制域的證明系統奠定了基礎。

2.3 PIOP:新的 multilinear shift argument------適用於 boolean hypercube

在Binius協議中,虛