RISC Zero的ZK-VM安全性：Veridise如何帮助RISC Zero实现可证明和持续的零知识验证…

RISC Zero的ZK-VM安全性：Veridise如何使RISC Zero实现可证明和持续的ZK安全性

自2024年7月以来，Veridise与RISC Zero密切合作，该公司正在开发RISC Zero zkVM——一个利用RISC-V架构进行安全和私密计算的零知识虚拟机。

虽然我们为RISC Zero完成了多次安全审核，但我们的安全合作不仅限于审核。

在这篇博客文章中，我们强调了我们是如何合作的，使用Picus，Veridise的自动化ZK验证工具，为他们的zkVM提供正式保证。我们解释了这样的集成如何实现他们电路不断演变的持续自动验证。最后，我们详细描述了我们在此过程中识别和缓解的三个关键漏洞。

实现数学上可证明的ZK安全性

我们与RISC Zero的合作旨在实现比传统审计更高标准的ZK安全性。

我们一直在帮助RISC Zero，让他们成为首个具有正式保证的RISC-V zkVM，以抵御最常见和关键的ZK漏洞之一：约束不足的漏洞。

利用我们的自动化ZK验证工具Picus，我们已经形式化验证了它们zkVM的关键组件的一致性。这个过程特别针对约束不足的电路——根据最新研究，这些电路负责近97%的已知ZK电路漏洞。

从一次性审核到持续验证

传统的手动安全审核在固定时间点提供有价值的见解——但随着代码库的演变，它们往往会变得过时。这可能会使关键组件暴露于审核完成后出现的新漏洞中。

通过将形式化方法与自动化工具相结合，我们实现了对RISC Zero的zkVM电路的持续验证。与Picus的集成与他们的代码库一起演变——自动检测引入的更改中的关键缺陷。这确保了在整个开发生命周期内，安全保证保持完整。

通过这种方法，RISC Zero无需在快速迭代和高保证之间做出选择。他们两者兼得：数学上可证明的安全性，持续维护，不牺牲开发速度。

与RISC Zero的合作

项目开始于在西雅图举行的一次长时间亲自会议。这些初步讨论在许多方面都非常富有成效，例如，它们加快了将RISC Zero的ZK电路语言转换为可以与Veridise的ZK工具Picus一起使用的形式的过程。

启动后，我们定期与RISC Zero举行会议，通常每周与他们的首席执行官、首席技术官和安全专家会面。RISC Zero团队在会议后迅速跟进任何未解决的问题。我们还通过一个共享的Slack频道进行了频繁的沟通。

RISC Zero的模块化设计简化了电路验证

RISC Zero的ZK电路易于使用，并且验证其正确性也很简单，这得益于他们的Zirgen DSL，使得读取和提取逻辑变得简单——非常适合我们的ZK漏洞检测工具Picus。

更有帮助的是RISC Zero的模块化设计理念。他们没有将所有逻辑塞进一个巨大的电路中，而是将它们分成可管理的部分，以便我们可以单独分析。

我们迄今验证的内容

到目前为止，我们与RISC Zero的合作成功确认了他们Keccak加速器电路的一致性，以及即将推出的R0VM 2.0版本的新RISC-V电路的相当大一部分。我们目前正在共同努力，完成整个RISC-V电路的完整正式证明。

正如RISC Zero在公告中所写：

“有了R0VM 2.0，ZK安全性不仅更强大，还可以证明。”

RISC Zero的观点：阅读他们的公告以获取更多细节

要了解更多关于我们与RISC Zero的合作，请阅读Jacob Weightman的博客文章 “RISC Zero通往首个形式化验证的RISC-V zkVM之路”。

Jacob描述了Veridise的形式化方法和自动化工具（Picus）如何使他们的核心zkVM组件具有可证明的持续安全保证。他还向你介绍了为何要优先处理约束不足的漏洞，Picus的大概工作原理，并详细描述了Keccak加速器电路的证明。

