本节主要介绍如何以形式化的方式确保ZK电路的安全性
区块链软件的bug在许多时候都具有很高的危险性，一旦这些软件出现了安全漏洞，黑客可以很轻松的提取或者伪造大量的加密货币，为了防止黑客利用这些bug来攻击区块链生态，在区块链系统中抓虫（find bug）和其他系统安全同样重要
这里的软件包括但不限于共识算法、智能合约、web应用（钱包之类的）、ZKP电路等等一系列与区块链配套的东西
bug看起来危害性很大，尤其是代码实现的过程中不可能完全避免bug（毕竟代码是人写的，人必然会犯错，哪怕是GPT写的也不一定完全没有bug），不过bug也不是完全不可避免，可以用形式化的方式来分析，并实现更安全的区块链系统
Introduction to Formal Methods
Formal Methods in a Nutshell
形式化证明简单来说就是以严格的数学方式来证明一个系统或代码是否安全，这个技术被广泛应用于fuzzing、软件分析、代码安全等多个领域
形式化验证可以分为两种：动态形式化和静态形式化，动态形式化就是执行程序，给定一些特殊的输入，并分析程序执行过程中可能导致的中间结果或者输出，fuzzing就属于这种
静态形式化就是对源代码进行分析，推理所有可能的执行结果，并分析这些结果是否会引起系统的不安全，代码安全分析属于这一种（应该属于，笔者不太懂）
本文主要关注静态形式化，但是静态形式化技术实际上很难推断给定程序的确切行为，因为程序的上下文通常不确定，但是无法推断程序实际执行过程中的行为并不意味着无法从抽象层面对其进行推断，因此可以通过对程序进行抽象，来获得一个过度-近似的保守推断（Obtain a conservative over-approximation），并期望这个推断足以证明程序的安全性
为了实现这一目标，通常使用抽象表示法（Abstract Interpretation）这个框架来获取程序执行的近似结果
这里给一个图来具体说明一下
这里蓝色代表程序实际的状态，绿色代表静态分析出来的可能的状态，红色表示预期之外的行为，包括漏洞、bug或不好的状态，不难看出蓝色的形状是不规则的，因为很难准确推断出程序在实际执行过程中的行为，不过我们可以用过度-近似的方式计算这个规则的绿色区域，从而覆盖所有可能的实际执行状态
这个例子中，红色和绿色没有交集，这表示这个程序经过静态分析后没有任何预期之外的行为，这表示程序很安全
但是并不是所有的程序都是这样的，还有可能出现下列两种情况
比如上图左侧，红色和绿色部分有交集，但是和蓝色部分没有交集，此时称为假阳性（False Positives），因为这些预期之外的行为并不会在实际执行中出现，只是静态分析的过度近似覆盖到了一部分错误行为而已，导致假阳性的主要原因是静态分析的近似性不够，这意味着采用的抽象方式并不能很好的拟合程序的实际执行状态（从图中可以看出，蓝色仅占了绿色的很小一部分）
不过右侧的假阴性（Flase Negatives）就不是很好了，首先静态分析仅包含了实际执行中一部分，并没有覆盖所有可能的执行状态，而且没有被覆盖到的状态中还包含了预期之外的行为，这也是不期望发生的，不仅没有覆盖所有状态，更关键的是没有覆盖到的状态中包含预期之外的状态，这就意味着不能很好的进行抓虫
这里为了便于理解，可以举一个具体表示法的例子，比如说等式$x=y+z$，如果$y=1,z=2$，则显然$x=3$
抽象表示法也是一样的，只不过抽象表示法用的值是抽象的值，而不是上面这种123的具体的值
还是上面$x=y+z$的例子，此时值以范围的形式给出$y\in[a,b],z\in [c,d]$，而不是像上面那样给一个具体的值，经过抽象解释器之后，可以得到$x\in [a+c,b+d]$
从这个例子可以看出，抽象表示法本质上就是通过符号执行或者符号推理的方式来找到程序所有可能的执行路径
如果说程序中出现分支，需要考虑所有的分支情况，比如下面这段代码中，抽象之后的$x$的取值就是$x\in [-1,1]$
if flag : x = 1
else x = -1 但实际上这是对$x$的值得过度近似，因为$x$实际上只会取到-1和1，其他中间的值根本不会取到
不过抽象表示法可以很好的分析智能合约中的bug，尤其是重入攻击（Reentrancy Attack） ，该攻击可以让敌手在不更新余额的情况下对用户的资金进行多次恢复
这里举个例子，左侧是攻击程序，右侧是被攻击的程序，这里右侧有一个提款的函数withdraw，用来提取sender的余额
如果说这个withdraw函数正好是攻击者payable函数和exploit函数的回调函数，那此时攻击者可以利用重入攻击来重复调用withdraw函数来进行二次或者多次提款
这里只是一个简单的例子，实际的智能合约更加复杂，为了捕获实际智能合约的这种类似的bug，可以利用基于时间顺序的抽象表示法，此时可以检查时间顺序中是否有重复的状态更新（或者重复的危险调用），如果有，则意味着敌手可以进行重入攻击
除了重入攻击以外，还有很多会导致智能合约被攻击的bug，包括但不限于：类型溢出、交易顺序依赖性、闪电贷（Flashloan Attack）等等，为了检测这些攻击，学界和开发者大佬们也给出了不少的解决方案，比如Slither（TrailOfBits）、Banguard（Veridise）、Sailfish（Oakland 2022）、Securify（CCS 2019）
From Abstract Interpretation to Formal Verification
尽管抽象表示法可以很好的检测到特定的bug和漏洞，但是并不能保证程序完全没有逻辑错误
简单来说就是抽象表示法可以分析函数是否按照预期的行为进行计算，但是并没有以形式化的方式检测函数是否存在某些逻辑错误，
说的简单一点：形式化规范是一种对程序预期行为的精确数学描述，这个方法通常用在形式化逻辑中，具体的比如一阶逻辑或时序逻辑
如果需要使用形式化分析，有一个前提条件：需要有一个形式化规范（Formal Specification）来表明程序的预期的行为
然后接下来看一下形式化验证的框架，这里放一张图
形式化验证中有两个程序，分别称为Verifier和Prover，这里的Prover和Verifier和ZKP协议中的Prover和Verifier不是同一个概念，需要区分一下
Verifier有三个输入
- Code：待验证的源代码或者字节码
- Specification：待验证程序的性质的形式化描述
- Annotations（可选）：一些注释信息
Verifier会利用一个称为验证条件生成器（Verification Condition Generator， VC）的玩意，将这些输入编译为逻辑公式，VC生成器确保了当且仅当逻辑公式有效时，代码可以满足给定的形式化描述
这个逻辑公式的有效性检查通常通过Prover进行检查，比如利用诸如Z3，CVC4之类的SMT求解器进行判断，如果Verifier输出Proven，则表示输入的源代码可以满足给定的形式化描述，说白了就是如果逻辑公式有效，则意味着这段代码在数学上是满足给定的形式化描述的
举个例子，比如下面左侧这段代码
经过VC生成器之后，可以得到右边的这个逻辑公式$F$，不难看出，无论如何执行这段代码，$F$总是为真（$x$总是大于0）
形式化验证是一个很好用的工具，因为当证明有效时，可以确保程序有效，但是证明无效时，通常意味着下列几种问题
- 逻辑错误：这里就是真阳性了，和前面提到的假阳性和假阴性都不同，真阳性表明程序确实存在逻辑上的问题
- 不可满足性：比如不可满足的输入，不可满足的循环条件等等
- Prover不完备：这个时上面的Prover的问题，从上面的分析我们可以知道，Verifier的工作分为两步，首先构造逻辑公式，然后将该公式“代理”给Prover进行验证，如果说Prover不完备（不够强大），或者说Prover只能验证一些简单的逻辑，此时就无法检测到代码中不满足形式化描述的一些问题
第三点需要特别关注一下，因为ZKP验证中经常会出现此类情况，如果说Prover只能处理线性算术，且代码中也只包含线性算术，这没问题，但是如果代码中包含非线性运算，那Prover就有可能检测不到了（而且ZKP电路中很有可能会包含部分甚至大量的非线性运算）
Bounded or Unbounded Verification
到目前为止都是在讨论无界的验证，但是实际上无界验证太难实现了，尤其是大的程序，想要遍历所有的分支几乎不可能实现，因为有的程序根本不知道会不会终止，循环是否会终止，内存是否足够大以运行程序
这里考虑有界的验证方式，通过削弱一些条件来完成验证，比如限制输入大小、限制输入空间、限制循环次数等等来完成验证
有界的方式可以用Certora Prover、K-framework、Mythril、Sailfish等等工具进行验证
Formal Methods in ZK（Part I）
本节介绍一些对ZKP实现的形式化验证，主要是基于Circom和Halo2的，主要分析语义和协议
首先介绍一下电路的原理及其工作流，以circom为例，编译器会将circom源代码编译为两个部分，分别是witness生成器和域上多项式等式，后者还会进一步转换为zkSNARK
对于circom的开发者而言，其在编写ZKP程序时，需要确保witness生成器和对应的约束是等价的，啥意思呢，举个例子
这里$P$表示witness生成器，输入为$x$，输出为$y$，$C$表示约束条件的集合，输入为$x,y$，输出为$true/false$，$true$表示对应的输入可以满足这个约束条件，否则表示不满足约束条件
这两个东西等价意味需要同时满足两种情况
- 在输入为$x$时，由$P$生成的输出$y$可以满足对应的约束条件，也即$C(x,y)=true$
- 所有满足$C$的输入输出对$(x,y)$均满足$P(x)=y$
但是有可能出现不等价的情况，也即违反等价条件（Equivalence Violations），此时可以将此类违反等价条件的情况分为两类
第一类称为过度约束（Overconstrained Bugs），此类情况表明存在某些输入-输出，使得$P(x)=y$，但是这些输入输出对不满足约束条件，也即$C(x,y)=false$
产生此类情况主要有两种原因，第一种是开发者自身的原因，因为在电路中加入过多的约束会导致额外的开销，另一个是编译器自身的问题，circom或者halo2会在编译电路时通过assertion来构造约束，但是编译器在编译过程中会对电路进行优化（尤其是circom），而优化过程中又会加入一些额外的assertion，此时原始的由开发者编写的电路是可满足的，但是加入这些额外的约束之后又不可满足了
第二类称为欠约束（Underconstrained Bugs），此类情况更复杂一些，它表明存在满足约束条件的输入输出$C(x,y)=true$，但是这些输入输出有$P(x)\neq y$
此类情况下会导致ZKP电路非常的危险，因为如果存在某些输入输出满足约束条件，但是其不是由witness生成器构造的输入输出，这意味着敌手或者恶意用户可以利用这个点来伪造证明
回到上面ZKP电路的工作流那张图，可以看到最后电路会生成对应的zkSNARK，包含对应的Prover和Verifier，如果真的出现了欠约束的情况，这意味着Verifier可以在最终的SNARK中接收一个错误的输入-输出对，这个非常严重，Tornado Cash曾经就被这么攻击过（2019年）
为了正确防止此类严重bug的出现，有必要分析ZKP电路和约束系统之间的等价性，这里回到前面的形式化分析，并尝试一些轻量级的静态分析来找到bug
A Taxonomy of ZK Bugs
和之前提到的一样，如果说我们需要对ZKP的bug进行抽象形式化分析，首先需要有这些bug的一些先验知识，比如说这些bug的语法或者语义
之前以太坊基金会和其他的一些大佬组织做了一些研究，分析了现有的大型ZKP开源项目中的语法错误，可以将现有已知的ZKP bugs大致可以分为下列三种类型，如上图所示，这里一个一个分析
Unconstrained Signals
欠约束信号，此类bug和之前的欠约束有点类似，区别在于出现此类bug时，表明对信号的约束条件永远为真（约束无论如何都会被满足）
这里举一个circomlib中的例子，Num2Bits函数的实现，该函数用于将一个n位的域元素转化为对应的二进制形式，这里修改一下源代码[2]中的循环边界，将第7行的错误的循环条件改为i < n - 1（现在的circomlib中的正确的循环条件为i < n）
template Num2Bits(n) {
signal input in;
signal output out[n];
var lc1=0;
var e2=1;
for (var i = 0; i< n - 1; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] -1 ) === 0;
lc1 += out[i] * e2;
e2 = e2+e2;
}
lc1 === in;
}这里可以看到开发者在第9行加入了一个对out[i]的约束，开发者希望将out[i]的值限制在0和1这两种情况，但是注意到第7行的循环条件为i < n - 1，这里的边界条件应该是n，而不是n - 1
再具体一点，如果是$n=3$的情况，上述代码执行完毕后，我们可以得到下面几个约束条件
$$ \left\{\begin{aligned} &input:in\\ &output:out[0],out[1],out[2]\\ &out[0] \cdot (out[0] - 1)=0\\ &out[1] \cdot (out[1] - 1)=0\\ &out[0]+2\cdot out[1] = in \end{aligned}\right. $$
可以看到少了对$out[2]$的二进制约束条件，最终约束条件也少了一个$4\cdot out[2]$的项
如果攻击者发现了这个点的话，$out[2]$可以是任意一个值，因为没有对它进行任何约束，所以是可以通过检查的
Unsafe Component Usage
不安全的组件使用方式，大型ZKP电路开发和程序设计一样，会包含大量的可重用的小函数，小组件之类的，在circom中这些组件称为Component
开发者在开发过程中或许会默认这些组件是安全的，但是如果有一个组件是不安全的，且这个组件在ZKP电路中用到了，甚至是频繁用到了，那整个ZKP电路就都有问题
举个例子，看下面这段代码
这里有两个点，首先可以看到这个函数中调用了两次Num2Bits组件，如果说Num2Bits组件和上面一样具有不安全的实现，那这段代码也是有问题的
另一个倒数第4行的lt = LessThan(n);，这里少了一个lt.out === 0;的约束条件（具体可以看LessThan的实现），这个约束条件表明余额总是应当大于提款的数目，否则不应当完成提款操作，但是可能某个开发者忘记加上这个限制，这样敌手可以提出比账户中更多的钱
Constraint/Computation Discrepancy
第三类问题是计算与约束之间的差异性，因为并不是所有的计算都是可以表示为约束条件的，约束也并不总是可以很好的表示计算的语义
举个例子，求乘法逆元的情况
template MulInverse(){
signal input a;
signal input b;
signal output out;
out <-- a / b;
out * b === a;
}这里函数的目的是求$a$的乘法逆元，但是根据数论的常识，0是没有乘法逆元的，而上述并没有约束$b\neq 0$的情况，这意味着如果输入的$b$为0，则会导致出错
Circuit Dependence Graphs（CDG）
好了，知道问题的种类之后，问题来到了如何检测到这些问题
为了检测这些问题，需要用到前面的抽象形式化，因此需要一个抽象的形式来量化ZKP中的语义，这里引入一个电路依赖图（Circuit Dependence Graphs，CDG）的概念，用于表示ZKP电路中的依赖关系
这里将输入信号以白色表示，输出信号以灰色表示，如果说是数据依赖关系，如o <-- i，则以i到o的单向箭头表示，如果是约束依赖关系i === o，则以虚线连接
举个例子，如果是下面左侧这段代码，可以得到右侧这个电路依赖图
我们得到了这个电路的依赖图的抽象之后，可以利用这个图进行一些检测，比如用请求语言（Query Language）进行检查，也就是下面那四行看不懂的英语
基于上述流程，这里用Vanguard框架来对电路进行分析
首先是将电路的源代码输入Vanguard，利用Vanguard构造电路的依赖图，然后对依赖图进行分析，得到对应的漏洞报告
这里演讲者分析了17个开源circom项目中的258个电路，并检测到了32个之前未知的漏洞，同时还检测到了不少上述三类漏洞
但是我们又如何知道修改是否正确呢，比如说前面Num2Bits的那个例子，把循环条件由n-1改成n之后，我们怎么知道这么改对不对呢，难道重新跑一遍形式化验证么，这也太麻烦了吧
Formal Methods in ZK（Part II）
这里回顾一下之前的欠约束的bug，如果我们希望对修了bug之后的程序进行检测，也即形式化证明新的电路中不存在之前的欠约束的bug，有两种办法
一，对约束条件再跑一遍原来的静态分析，很快，这里如果说约束条件满足某些线性约束关系的话，可以很快得出结论，但是电路不总是包含线性约束条件
二，利用SMT求解器，欠约束的情况可以被表示为SMT求解器的查询，这里将这些欠约束的情况作为求解器的查询，如果说求解器返回一个可满足的结果，则意味着电路中存在欠约束的情况，比静态分析慢得多
不过这两种方式各有优劣，静态分析的方式具有很好的可扩展性，非常适用于大型电路的验证，但是缺点在于很容易产生误报（假阳性或者假阴性），而求解器不会有误报的情况，因为求解器底层是非常精确和严格的符号推理，但是这也意味着其难以扩展至具有大量约束的电路
Picus
为了解决上述两个方式的问题，这里介绍一个新的玩具，称为Picus
Picus可以以一组域上多项式等式作为输入，并返回电路是否可满足，可满足返回1，不可满足返回0，如果上述两种情况均不成立，则会返回一些其他的信息（比如返回一个Unknown）
Picus的关键思想在于结合了静态分析的扩展性和求解器强大的分析能力，使得其可以对大型电路进行分析，两者互补，在确保分析效率的同时，又利用求解器来弥补静态分析中的误报的情况
下面看一下Picus的工作流，分为两个阶段
Static Analysis Phase
首先是静态分析阶段，该阶段会输入一系列的域上等式$P$，以及信号集合$K$，最开始信号集合为空集，也即$K=\{\}$
然后Picus会在每次迭代中在静态分析器中加入对应的约束等式，然后生成一个新的信号集合$K'$
经过若干次迭代之后，静态分析器会得到最终的信号集合，如果说电路的最终输出信号是最终集合$K'$的子集，也即$\mathrm{OutputSignals}\sube K'$，则表明约束是可满足的，此时Picus会输出1，表示电路可满足
如果说静态分析阶段中Picus没有输出1，则会将这个集合$K'$传递给SMT求解器，进行下一个阶段
SMT Phase
这里SMT求解器有两个输出，第一个$K''$和静态分析里面一样，第二个$K_{uncons}$表示那些不满足约束条件的信号的集合
将静态分析的结果丢给SMT求解器之后，如果说$\mathrm{OutputSignals}\sube K''$，则仍然表明约束是可满足的
但是如果$\mathrm{OutputSignals}\cap K_{uncons} \neq \empty$，则返回0，表示输出信号中存在不可满足的信号
还有一种情况，为$K=K''$，此时返回Unknown，表示SMT求解器无法搞定这个情况
如果说没有出现上述三种情况，则将$K''$返回给静态分析器，重复上述过程，直到SMT求解器给出一个对应的输出为止
Evaluation
这里演讲者利用上述三种方式（静态分析，SMT求解器，Picus）分析了现有的163个开源的circom电路，得到了下面这个结果
上面的表格是一些统计数据，下面的图表表示分析结果，可以看到Picus可以分析出更多电路中的bug
Future Directions
回到最开始的那个图
大部分的形式化证明主要依赖于用于验证逻辑公式有效性的Prover，所以问题在于：如果Verifier无法得到有效的证明时，我们应当如何构造相关的信息来反馈电路中潜在的bug
References
$[1]$ ZKP MOOC Lecture 15: Secure ZK Circuits with Formal Methods - YouTube
$[2]$ circomlib/bitify.circom at master · iden3/circomlib · GitHub