RISC Zero通往首个形式化验证RISC-V zkVM之路

返回

RISC Zero迈向首个形式化验证的RISC-V zkVM之路

概要;

RISC Zero 正在通过即将发布的R0VM 2.0版本提升ZK安全性。我们的目标：一个既非常快又具有可证明安全性的zkVM，以便开发者无需妥协。

通过与Veridise的合作，我们正在使用Picus来形式化验证我们的zkVM各个组件的确定性。这种自动化的验证过程针对的是欠约束的错误，研究表明，这种错误占了ZK电路漏洞的近97%。通过证明我们的电路对于任何给定的输入都只有一个有效的输出，我们有望成为第一个具有针对最常见ZK安全缺陷的形式化保证的RISC-V zkVM。我们最初的工作已经确认了我们整个Keccak加速器和我们新的RISC-V电路的大部分组件的确定性。我们希望很快能得到RISC-V电路的完整证明。这种方法将严格的安全性与敏捷的开发相结合，从而能够在我们的电路演进时进行持续的形式化验证。有了R0VM 2.0，ZK安全性不仅更强，而且是可证明的。

欠约束错误的终结

不幸的现实是，构建安全的ZK软件非常困难。幸运的是，RISC Zero 即将变得更加安全。我们正处于开发R0VM 2.0的最后阶段，除了比我们之前的版本快几倍之外，它还包括对我们某些电路的一个新的安全属性的形式化证明：确定性。

首先，介绍一点背景知识。ZK软件中的大部分安全缺陷都来自电路：使用像RISC Zero这样的zkVM的主要原因之一是简化你的应用程序的安全性，因为你可以用像Rust这样的高级语言编写你的应用程序，而无需编写你自己的电路。不幸的是，你仍然必须相信我们做得正确。电路将计算编码为一组约束，这是一堆描述计算的输入和输出之间关系的等式。编写电路困难的原因是，如果你忘记了一个等式，你就会允许额外的你并不想要的“输出”。这些错误被称为欠约束错误，它们允许恶意的证明者令人信服地谎报计算结果，这会破坏可靠性，并且通常是一个关键的漏洞。

现在让我们将其与确定性联系起来。确定性计算是指输出完全由输入加粗确定加粗的计算 - 换句话说，对于你传入的任何数据，你都会得到一个可预测的输出。另一方面，非确定性计算可能会给出几个不同的结果。因此，如果我们试图为确定性计算编写一个电路，例如评估哈希函数或模拟RISC-V处理器，并且我们可以证明我们的电路加粗实际上加粗是确定性的，那么我们就知道我们没有任何欠约束的错误。原因很简单：没有我们不希望的运行我们计算的方法，因为只有一种！

感谢与Veridise的富有成效的合作，我们能够使用他们的Picus工具来数学证明（在一些相对标准的假设下）我们的一些电路是确定性的，因此完全没有欠约束的错误。这是一件非常重要的事情 - 最近的一些研究表明，高达三分之二的ZK错误属于这一类别。这也意味着，如果一个电路被证明是确定性的，那么它就被证明没有加粗任何加粗此类错误。到目前为止，我们已经证明了我们整个Keccak加速器电路是确定性的，以及我们新的RISC-V电路中的一些大部分组件。我们很快将进行整个电路的证明，这将是RISC-V zkVM的第一个此类证明。

给我看数据！

让我们支持这些数字，因为它似乎有点离谱，三分之二的错误都属于这样一个狭窄的类别。这个数字是基于以太坊基金会和0xPARC赞助的最近的工作，代表了ZK领域的广泛合作，它为ZK应用程序提供了一个有用的系统模型，以及一个用于推理不同类型错误频率的有用数据集。在搜索了该领域一堆项目的审计报告、安全公告和问题跟踪器后，该团队创建了一个真实的ZK错误语料库，并定义了他们遇到的所有漏洞的分类。在高度概括的层面上，他们将ZK应用程序堆栈分解为四个层：

1. 电路层 - “要证明的计算”的数学描述，由前端处理。对于我们的zkVM，该计算是模拟在用户程序上运行的RISC-V处理器，该程序在Zirgen DSL中实现。