Veridise在RISC Zero zkVM中修复的三个漏洞：

在这篇文章的下半部分，我们将详细描述Veridise在我们的安全评估期间识别和帮助缓解的三个关键漏洞。

我们的安全评估涵盖了RISC Zero的zkVM的各个组件，耗时96个人周，由六名安全分析师在16周的时间内审查该项目。

1) Component ExpandU32约束不足 (5.1.1)

第一个漏洞是在“ExpandU32”组件中存在约束不足电路漏洞。

ExpandU32组件如下所示，输入一个类型为ValU32的值x，以及一个布尔变量signed，表示x是否为有符号值，返回字节b0、b1、b2和b3，代表x的第i字节。ValU32类型是Felts(low, high)的一个元组，其中low旨在捕捉低16位，high捕捉高16位。

基本思想是，值x旨在表示一个u32值。然而，由于所有操作都在BabyBear域内，因此u32不能被直接表示。为了解决这个问题，开发人员将u32值拆分为两个字段元素：low和high。low字段元素捕捉u32的低16位，而high字段元素捕捉高16位。

进一步分解后，x表示的u32值被分成四个不同的字节值：b0、b1、b2和b3。这个过程背后的逻辑相对复杂，审计报告中对此进行了更详细的解释。简而言之，b0到b2是使用NondetU8Reg机制初始化的，这确保了这些值将是字节。

然而，原始实现中有一个疏漏：没有对b3应用相同的约束。这一遗漏使攻击者能够利用表示，因为b3可以被设置为超出字节范围的值。因此，u32值可以以多种意外方式表示，从而启用关键的漏洞。

问题在于它们如何表示b3Top7times2。该字段旨在持有一个u8值，并且约束为字节。然而，在设置b3值时，他们进行了除以2的操作。在标准计算机程序中，除以2将执行整数除法。例如，将255除以2将得到127。在这种情况下，除以2并不相同——它涉及在字段内乘以2的逆元。这允许b3Top7times2被设置为一个大的字段元素。如果b3Top7times2是一个奇数，乘以2的逆元将产生另一个较大的值。因此，b3字节不再遵循有效字节的约束，因为它超过了允许的范围。

在审计报告中，我们更详细地分析了这个漏洞，并提供了一个恶意证明者利用该漏洞的示例。

💡 修复方法： 对于这个问题的修复是在b3的初始化中使用u8寄存器，就像其他字节（b0、b1、b2）一样。这确保了b3被适当地约束在有效字节范围内。一旦进行了这个调整，该问题就解决了。

2) DoDiv约束不足 (5.1.2)

下一个漏洞出现在一个名为DoDiv（执行除法）的模块中，这是RISC Zero zkVM中负责执行所有除法操作的主要电路。

该电路的目的是将一个分子和一个分母作为输入，并生成相应的商和余数。

挑战在于直接在电路中实现一个除法算法，这是相当复杂的。为简化此过程，RISC Zero团队采用了一种聪明的技巧：给定一个分子和分母，他们猜测一个商和余数，然后断言关系：

分子=(商×分母)+余数。

他们实现中的bug出现是因为缺失了对商和余数的关键约束。具体来说，攻击者可以将余数和商操纵为他们想要的任何值。

为了使该方法正确工作，必须断言余数始终小于分母并且商在除法操作的上下文中是有效的。

此外，关于商的符号的复杂性也是相关的，具体取决于除法是有符号还是无符号。为了简单起见，我们在这篇博客总结中跳过了有符号/无符号的复杂性。

本质上，原始代码未能强制执行“余数必须始终小于分母”这个关键约束，这导致电路约束不足。

示例：

以下是一些补充内容和背景，帮助澄清这个漏洞：

通常构建实现可直接计算商和余数的算法。然而，这些算法在电路内复制的计算开销较大。为了解决这个问题，使用了以下标准方法：电路“猜测”商和余数，然后添加一个约束进行验证：

分子=(商×分母)+余数

