文章探讨了以太坊协议中引入zkEVMs后,在安全性方面面临的18个潜在问题,涉及网络组成、多样性、Guest Program、Proving以及工程堆栈等多个层面。文章强调了通过多样性、严格测试、形式化验证以及审计等手段来应对这些安全挑战的重要性,旨在提升以太坊zkEVMs的整体安全性。
一个拟议的协议变更邀请新的实体,Provers,在密码学 VM 内部执行 EVM,生成由 attesters 检查的证明。与它们所证明的交易相比,这些证明非常小,并且 attesters 不需要接收所有的状态更新,因此对 attesters 的网络要求仍然很低。此外,与重新执行一个区块中的所有交易相比,检查一个证明的工作量非常小,因此 attesters 可以运行在适度的硬件上。
本文着眼于与此升级的安全性相关的十八个问题,特别关注 zkVM 的安全性以及它们将执行的软件。它旨在展示我们在追求整体安全性时所做的权衡,同时也提出了许多具体的缓解措施。zkEVM 安全工作组将定期会面讨论这些问题。你可以在 以太坊研发 Discord 上关注我们的进展。
我们使用以下术语和缩写:
目前,为了检查区块的有效性,节点执行 STF 的实现。在变更之后,节点将乐观地等待 STF 执行的证明。
在 zkEVM 之前:
使用 zkEVM:
zkEVM 实现的多样性将是安全性的一个关键组成部分。这种多样性应该是 zkVM provers 和 STF 实现的多样性。如果 CL 客户端在验证了几个不同的 zkEVM 证明(涵盖了 EL 实现和 zkVM 的多样性)之后才接受一个区块,那么安全性将比只有一个证明时要高得多。我们称之为“多重证明”策略。Kev Wedderburn 即将发表的一篇文章将进一步探讨这个话题。
zkEVM 形式化验证项目的目标是形式化验证 zkEVM 的一些组件。目标包括在理论上验证某些 zkSNARK 协议 的安全性,验证虚拟机实现与这些机器(EVM 和 RISC-V)的形式化规范的符合性。这些技术非常强大,但开发速度可能很慢,作者不认为形式化验证应该是使用 zkEVM 扩展 L1 的障碍。
术语“zk”通常被滥用,用来指代那些仅仅提供 SNARK 证明(zkVM、zk 证明等),而没有零知识属性的系统。这些系统对于扩展来说已经足够好,但读者应该知道,这些证明不提供隐私保证,而隐私保证会增加额外的复杂性和 prover 的工作量。
在本文的剩余部分,我们将深入研究系统安全性的几个方面,以及它们如何随着 zkEVM 的出现而改变。每个方面都被赋予一个主观的衡量标准,“关注程度”,这是作者对由于这个因素而可能造成的严重漏洞的粗略看法。当然,意见差异很大,这里的意见不一定反映审查过这篇文章的人的意见。
改变协议以依赖于一类新的、未指明的参与者,provers,引发了关于去中心化和激励对齐的问题,特别是由于在家进行证明的基础设施,在典型情况下,将花费数万美元,并且需要电力升级(至少在 2025 年的情况是这样)。我们在这里不讨论这个重要的话题。作为一个有用的起点,我们推荐 ZKEVM Book。
目前,https://clientdiversity.org/ 显示有三个客户端的市场份额超过 10%,五个客户端的市场份额超过 1%。如果在 zkEVM 的世界里,只有一两个客户在速度和成本方面具有竞争力,那么客户多样性将会恶化。应该注意的是,上面列表中未包含的新客户端,例如 Ethrex,可能会由于它们对 zk 证明的适应性而获得关注(正如我们将看到的,Rust 在这方面具有有利的权衡)。虽然用未经充分测试的客户端替换经过实战考验的客户端池会降低安全性,但当然,新客户端有可能从长远来看改善多样性指标。
关注程度:中等
这是一个严重的潜在问题,但有一批核心的 EL 开发者希望看到他们的工作成果投入生产。
缓解措施:多样性可以在多重证明策略的层面上强制执行。这要求 RTP 为多个不同的 STF 产生及时的证明,这使得扩展更加困难,但也更加安全。
正如我们努力实现 STF 实现的多样性一样,我们也在努力实现 zkVM 的多样性。事实上,我们还应该努力实现所有这些软件依赖项的多样性。值得注意的是,如果所有正在使用的 zkVM 都依赖于一个单独的 SNARK 库来构建证明,那将是冒险的。
关注程度:中等 有许多团队致力于提供安全的以太坊 L1 扩展,预计来年将有更多项目从隐身模式中走出来。此外,这些团队看到了以太坊之外的机会,例如在可证明的 AI 推理中。总而言之,我们应该有信心会有一个强大的 zkVM 生态系统。
缓解措施:同样,多重证明策略是关键。验证者应该只在验证了几个证明(涵盖了一系列 zkVM+STF 组合)之后才接受区块。此外,还应该跟踪对共享故障点的分析,包括至少用于构建 zkVM 的 SNARK 库和其他密码学原语,如果发现任何关键的单点故障,就应该分散风险。
EL 客户端已经在生产环境中运行了多年,成功地支持了以太坊上价值数十亿美元的经济活动,并使网络发展到全球重要性。对 EL 客户端进行重大更改以支持证明会增加其核心逻辑中出现严重 bug 的可能性。
关注程度:中低 EL 客户端团队的经验,加上广泛的 EEST 测试框架,使我们有信心根据需要进行重构以进行证明。
缓解措施:各团队应注意避免不必要的代码更改,并保持甚至扩大测试范围。形式化验证编译后的 guest program 与 EVM 规范相匹配(正在进行中),将增加我们在更改 STF 实现时的信心。
现有的 EL 客户端被设计为在最常见的操作系统中的传统 CPU 上运行。在这种设置下,编译器可以自由地发出大量指令和 syscall。正如它们现在存在的那样,zkVM 受到极大的约束(即,它们仅支持传统程序中的指令和 syscall 的子集)。这给编译一些语言以在 zkVM 中执行带来了困难。
在此处列出的 EL 客户端中,只有 Reth 是用 Rust 编写的,Rust 是一种对编译成由多个 zkVM 支持的最小目标 ISA、称为 RV32IM 的 RISC-V ISA 提供官方支持的语言。对于使用 Go 编写的客户端,支持编译为可以由 Ziren 证明的 MIPS。还支持 RISC-V rva20u64 profile,它使用了一组相当复杂的扩展,比 RV32IM 大得多。对于给定的 guest program,可能只需要支持这些指令的子集,但不能保证该子集在依赖项或编译器升级时会保持稳定。对于其他托管语言的客户端,也会出现类似的考虑因素。
最近几个月,对其他 ISA 的支持有所增加,Jolt 升级到 RV64IMAC,Zisk 升级到 RV64IMAFDCZicsr 的轻度不符合标准的子集。对 rva20u64 等的广泛支持感觉还很遥远。
类似地,存在对 guest program 中 Linux syscall 的支持问题。在最近的客户端互操作性事件中,出席的 zkVM 团队之间达成了宽松的共识,即围绕 Linux syscall 进行标准化,例如,分配 guest 内存,但尚未写下对该承诺的正式描述。请注意,有很多 Linux syscall,但只需要支持其中一些。
有人 建议 以 rv64im-unknown-none-elf 目标作为最小基线进行标准化。Geth 团队拒绝了该提议,理由是 zkVM 应该支持其他扩展,以支持对 Go 和其他托管语言的证明。目前正在进行有关此方面的研究。
关注程度:高 在 zkVM 中支持大型目标需要以下某种组合:
缓解措施:在安全性的不同方面之间取得平衡是 zkEVM 项目的核心关注点。我们根据以上几点address这个问题。
同样的考虑因素适用于对 Linux syscall 的部分支持问题。
Rust 定义了 目标层级 来描述在发布编译器之前将对该目标进行的测试级别。 简而言之:
Rust 对 RV32IM 的支持仅为Layer2,而 RV64GC 是Layer2“带有主机工具”(但此目标会发出 Linux syscall)。针对 RISC-V 64 位目标的 Rust 测试的 CI 运行示例 此处。
相比之下,Go 似乎对 RISC-V 进行了强大的测试。例如,在 此 Go CI 仪表板 上,可以找到 此 RISC-V 目标的 CI 失败,其中 61836 个测试中有 127 个失败。不幸的是,Go 对发出的 RISC-V 代码的控制要少得多, (目前)可以使用相当大的扩展集、Linux syscall,并且不提供内置的浮点模拟。
关于 C++ 编译器,GCC 对 RISC-V 没有更高层的支持,尽管它支持 MIPS。Clang 确实测试了 RISC-V,例如,它似乎在 此处 运行了超过 6000 个 RISC-V 特定的单元测试。但是,与 Go 编译器一样,仅涵盖了大型目标 ISA。
The RISE Project 正在寻求改进编译器测试和对 RISC-V 目标的支持。我们参考他们的博客以获取有关支持 Rust 和 Go 的信息。
关注程度:高 编译器是本项目中高度复杂的黑盒。对这些测试的任何不足意味着 zkVM 可以生成在所有输入下都不共享 STF 语义的二进制文件。这显然可能非常糟糕,因为 attesters 然后实际上不会验证以太坊状态转换的证明,而是验证一些相关但略有不同的状态转换的证明。对于一个特定的例子,请参见 Certora 的这篇博文,该博文在 Argument 的此有用概述 中提到。
缓解措施:
像 Valida 这样的项目引入了专为高效证明而设计的定制 ISA。这意味着使用无法从最著名的编译器收到的广泛测试和审查中受益的编译器。
关注程度:中高
一方面,LLVM 堆栈有很多关注者。另一方面,它非常复杂,并且经常在其中发现错误。尽管如此,总的来说,使用标准编译器感觉更安全,至少因为在其中任何一个出现严重错误时,人们可以切换编译器(例如,在 GCC 和 Clang 之间)。
缓解措施:彻底的测试和审计。如果编译器足够简单和稳定,那么随着“在野外”的时间流逝,我们可以对其安全性更有信心。
由于算术电路执行的成本模型与在传统二进制计算机上执行的成本模型根本不同,因此 zkVM 引入了 ZkVM 预编译来优化困难情况(如 Keccak 哈希)的证明。长期以来,传统的 EVM 预编译一直是简化的目标,以提高以太坊的安全性。虽然 zkVM 预编译在实践中通常与现有的 EVM 预编译相关,但它们是一个不同的概念。当我们追求 L1 扩展时,zkVM 预编译也可能比传统的预编译更难消除,因为这种追求会产生优化执行速度和成本的巨大压力。请注意,在 EVM 预编译的情况下,执行环境是一件商品硬件,而在 ZkVM 情况下,执行环境是一个更容易定制的虚拟环境。人们可以自定义该环境的相对容易程度往往会增加复合系统的攻击面。
关注程度:中高
这些预编译往往很复杂。
缓解措施:prover 激励机制,与维护甚至预编译的扩散更加一致。 一些可以提供帮助的事情是:
每个 zkVM 都实现了一个自定义 VM 模拟器来执行给定的程序。如果模拟器有 bug,那么在模拟下游完成的证明将不能证明 EVM 语义已得到忠实遵循。
关注程度:中高
缓解措施:存在全面的测试套件来测试 RISC-V 模拟器的合规性。这些正在 zkEVM 团队的 zkEVM 测试监视器 中运行。应每晚进行额外 ISA 的合规性测试并以类似方式进行跟踪。准备就绪后,形式化验证将提供更大的正确性保证。
每个 zkVM 库的核心都是使用算术电路实现机器规范。需要该机器实现正确的语义。否则,证明在给定了 STF 和一组输入和输出之后,它已正确执行,并不意味着状态转换在符合以太坊协议规范的意义上是有效的。
关注程度:高
缓解措施:对基本电路进行详尽的单元测试至关重要。彻底的审核和引人注目的漏洞赏金至关重要。已证明模糊测试在发现电路错误方面是有效的。请参阅 Hochrainer、Isychev、Wüstholz 和 Christakis 的工作,他们已经在 R0VM、Noir 和其他 zkSNARK 软件中发现了重大错误。
zkEVM 的最终期望属性是它完全约束 prover 来描述有效的状态转换。虽然出于安全目的,采用模块化方法很有用,但强调对整个管道进行压力测试也很重要。
关注程度:高 这是一个包含许多其他问题的元问题。
缓解措施:应证明所有 EEST 测试用例,而不仅仅是这些测试用例的子集。如前所述,形式化验证最终将提供强大的保证,直至证明系统使用编译器的 guest program。
zkVM 将输入二进制文件转换为适合证明的表示形式。在某些情况下,这与 RISC-V 本身非常忠实,而在其他情况下,这引入了程序员或审计员必须理解的另一个低级抽象。在某些情况下,这样做是出于性能原因,特别是关于这些程序的模拟。如果转译步骤有 bug,例如,它以静默方式 NOPs 指令块,那么该程序部分的 witness 生成(参见下文)是没有意义的。
关注程度:中等
缓解措施:彻底、明确的文档,理想情况下以涵盖成功和失败案例的单元测试的形式呈现,可以帮助工程师避免错误,并且可以帮助审计员发现错误。
除了为给定的一组输入生成客户端执行的完整跟踪,并可能将其转译为适合证明的内部表示形式外,zkVM 还必须生成完整的 witness 以进行证明。这是一种更细粒度的执行跟踪生成,例如,可以为查找参数或约束生成数据,从而粘合链接程序不同部分的约束。如果 witness 生成不正确,即使对于正确的算术电路,系统也可能会错误地拒绝有效的交易,或错误地接受无效的交易。
关注程度:高 请注意,这与 circuit 正确性密切相关。
缓解措施:类似于 circuit 正确性。最好编写许多失败测试,例如,检查提供专门制作的恶意 witness 是否导致未通过验证的证明。可以从 0xPARC 和 zkSecurity 维护的 bug 跟踪器中的示例开始。
即使在经过充分研究的论文中,包括著名的 ZCash 错误(参见 BCTV 的第 25 页),也会在发表多年后被世界顶级 zk 证明专家发现。对于更新且不太知名的协议,出现 bug 的可能性可能更高。
关注程度:中等
缓解措施:在实现不太知名的论文中描述的系统时,实现团队及其审计员应审查该论文,并可能寻求理论专家的指导和意见。形式化验证将在此处提供很大的帮助 - 它需要对协议进行深入的重写,然后将正确性语句(例如协议的完整性和可靠性)简化为某些基本公理。
著名的 Frozen Heart Vulernability 在某些情况下可以归因于论文不清楚要哈希哪些数据才能正确实现 Fiat-Shamir 转换,而 Fiat-Shamir 转换是 zkEVM 的普遍组成部分。有人可能会争辩说这是一个协议错误,但更准确的说法是将其归因于理论和实现之间的差距。
关注程度:中等
缓解措施:彻底的规范和深入的审计。
论文中编写的协议可能与团队打算实施的协议不同。例如,可能会添加或修改多项式承诺的批处理,或者可能会错误地将需要更多 prover-verifier 交互的其他步骤融合到其他步骤中。另一种不太令人担忧的差异是,关于 SNARK 协议的论文通常会修复一个简单的算术化,例如 R1CS 或 PlonK 中的“vanilla”Madd 门。对于能够实时证明以太坊的生产级系统,需要更复杂的设置。在实践中,此组件是相当模块化的,并且对协议的安全性没有太大的影响(但是这 对于 zkEVM 的语义正确性来说是一个很大的问题!)。
关注程度:高 优化这些系统的动机很强。攻击可能允许构造恶意负载,从而损害网络或导致接受无效的交易。
缓解措施:应编写精确、清晰的协议规范,最好在实施之前编写。这些应保持最新。审计员应阅读这些规范,并确保“基本”协议的安全证明确实在修改后被延续。这也应通过形式化验证来覆盖 - 应指定 已实施的 协议。
如果 SNARK 协议的实现与正确的规范不符,那么即使验证者接受证明为有效,也不清楚这暗示着什么。
关注程度:中等 潜在影响很高,但审核侧重于此类问题,应能解决此问题。
缓解措施:代码的清晰性、代码中的正确注释,以及最好的是,将代码的各个部分与规范显式链接起来,所有这些都意味着可以检查规范。这种缓解措施的最极端和最强大的版本是形式化验证。测试(包括失败案例)对此有所帮助。
任何密码学协议的安全性都取决于计算难度假设。zkVM 依赖于各种假设以及安全参数的正确设置。此类参数可以包括椭圆曲线、格参数和哈希函数的选择。一个突出的安全参数是在证明“邻近证明”期间执行的查询轮数,而“邻近证明”是最广泛使用的多项式承诺方案的核心。在这种设置中,已知如何安全地设置查询数(例如,实现 128 位的安全性),但 推测 大约一半的查询实际上会提供此级别的安全性。Arantxa Zapico 即将发布的一篇 ethresear.ch 帖子将详细介绍这些问题。如果这些推测被证明是不正确的,那么使用该协议的 zkEVM 实际上会比人们认为的更容易受到暴力攻击,从而允许 prover 找到可能导致错误接受证明的恶意输入。
关注程度:中等 此处的目的是通过威慑实现安全。潜在影响很高,但是除非社区标准显着下降或安全分析存在巨大差距,否则与对代码的更普通的攻击相比,可利用性较低。
缓解措施:密码学家的审核至关重要。明智的做法是实施并定期测试使用已被证明是安全的或具有更长的“在野外”使用记录的参数的后备系统。
对于安全来说,zkVM 以 Rust 等更安全的语言编写是件好事,但是使用不安全的 Rust 会大大削弱这一点。不安全的代码主要出于性能原因而出现,要么是优化 Rust,要么是调用 C、C++ 或 CUDA。Bug 往往源于复杂性,因此将默认设置为不安全语言用于最复杂、最低级别的代码会大大削弱使用安全语言的价值。
关注程度:中高
缓解措施:尽可能减少不安全代码的数量。定期并在任何发布之抢跑 sanitizers。对崩溃进行模糊测试也对此有所帮助。
zkEVM 依赖于通常被称为“疯狂数学”的东西。虽然这些系统确实代表了密码学的最前沿,但确保这些系统的安全性将归结为几个简单的想法。 其中一个想法是通过多样性来分散风险,验证者不仅要验证一个证明,还要验证多个证明,目的是最大限度地减少共享的 zkEVM 依赖项的数量。彻底的测试至关重要。维护和符合正式规范,无论是加密协议还是虚拟机,对于推理系统都是必要的。诸如审计和模糊测试之类的错误查找技术,多年来已被许多不同的安全公司成功部署。从长远来看,对 zkEVM 的部分进行形式化验证将为我们提供更高程度的安全性,甚至可能使我们有信心更快地增长。
- 原文链接: zkevm.ethereum.foundatio...
- 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!