2. 前端层 - 从电路描述到证明者和验证者使用的工件的转换。对于我们来说，这包括我们的执行器、preflight以及Zirgen编译器的输出。

3. 后端层 - 核心证明系统，包括证明者和验证者逻辑。

4. 集成层 - 其他所有内容：证明委托、证明聚合、验证者智能合约等。

任何层的错误都可能构成严重的安全风险。然而，该研究背后的团队发现，错误并非均匀地分布在各层中。在我们RISC Zero的经验中，电路中的约束错误是迄今为止最常被发现的漏洞，并且数据证实这在各个项目中都是如此。绝大多数 - 141个中的99个，或约70%的错误 - 出现在它们各自堆栈的电路层中。这是一个强烈的指标，表明电路层是开始的正确位置。

事实证明，实际上在电路层中有一个更好的地方可以关注。他们进一步将电路漏洞分为三种：

1. 欠约束错误 - 电路缺少一些检查，因此某些无效计算的见证被接受为有效。这会破坏可靠性。

2. 过约束错误 - 电路具有过于严格或矛盾的检查，因此某些有效计算的见证无法被接受为有效。这会破坏完整性。

3. 计算错误 - 见证生成程序计算错误的见证，这会导致“诚实”的证明者生成无效的证明。这会破坏完整性。

事实证明，电路层中几乎所有的漏洞都是第一种 - 99个中的95个，或语料库中约96%的电路错误 - 都是欠约束错误。在系统的所有层中，141个中的95个或加粗超过三分之二加粗的加粗所有加粗语料库中的错误都是欠约束的电路错误。这类错误使数据集中所有其他类型的安全漏洞相形见绌，因此如果我们能够完全避免我们软件中的任何一类错误，那就是它了。

稍微思考一下，这似乎是一个相对自然的结果 - 从根本上说，测试完整性问题比可靠性问题更容易。要捕获完整性错误，你只需以适当执行约束和见证生成程序的方式运行“诚实”的证明者即可。但是要捕获可靠性错误，你必须提出正确的恶意证明者来利用电路中欠约束的部分。模糊测试之类的方法可以对此有所帮助，但是在日常开发工作中进行模糊测试的开发者很少，有时利用缺失的约束需要比简单的模糊测试方法可以提供的更精心制作的见证。可以说，充分测试可靠性比完整性要难得多，这也使其成为应用形式化方法的理想领域。

迈向完美的约束

因此，希望你相信欠约束的电路错误对ZK系统构成了最大的安全威胁。我们如何才能真正证明我们没有此类错误？Veridise在一个早期的会议中给了我们一个非常令人信服的答案，当时我们正在考虑选择他们来审计R0VM 2.0.0的新电路。他们的审计员和Picus的发明者Shankara Pailoor参加了会议，并在审计甚至开始之前就掌握了两个欠约束的错误，他通过在电路代码上运行该工具自动发现了这些错误。不用说，我们选择了他们，并且我们一直在合作进行电路的“确定性的完整证明”。

那么Picus实际上是如何证明这一点的呢？在高层次上，该方法非常简单 - 它接受电路约束的表示形式，以及有关哪些变量是“输入”以及哪些是“输出”的信息。然后，使用静态分析和SMT求解的复杂组合，Picus尝试证明如果输入是确定性的，那么输出也是确定性的。静态分析可用于使用诸如“如果a是确定性的并且b是确定性的，则a + b也是确定性的”之类的规则来快速证明大量变量是确定性的。另一方面，SMT求解器对变量可以采用的可能值进行“穷举搜索”，使用花哨的搜索算法来快速缩小搜索空间。这两种方法之间存在权衡，因为静态分析速度很快，但往往会陷入困境而无法完成，而SMT求解器在找到解决方案（如果存在）时要好得多，但可能非常慢。将两者结合起来可以为我们提供两全其美的优势，并且证明对于大型电路的确定性至关重要。在分析结束时，Picus总是给出三种类型的答案之一：电路完全是确定性的，电路是非确定性的并提供了一个反例，或者证明花费的时间太长而放弃了。通过一些调整和关于特定电路的约束描述的提示，我们可以引导Picus进行证明或反例。

