Abstract
SNARK是学界和密码学社区的热点研究方向之一，尽管现有的一些方案已在实践中进行使用，但是只有社区对这些协议的安全性进行了严格的评估，且部分协议中也出现了安全性缺陷的问题
为了提高这些协议的严谨性，本文采用形式化方法，重点分析了一类常用SNARK协议的合理性，包括但不限于Groth16
本文采用Lean证明语言，并采用了各种可能的技术来尽可能地简化和自动化这些证明
Lean可以用机器编写证明的工具，在编写完证明的推导之后，Lean可以自动检查推导过程是否正确
1 Introduction
近年来SNARK在区块链、可验证计算、身份管理方面都有应用，但是安全性是这些技术落地的主要问题之一
Parno和Gabizon的研究发现了开源库libsnark中存在合理性缺陷，为了防止未来再出现此类错误，本文希望以形式化的方式来确保SNARK协议的安全性
本文重点关注基于SRS和配对的SNARK（因为它可以做到$O(1)$的证明大小），包括下列六个协议
- GGPR13：第一个SNARK，基于QAP实现
- Pinocchio：基于GGPR13改进
- Groth16：典中典
- Baghery$[2]$：Groth16的III型配对版本
- Lipmaa：Groth16的变体，改进了模拟可抽取性
- Baby SNARK$[3]$：Groth16的青春版，主要用于教学，旨在提供易于理解的合理性证明
本文采用Lean 3作为形式化工具（具体采用mathlib这个开源库），Lean允许用户通过计算机代码来构建数学命题的形式化证明，本文基于Lean来构建多变量多项式的等式集合的合理性证明
相关工作没看，感兴趣看原文$[1]$
2 Overview of Pairings and the Algebraic Group Model
合理性可以确保恶意的Prover欺骗诚实的Verifier的概率可忽略，说人话就是假的真不了，合理性通常通过定义抽取器来完成，抽取器可以在Prover成功的时候抽取出对应的知识
但是SNARK中存在一些问题，与交互式协议不同，因为交互式协议中Prover从原则上来说，可以以确定性的方式构造证明，非交互协议中抽取器只能看到一个有效的证明，此时抽取器在尝试重构witness的时候其渐进性可能会逐渐增大
为了解决这个问题，本文假设证明的构建与一个更大的随机数据相关，也即SRS串，因此本文的分析也是基于SRS模型中的配对SNARK协议
基于配对的SNARK的SRS包含一系列的ECC群元素，这些元素均来自于由$(p,\mathbb G_1,\mathbb G_2,\mathbb G_T,e)$定义的椭圆曲线群，Prover可以利用椭圆曲线运算来构造基于SRS的线性组合，以生成证明串，之后Verifier通过配对的方式来验证证明
协议的合理性通常基于一个密码学假设，通过密码学假设来限制Prover在构建证明时的能力，以防止其违背协议，目前SNARK通常采用代数群模型（Algebraic Group Model，AGM）中的假设来构建，AGM中的假设要求Prover只能输出SRS中的元素的线性组合，之后抽取器可以通过访问这些线性组合的系数来重构witness
总结一下，基于配对的SNARK在AGM模型中包含下列性质
- （非透明的协议）包含毒物（Toxic Waste）
- SRS为毒物的多项式
- 证明串为SRS的线性组合
- 验证等式为基于SRS和证明串的配对
- 验证通过意味着抽取器可以抽取出witness
3 Lean Formalization of the Soundness Proof
本节介绍一个基于Lean的技术，可以用于验证基于配对的SNARK的合理性，接下来以III型配对的Groth16算法为例
3.1 Stage 0：Multivariate Polynomial Formalization
本文的形式化方法中考虑了证明过程中出现毒物的数据类型
首先回顾一下Groth16算法，其包含五个毒物$\alpha,\beta,\gamma,\delta,x\in \mathbb F^*$，其中前四个元素在SRS中独立出现，后续的SRS元素包含了这五个元素的线性组合，具体如下（详细的Groth16可以参考之前的博客$[4]$）
$$ \begin{aligned} \{x_i\}^{n-1}_{i=0}, \{\frac{\beta u_i(x)+\alpha v_i(x)+w_i(x)}{\gamma}\}^l_{i=0}\\ \{\frac{\beta u_i(x)+\alpha v_i(x)+w_i(x)}{\delta}\}^m_{i=l+1}, \{\frac{x^it(x)}{\delta}\}^{n-2}_{i=0} \end{aligned} $$
这里将Groth16的SRS划分为8个部分（8个SRS组件），以便进行形式化分析，前四个分别为四个随机性$\alpha,\beta,\gamma,\delta$，后四个则是上述这四个集合
其他算法考虑的组件的数量如表2中的第三列所示
回到Groth16，这里可以观察一下Groth16的SRS，可以看到如果不考虑分母的话，后续三个集合都是多变量多项式，Groth16和Sonic之类的方案类似，采用洛朗多项式构建SRS
洛朗多项式（Laurent Poly.）的特点在于其指数可以为负数，且同时具备常规多项式相同的性质，比如SZ引理也适用于洛朗多项式
但是本文使用的mathlib不支持多变量洛朗多项式，不过注意到Groth16实际上没必要采用洛朗多项式来形式化，而是可以采用所有SRS元素乘以一个域元素的最小阶来得到一个等效的SNARK，后续这个方法可以用多变量多项式进行形式化
把这个方法用在Groth16中的话，就是对所有的SRS元素（上述的8个组件）全部乘一个$\gamma \cdot \delta$，可以证明基于洛朗多项式的方案的合理性可归约至非洛朗多项式版本的方案，此时原来的8个组件就变成了下面这样
$$ \begin{aligned} &\alpha \gamma\delta,\beta\gamma\delta,\gamma^2\delta,\gamma\delta^2 \\ &\{\gamma\delta x_i\}^{n-1}_{i=0}, \{\delta\big({\beta u_i(x)+\alpha v_i(x)+w_i(x)}\big)\}^l_{i=0}\\ &\{\gamma\big({\beta u_i(x)+\alpha v_i(x)+w_i(x)}\big)\}^m_{i=l+1}, \{\gamma{x^it(x)}\}^{n-2}_{i=0} \end{aligned} $$
不难看出，四个随机性$\alpha,\beta,\gamma,\delta$的最大阶分别为1，1，2，2，因此实际上SRS的最大阶仅取决于元素$x$，而该元素的阶又取决于电路，因此在后续的形式化证明中，可以利用这一特点，并转变思路：与其将值形式化为$\mathbb F$上的五个变量的多变量多项式，不如将其形式化为多项式上的多变量多项式
论文的原话是：Instead of formalizing there values as multivariable poly. in five variables over $\mathbb F$，we formalize them as multivariable poly. over poly.
3.2 Stage 1: Coefficients of the Equations
证明AGM中的SNARK的合理性要求证明元素具有对应的AGM表示，且需要证明这些表示满足协议指定的验证等式，基于SRS的SNARK中，证明元素由SRS的线性组合表示
前面提到了Groth16中四个随机性$\alpha,\beta,\gamma,\delta$的最大阶分别为1，1，2，2，且Groth16只用一个配对等式来验证，因此输出的项中可能会包含下列几种可能的系数
- $\alpha$：$(1,\alpha,\alpha^2)$
- $\beta$：$(1,\beta,\beta^2)$
- $\gamma$：$(1,\gamma,\gamma^2,\gamma^3,\gamma^4)$
- $\delta$：$(1,\delta,\delta^2,\delta^3,\delta^4)$
共计$3\times 3\times 5\times5=75$种不同的非零系数组合（实际上只有51个是非零的，不知道为啥），之后通过合理构造Lean来隔离这些不同的方程即可，具体如表1所示
没学过Lean和形式化证明，看不懂，感兴趣的话这里指路另一个大佬：Wei Li's blog (hu4i.github.io)
3.3 Stage 2: Mutual Simplification
有了上述表1的过程，接下来是简化这些方程来尽可能实现自动化
如果仔细观察Groth16的验证等式，会发现三个多项式$u,v,w$和其他多项式的加法和乘法出现了很多次，且通常而言SNARK的有效性不太取决于这些多项式，因此有效性的证明也不太需要这些结构，这里将这些多项式视为原子（atoms），并以一种简单的方式处理这些加法和乘法
此外，SNARK基于配对进行验证，通常会出现$A*B=0$这样的验证等式，这意味着$A,B$至少有一个为零，这个点可以用于优化本文的形式化目标，具体而言就是将所有形如$A*B=0$的等式简化为$A=0$或$B=0$的情况，直到这些等式无法再进一步化简为止
这部分具体的看原文的第7页，有几行看不懂的符号和代码
4 Evaluation
表2给出了本文方案推理各类SNARK所需要的时间，这里再粘贴一下那个图
经分析，化简主要占据了推理时间的主要部分，因为这一阶段可能需要指数级别的步骤来完成化简
从表中可以看出，原始版本的Groth16的推理时间高达3.8个小时，比采用III型配对的方案（第四行的Baghery）还要高两个数量级，这是因为原始的Groth16中具有更多的对称性，而采用III型配对的方案对称性更少
本文不失一般性地处理了这些对称性，再加上指数爆炸，所以才导致了Groth16的推理时间比其他的长很多
5 Comments on Proof Exposition
前面都是对Groth16的分析，这里讲一下其他几个方案，但是构建这些方案的形式化证明过程有些问题，部分原因是由于方案的原始论文中存在一定的误导性（甚至是存在错误），为了让ZKP社区更好的理解这些证明，这里做一些简单的解释
5.1 Pinocchio
这里主要关注Pinocchio原文的协议2（基于常规QAP的SNARK）和原文的定理1
回顾一下协议，Prover基于witness构造了三个证明元素
$$ g^{V_{mid}},g^{W_{mid}},g^{Y_{mid}} $$
同时还基于SRS构造了三个用于验证的元素
$$ g^{V'_{mid}},g^{W'_{mid}},g^{Y'_{mid}} $$
最后由Verifier验证三个配对等式
$$ e(g_v^{V'_{mid}},g)=(g_v^{V_{mid}},g^{\alpha_v})\\ e(g_w^{W'_{mid}},g)=(g_w^{W_{mid}},g^{\alpha_w})\\ e(g_y^{Y'_{mid}},g)=(g_y^{Y_{mid}},g^{\alpha_y}) $$
根据Pinocchio的原文，上述三个配对的目的是检查$\mathcal V,\mathcal W,\mathcal Y$中的线性组合是否在正确的跨度（spans）内，也即是否在$v_k(x),w_k(x),y_k(x)$内，但是原文并没有阐明这里的$k$是表明witness中的索引，还是statement中的索引
如果witness和statement多项式不是线性独立的，则AGM敌手可以将这些线性组合添加到证明系数中，从而可以得到一组对应的验证系数，且$\mathcal V,\mathcal W,\mathcal Y$的线性组合与witness不匹配，这个过程实际上并没有改变证明元素，但是会导致更难在本文的模型中进行推理
而且Pinocchio还有一个更明显的问题，验证等式不能确保证明元素在statement和witness所组合的范围内，看上去好像是这么回事，但是Prover可以为Verifier的关键元素构建一个系数非零的证明元素，且这些元素可以通过检查，具体而言，Prover可以对$g^{V_{mid}}$乘一个$g$，对$g^{V'_{mid}}$乘一个$g^\alpha_v$，$g^{W_{mid}},g^{Y_{mid}}$同理，这样一来也可以通过验证
这里的思想和ElGamal的修改密文类似，ElGamal可以在不知道私钥的情况下，对密文分别乘上生成元即可在不改变所加密的明文的情况下构造一个全新的密文
但是这样会导致在推理化简的过程中有一些项无法消掉，且只有在下一次检查中，此类攻击才会被检测到：如果在验证等式中加入第五个配对检查，用以确保$\mathcal V,\mathcal W,\mathcal Y$都使用了相同的系数，则敌手无法构建上述那样的超出协议范围的证明元素
5.2 Groth16
Groth16中的合理性证明对其验证多项式中的某些项的系数关系做出了类似的过度假设
Groth16原文的定理1给出的合理性证明中，首先分析了多项式的$\alpha^2,\alpha\beta,\beta^2$三个系数所对应的项为零，之后不失一般性分析了系数为$1/\delta^2$的项，如下
$$ \sum^m_{i+1}A_i(\beta u_i(x)+\alpha v_i(x)+w_i(x))+t(x)A_h(x)=0 $$
这一项为零，不过Groth16的原文打错了（偷偷瞄了一眼原文，原文写的是$A_t$而不是$A_h$）
然后Groth16分析了下面这项为零
$$ \alpha\frac{\sum^m_{i+1}B_i(\beta u_i(x)+\alpha v_i(x)+w_i(x))+t(x)B_h(x)}{\delta}=0 $$
由于$\alpha$不为零，上式等于0意味着分母的求和式为零
然后Groth16中分析了$\alpha^2,\alpha\beta,\beta^2$三个系数对应的项（把前面的$\alpha$乘到求和式里面），然后系数为$\alpha^2/\delta$的项为零，意味着$\sum^m_{i=l+1}B_iv_i(x)=0$，系数为$\alpha\beta/\delta$的项为零，也即$\sum^m_{i=l+1}B_iu_i(x)=0$，上式的分子就只剩下下面这两项
$$ \sum^m_{i=l+1}B_iw_i(x)+t(x)B_h(x) \tag 1 $$
也即剩下这两项对应于系数为$\alpha/\delta$的项，但是系数为$\alpha/\delta$的项还涉及到一个与$A(x)$相关的项$A(x)\sum^m_{i=l+1}B_i\frac{\alpha v_i(x)}{\delta}$，因此这三个相关系数求和结果不等于0，只等于负的$A(x)\sum^m_{i=l+1}B_i\frac{\alpha v_i(x)}{\delta}$
不过系数为$1/\delta$中有下面这个项
$$ A(x)\cdot \Big(\sum^m_{i=l+1}B_iw_i(x)+t(x)B_h(x)\big)=0 $$
且无论$A(x)$是否为零，该项均为零，因此式1也为零
Baghery等人论文中的定理2可以解决这个问题，该定理分析了每个系数对应的方程来提供正确的合理性分析，并且与Groth16不同的是，Baghery等人的定理2明确声明了$A(x)=0$的情况，目的是适配基于III型配对的Groth16方案（但是证明仍然是非III型配对）
5.3 Lipmaa's Simulation Extractable SNARK
对Lipmaa不太了解，回头有空补个课
这里先留个坑
6 SNARK Transformations
没看懂
7 Conclusion
总结一下，本文研究了SNARK的形式化证明，有助于未来的研究员对其他的SNARK协议的安全性研究
References
$[1]$ Formalizing Soundness Proofs of SNARKs (iacr.org)
$[2]$ Karim Baghery, Markulf Kohlweiss, Janno Siim, and Mikhail Volkhov. Another look at extraction and randomization of groth's zk-snark. Cryptology ePrint Archive, Report 2020/811, 2020. https://ia.cr/2020/811.
$[3]$ Andrew Miller, Ye Zhang, and Sanket Kanjalkar. Baby snark (do do dodo dodo. 2020.)
$[4]$ 精读Groth16算法 - 三两老友杂的小岛 (snowolf0620.xyz)