为了深入理解形式化验证技术是如何应用于 zkVM（零知识虚拟机）之上的，本文将聚焦于单条指令的验证。
作者：Certik
封面：Photo by Cory Bunge on Unsplash
为了深入理解形式化验证技术是如何应用于 zkVM（零知识虚拟机）之上的，本文将聚焦于单条指令的验证。关于 ZKP（零知识证明）先进形式化验证的总体情况，请查阅我们同期发布的「零知识证明区块链的先进形式化验证」文章。
什么是 ZK 指令的验证？
zkVM（零知识虚拟机）能够创建简短的证明对象，以作为证据来证明特定程序可以在某些输入上运行、并成功终止。在 Web3.0 领域，zkVM 的应用使得吞吐量变高，这是因为 L1 节点只需要验证智能合约从输入态到输出态转变过程的简短证明，而实际的合约代码执行则可以在链下完成。
zkVM 证明器首先会运行程序以生成每一步的执行记录，然后将执行记录的数据转换为一组数字表格（该过程被称为「算术化」）。这些数之间必须满足一组约束（即电路），其中包括了具体表单元格之间的联系方程、固定的常数、表间的数据库查找约束，以及每对相邻表行间所需要满足的多项式方程（亦即「门」）。链上验证可以由此确认的确存在某张能满足所有约束的表，同时又保证不会看到表中的具体数字。
每条 VM 指令的执行都面临很多这样的约束，这里我们将 VM 指令的这组约束简称为它的「ZK 指令」。下面是用 Rust 语言编写的一个 zkWasm 内存加载指令约束的示例。
ZK 指令的形式化验证是通过对这些代码进行形式化推理来完成的，我们首先将其翻译成形式化语言。
即便只有单个约束包含错误，攻击者都因此而有可能提交恶意的 ZK 证明。恶意证明所对应的数据表格并不对应智能合约的合法运行。与以太坊等非 ZK 链不同，后者有许多节点运行不同的 EVM（以太坊虚拟机）实现，从而不太可能在同时同地出现相同的错误，一个 zkVM 链则只有单一的 VM 实现。单就这个角度而言，ZK 链比传统的 Web3.0 系统更为脆弱。
更糟糕的是，和非 ZK 链不一样，由于 zkVM 交易的计算细节并没有被提交并存储在链上，在攻击发生后，不仅是要发现攻击的具体细节非常困难，甚至要识别攻击本身也会变得极具挑战性。
zkVM 系统需要极为严格的检视，不幸的是，zkVM 电路的正确性很难保证。
ZK 指令的验证为何很难？
VM（虚拟机）是 Web3.0 系统架构中最为复杂的部分之一。智能合约的强大功能是支撑 Web3.0 能力的核心，其力量源自于底层的 VM，它们既灵活又复杂：为了完成通用计算和存储任务，这些 VM 必须能够支持众多的指令和状态。比如，EVM 的 geth 实现需要超过 7500 行 Go 语言代码。类似的，约束这些指令执行的 ZK 电路也同样庞大而复杂。像在 zkWasm 项目中，ZK 电路的实现需要超过 6000 行 Rust 代码。
与专为特定应用（如私人支付）设计的 ZK 系统中使用的专用 ZK 电路相比，zkVM 电路的规模要大得多：其约束规则的数量可能比前者多出一到两个数量级，而其算术化表格则可能包括数百列、含有数以百万计的数字单元格。
ZK 指令的验证意味着什么？
我们在这里想要去验证 zkWasm 中的 XOR 指令的正确性。从技术上讲，zkWasm 的执行表对应一个合法的 Wasm VM 执行序列。所以宏观来看，我们想要验证的是：每次执行这条指令总是会产生一个新的合法的 zkVM 状态：表中的每一行都对应 VM 的一个合法状态，而紧接着的一行则总是要通过执行相应的 VM 指令来生成。下图为 XOR 指令正确性的形式化定理。
这里「state_rel i st」表明状态「st」是步骤「i」中智能合约的合法 zkVM 状态。 正如你可能猜测的那样，要证明「state_rel (i+1) …」不是轻而易举的。
如何验证 ZK 指令？
尽管 XOR 指令的计算语义很简单，就是计算两个整数的按位异或（bitwise xor）并返回整数结果，但它所涉及的方面却比较多：首先，它需要从栈内存中取出两个整数，进行异或计算，然后将这个计算得出的新整数存回同一个栈。此外，该指令的执行步骤应融入于整个智能合约的执行流程中，并且其执行顺序及时机必须正确。
因此，XOR 指令的执行效果应该是从数据堆栈中弹出两个数，压入它们的 XOR 结果，同时增加程序计数器，以指向智能合约的下一条指令。
不难看出，这里的正确性属性定义总体上与我们在验证传统字节码 VM（比如以太坊 L1 节点中的 EVM 解释器）的时候所面对的情况非常相似。它依赖于机器状态（这里指栈内存和执行流）的高级抽象定义，以及关于每条指令预期行为的定义（这里指算术逻辑）。
然而，如我们下面所将要看到的，由于 ZKP 和 zkVM 的特殊性，其正确性的验证过程经常与常规 VM 的验证很不一样。光是验证我们这里的单条指令，就要依赖于 zkWASM 中很多表的正确性：其中有一张用于限制数值大小的范围表，一张用于二进制位计算中间结果的位表（bit table），一张每行都存储恒定大小的 VM 状态的执行表（类似物理 CPU 中的寄存器和锁存器中的数据），以及代表动态可变大小的 VM 状态（内存、数据栈和调用栈）的内存表和跳转表。
第一步：栈内存
与传统 VM 类似，我们需要确保指令的两个整数参数可以从堆栈中读取，并且其异或结果值被正确地写回堆栈。堆栈的形式化表述看起来也相当熟悉（还有全局内存和堆内存，但 XOR 指令不使用它们）。
zkVM 使用一种复杂的方案来表示动态数据，这是因为 ZK 证明器并不能原生支持像堆栈或数组这样的数据结构。相反的，对于压入堆栈的每个数值，内存表用单独的一行来记录，其中的某些列则用于指示该表项的生效时间。当然，这些表的数据可以被攻击者所控制，因此还必须加以一些约束，以确保表项真实对应于合约执行中的实际压栈指令。这是通过精心计算程序执行过程中的压栈次数来实现的。验证每一条指令时，我们需要确保这个计数始终正确。此外，我们还有一系列引理，将单条指令生成的约束与实现堆栈操作的表查找和时间范围检查相关联。从最顶层看，内存操作的计数约束定义如下。
第二步：算术运算
与传统 VM 类似，我们希望确保位异或的运算正确无误。这看起来很容易，毕竟我们的物理计算机 CPU 都能够一次性完成这个操作。
但对于 zkVM 来说，这实际上并不简单。ZK 证明器原生支持的唯二算术指令是加法和乘法。为了进行二进制位运算，VM 使用了一个相当复杂的方案，其中一张表存放固定的字节级运算结果，另一张表则充当「草稿本」，用以在多个表行上展示如何将 64 位数字分解为 8 个字节，然后再重新组合出结果。
在传统的编程语言中非常简单的异或运算，在这里则需要很多引理来验证这些辅助表的正确性。对于我们的指令，我们有：
第三步：执行流
与传统 VM 类似，我们需要确保程序计数器的数值正确更新。对于像 XOR 这样的顺序指令，每次执行步骤后，程序计数器需要加一。
由于 zkWasm 被设计用来运行 Wasm 代码，因此也要确保在整个执行过程中，Wasm 内存的不变性质始终得到保持。
传统的编程语言对布尔值、8 位整数、64 位整数等数据类型有原生支持，但在 ZK 电路中，变量始终是在大素数（≈ 2254）模下的整数范围内变化。由于 VM 通常以 64 位数运行，电路开发者需要使用一套约束系统来确保它们具有正确的数值范围，而形式化验证工程师则需要在整个验证过程中追踪关于这些范围的不变性质。对执行流和执行表的推理会涉及到所有的其他辅助表，因此我们需要检查所有表数据的范围是否正确。
类似于内存操作数量管理的情形，zkVM 需要一组类似的引理来验证控制流。具体而言，每个调用和返回指令都需要使用调用栈。调用栈使用与数据栈类似的表方案来实现。对于 XOR 指令，我们并不需要修改调用栈；但验证整条指令时，仍然需要追踪并验证控制流操作计数是否正确。
验证这条指令
让我们将所有步骤整合起来，验证 zkWasm XOR 指令的端到端正确性定理。以下验证是在交互式证明环境中完成的，其中每一个形式化构造和逻辑推理步骤都经过了最严格的机器检查。
如上所见，形式化验证 zkVM 电路是可行的。但这是一项艰巨的任务，需要理解和追踪很多复杂的不变性质。这反映了被验证软件本身的复杂性：验证中所涉及的每一条引理都需要得到电路开发者的正确处理。鉴于其中的风险很高，让它们由形式化验证系统进行机器检验，而不是仅仅依靠小心谨慎的人工审查，是非常有价值的。
免责声明：作为区块链信息平台，本站所发布文章仅代表作者及嘉宾个人观点，与 Web3Caff 立场无关。文章内的信息仅供参考，均不构成任何投资建议及要约，并请您遵守所在国家或地区的相关法律法规。