Keccak电路是确定性的！

通过与Veridise的合作，我们已经能够提取Keccak加速器电路的完整描述到Picus，并证明它是确定性的，达到了一些相对温和的假设。首先，我们需要定义Keccak电路的输入：这些是要哈希的数据（以非确定性方式读取），以及一个非确定性标志，指示是否还有更多数据要哈希。请注意，后一个假设是无害的 - 如果此“更多数据”标志过早地设置为false，则就好像其余输入根本没有发生一样，因此计算出的哈希只是截断数据的哈希。此外，对于所有电路，我们还将所有“公共输入”（与验证者共享的输入）作为Picus的输入：由于验证者知道这些值，因此它们是完全确定的。输出只是所有写入STARK跟踪并提交的值。因此，如果Picus证明该电路是确定性的，则意味着对于这些输入存在唯一的见证。

这里有一些复杂性：首先，完整的STARK跟踪由一系列“行”组成，每行都应用相同的约束集。对所有行重复相同的分析将是一种浪费，并且还需要我们为最终使用的所有跟踪长度重复证明。更糟糕的是，STARK跟踪“在旋转方面”是等效的，因此你实际上可以在表中间的某个任意行“开始计算”。此处的解决方案是使用特殊的CycleCounter组件来区分唯一的“循环0”（将在我们即将发布的白皮书中进行证明）。观察到循环0不引用跟踪的任何其他行，并且它本身是确定性的 - 这将成为归纳的基础情况。然后，对于所有后续行，假设跟踪中到循环0的所有先前行都是确定性的，并表明该行是确定性的。通过归纳，我们现在已经证明整个STARK跟踪是确定性的。这里的警告是，Picus不验证电路中的“backs”是否永远不会到达循环0之外（在独立验证的CycleCounter之外），但是通过观察最大后向距离为4，并且前4个循环从未使用超过循环0的后向来直接检查这一点。

最后一件事值得一提的是我们的“受信任代码假设” - 对于任何机器检查的证明，总是会有一段我们假设没有错误的运行的代码。就这项工作而言，我们当然取决于Picus和底层SMT求解器的正确性。我们还假设编译器从Zirgen到Picus的翻译是正确的。此外，Zirgen编译器有可能通过进行一些非法转换而在编译过程中引入欠约束的错误。对于最后一点，我们通过翻译Zirgen编译器的中间表示形式之一来缓解这种情况，而不是例如该语言的表面语法。这意味着我们加粗不需要加粗信任Zirgen编译器管道的正确性，直到我们翻译到Picus为止，但是我们需要信任之后的一切。为了说明，此图显示了Zirgen编译器管道；红色箭头表示必须信任的代码，以使确定性证明具有说服力，而绿色代码可以包含错误，而不会影响我们确定性证明的有效性。

这些“受信任代码假设”目前是证明中最薄弱的环节。但是，应该注意的是，信任编译器的正确性是在任何电路DSL之上进行构建的必要条件，而信任形式化方法工具的正确性是任何形式化方法工作的基础假设。将来，我们可以通过形式化验证到Picus的翻译并将Picus证明提取到另一个证明检查器（如Lean4）中来放宽这些假设，但这并没有阻止此验证工作贡献真正的价值 - 在发布之前，我们已经能够识别出电路中的许多真实的欠约束错误，并且Picus提出了一个令人信服的论点，表明我们已经找到了所有这些错误。这使我们对电路的正确性比以往任何时候都更有信心。最好的部分？它速度极快-重新运行证明以验证从87个Zirgen组件生成的超过45,000个Picus约束所花费的时间不到3分钟，这意味着我们可以检查每个未来的电路和编译器更改是否保留此安全属性。

2.0及以后

我们已经能够为我们的Keccak电路完成此证明，并且新的rv32im的工作进展顺利。这代表了我们形式化方法之旅中的第一个也是非常重要的里程碑，并且排除了zkVM的重要部分中最大的ZK安全错误类别。当我们继续进行完整验证时，我们将继续寻找高影响的方式，以使用形式化方法提供有意义的安全保证。

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