然而，如果这仅是添加的唯一约束，会出现问题。例如，考虑6除以2：我们期待的结果是商为3和余数为0。

但如果没有额外约束，就可能出现其他解决方案。例如：

• 商=0，余数=6（满足该公式）。
• 商=1，余数=4（也满足该公式）。

这些解决方案是错误的，但电路无法区分它们，因为缺乏额外的规则。为了确保正确和唯一的结果，必须添加约束：

• 余数必须小于分母。
• 余数也必须为非负数。

在该电路中，唯一的断言是：分子=(商×分母)+余数。

然而，代码未能包含“余数必须小于分母”这一关键约束。没有这个约束，电路就会约束不足，导致错误的结果也能满足公式，从而引发严重的漏洞。

💡 修复方法： 此漏洞可以通过添加约束断言“余数 < 分母”来修复。

3) 解码器约束不足 (5.1.4)

该漏洞的核心问题在于如何处理作为u32值的RISC-V指令。当处理RISC-V指令（编码指令）时，处理器必须对其进行解码以确定操作及执行所需的各种参数。

该电路负责解码指令并提取所有相关参数。

带下划线的参数表示指令的解码组件。

第11行和第20行的约束旨在确保这些参数被正确解码。每个解码参数对应指令的具体位，约束验证这些值是从适当位推导而来的。这是一种聪明的方法，以验证解码的正确性。

然而，解码过程的实现不正确，导致电路约束不足。问题出在第一行的_rd_0字段声明上。

_rd_0字段被初始化以接受0到3（不包括3）范围内的值，但它应该只允许0到1（包括1）之间的值。这种过于宽松的范围允许_rd_0字段接受无效值，从而引入不一致性。

结果，攻击者可以操纵解码过程，因为单个编码指令有多种有效解释，造成重大问题。这意味着攻击者可以为同一个ELF二进制文件生成两个执行证明，从而利用此漏洞。

💡 修复方法： _我们建议将_rd0更改为NondetBitReg，而不是NondetTwitReg。我们在进行修改后运行了Picus，并证明电路是确定的。

针对zkVM内存建模调整Picus

虽然对zkVM的审计与其他零知识应用大体相似，但我们必须进行一些调整。

zkVM必须以许多其他电路（尤其是传统R1CS风格电路）所不具备的方式利用程序内存。因为Picus不直接建模内存，所以我们需要开发一种策略，在zkVM电路中以Picus能够推理的方式编码内存读写。

我们决定将内存读取建模为Picus中的输入，将内存写入建模为输出。这种方法结合初始内存状态作为证明输入提供，给了我们一个归纳论证，说明这种编码是合理的。

最后评论：提升ZK安全性标准

我们与RISC Zero的合作代表了一种模式，展示了深入合作、形式化方法和自动化工具如何共同提高零知识系统的安全标准。

通过将传统审计与正式保证和通过Picus的持续验证相结合，我们帮助RISC Zero构建了一个zkVM，它不仅_声称_安全——它可以_证明_安全性。随着ZK基础设施成为下一代去中心化应用的基础，这种程度的保证显得愈发重要。

得益于我们与RISC Zero的顺利合作，我们还能够对Picus本身进行改进。Picus解决了某些性能问题，使其更具可扩展性。因此，我们在未来有能力处理复杂的ZK审计。

我们很自豪能够支持RISC Zero，为zkVM安全设定新的行业基准。随着他们产品的发展，我们期待继续我们的合作——并帮助更多团队在ZK生态系统中应用同样的高安全标准。

完整审计报告

在此处下载完整的RISC Zero zkVM审计报告：https://github.com/risc0/rz-security/blob/main/audits/zkVM/veridise_zkVM_20250224.pdf

作者：

Shankara Pailoor，ZK工具负责人

编辑：Mikko Ikola，市场副总裁

想了解更多关于Veridise的信息？

Twitter | LinkedIn | Github | 请求审计

• 原文链接： medium.com/veridise/risc...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～