他山之石 | 如何用 ZK 可利用性证明重塑漏洞披露方式？

技术的突破是推动区块链行业前进的引擎，币安中国区块链研究院与链闻 ChainNews 同为密切关注区块链与密码学等领域技术发展前沿的组织，故而联合推出「他山之石」专栏，向中文世界读者介绍全球范围最值得关注的区块链技术进展，以及在金融等产业最新的应用分析与动态，以期为中国的区块链行业「攻玉」提供借鉴和思考。

本文引介一种零知识证明方式（ZK 可利用性证明），能够让企业精准地明确漏洞悬赏范围，让研究人员在不冒险进行公开披露情况下提交能证明其掌握了漏洞利用情况的证据。

原文标题：《【他山之石】使用零知识证明重塑漏洞披露方式》
撰文：Trail of Bits
本文已取得作者授权，并由链闻和币安中国区块链研究院获得中文地区翻译首发权

自 2012 年始，Trail of Bits 帮助全球最受瞩目的组织和产品进行安全防护。 他们将高端安全性研究与现实世界中的网络攻击者的思想相结合，以降低安全风险并强化代码。

目前，我们正在与约翰斯·霍普金斯大学（Johns Hopkins University）的 Matthew Green 教授共同研究通过零知识（ZK）证明创设一个可信可靠的环境，让科技企业和漏洞研究人员能够在这样的环境中无后顾之忧地沟通交流。在未来四年中，我们将推动 ZK 证明从理论走向实践，并面向漏洞研究人员提供可得出 ZK 可利用性证明的软件。此项研究隶属于美国国防部高级研究计划局（DARPA）所资助的加密验证和评估信息安全（SIEVE）项目。

近年来，ZK 研究主要集中在区块链应用领域，其中参与方需要证明其交易符合公认的底层规则。而我们的研究则大幅拓宽了 ZK 可证明的语句种类。该项目结束后，用户将能够验证 x86 处理器程序的相关语句。

为什么是 ZK 可利用性证明

就 bug 的发现和报告，软件开发者和漏洞研究人员无法达成一致。披露过多的漏洞信息会中伤第三方研究人员的收益，而披露过早则会对软件厂商的信誉造成永久的损失。各方之间的沟通往往以失败告终，同时技术产业的损失也十分惨重。

而且，在很多时候，企业不愿意接触安全团队，也不会理睬用户隐私所面临的潜在威胁。在这样的情况下，漏洞研究人员的处境十分艰难：要么在知道用户面临风险的情况下保持沉默，要么公开披露漏洞，迫使企业做出行动。如果选择了后者，研究人员则将漏洞利用路径告诉了攻击者，亲手把用户放到了砧板之上。

ZK 可利用性证明将彻底颠覆了漏洞的披露方式，能够让企业能够精准地明确 bug 悬赏范围，让研究人员在不冒险进行公开披露情况下提交能明确证明其掌握了漏洞利用情况的证明。

设计 ZK 证明

通过 ZK 证明，验证人能够让校验人相信自己持有一段信息，同时不需要暴露信息本身。例如，Alice 希望让 Bob 相信自己知道了某个值 Y 的 SHA256 预映射 X，但是并不需要告诉 Bob X 具体是什么。（或许 X 是 Alice 的密码）。ZK 证明最知名的工业应用或许是在 ZCash 等注重隐私保护的区块链领域，在此领域，用户在提交交易时，希望自己的身份、接收人的身份、交易金额都能保持匿名。为此，他们需要提交一个 ZK 证明，证明其交易符合区块链规则，并且发送者具有足够的资金。（请阅读 Matt Green 的文章了解 ZK 证明及相关示例。）

现在你已经知道了 ZK 证明的用处，但是这些算法是如何开发的呢？需要权衡哪些利弊呢？关于高效系统的开发，有三大衡量指标：验证时间（prover time）、校验时间（verifier time）和带宽（bandwidth）（即一方必须通过协议向另一方发送的数据量）。某些 ZK 证明不需要验证人与校验人进行交互，在此情况下，带宽仅是证明的大小。

接着，我们谈一谈目前的难点以及影响 ZK 证明投入实践的主要障碍。大多数传统的 ZK 协议要求底层语句必须首先用布尔电路（Boolean circuit）或无循环的运算电路（即组合电路）来表示。对于布尔电路，可以用 AND 门、NOT 门和 XOR 门，而对于运算电路，可以用 ADD 门和 MULT 门可以想象，要想把一个要证明的语句转换成这样的电路并不容易，如果还没有简洁的数学公式，更是难上加难。例如，如果一个程序包含循环行为，那么在电路生成之前，必须先把它展开，而当程序包含数据依赖型循环时，那就无法展开了。

布尔电路与运算电路示例

另外，电路尺寸也会影响到 ZK 协议的效率。一般情况下，验证时间与电路尺寸至少呈线性关系（通常，各个门的开销通常很大且恒定）。因此，在漏洞披露时，ZK 证明需要底层漏洞能被尺寸合适的电路捕捉到。

证明可利用性

由于 ZK 证明一般会接收写成布尔电路的语句，因此，这里的难点在于需要布尔电路仅在漏洞利用成功时返回「true」，以此表示存在漏洞利用。

我们希望当验证人向程序中导入会造成漏洞利用的输入时，电路能够接收（accept），例如：能够让攻击者取得程序执行权限的缓冲区溢出（buffer overflow）。由于大多数二进制漏洞利用针对的是二进制（binary）和特定的处理器，因此，我们的电路必须准确地对程序的目标编译架构进行建模。最后，当程序成功运行时，以及当漏洞利用在执行过程中被触发时，我们需要一个电路来接收。

初级的方法是开发一个电路来代表目标建模处理器的「一步」（one step）。接着，我们根据要执行的程序，将容纳该程序的内存初始化；按照程序的启动时间，设置程序计数器；验证人使程序运行在自己的恶意输入上——重复处理器电路，直至程序结束，检查每一步是否均满足了漏洞利用条件。也就是说检查程序计数器是否被设置成了一个已知的「恶意」（bad）值，或被写入了一个有权限的内存地址。关于此策略的重要注意事项：在每一步均需要完整运行整个处理器电路（即便实际上只有一条指令在运行），因为单独列出一项功能会泄露相关的跟踪信息。

不幸的是，这种方法会导致电路过大，因为程序执行的每一步都需要有一个电路对核心处理器逻辑及整个 RAM 进行建模。即便我们把 RAM 限制成 50 MB，对于一次漏洞利用，如果其跟踪使用了 100 条指令，那么产生一条相应的 ZK 语句会导致电路至少达到 5GB。这种方法效率太低，无法用于有意义的程序。关键问题在于电路尺寸与跟踪长度和 RAM 大小成线性关系。为了解决这个问题，我们采用了 SNARKs for C 的方法，即把程序执行证明分为两部分，一部分为核心逻辑，另一部分为内存正确性。

要证明逻辑有效性，必须将处理器电路应用于程序跟踪中连续的每一对指令（sequential pair of instructions）。该电路可以验证一个寄存器状态能否合法地跟随另一寄存器状态。如果每一对状态均有效，则电路接收。不过要注意，这里的前提是内存操作是正确的。如果转移函数电路中存在一个存储器检查器，则会产生开销，此开销与所使用的 RAM 大小成比例。

无内存检查处理器执行有效性

让验证人也输入一个内存排序的执行跟踪，就能进行内存验证。如果第一个内存地址访问了一个低于第二个内存地址的内存地址（破坏了时间戳（timestamp）关系），那么这个跟踪就会在另一个跟踪之前放置一条跟踪记录。这个跟踪能让我们线性地扫描内存排序指令，确保内存访问的一致性。此方法无需根据 RAM 大小创建相应尺寸的电路。不过，该电路与跟踪尺寸呈线性关系，并且仅能执行基础的相等性检查（equality check），不能明确地记录每一步下的完整 RAM。

检查内存排序跟踪

最后一个要解决的问题是，验证人不受阻挠地使用与最初情况不符并且无法创建假证明的内存排序跟踪。要解决此问题，我们必须添加一个「排列检查器」（permutation checker）电路来验证我们是否确实根据内存位置对程序跟踪进行了排序。欲进一步了解相关讨论，请参见 SNARKs for C 论文。

建模 x86

知道了如何证明 ZK 中存在漏洞利用，接下来我们需要把相关的处理器架构建模成布尔电路。此前已经有人对 TinyRAM 进行了建模，这是一种 RISC 架构，其目标是在 ZK 环境中高效运行。不幸的是，TinyRAM 并未商用，而且由于漏洞利用大多依赖特定于架构的行为，因此 TinyRAM 不能为现实程序提供 ZK 可利用性证明。

我们接下来将通过建模一种相对简单且应用广泛的微处理器——MSP430 进行建模，以开发 ZK 可利用性证明，这种简单的芯片被广泛应用于各种嵌入式系统。另外，Microcorruption CTF 系统也是基于 MSP430 运行。我们的首要目标是针对 Microcorruption 受到的每一次挑战提供 ZK 证明。在完成此「可行性演示」后，我们会转向 x86。

从简单的 RISC 架构过渡到复杂的 CISC 架构，随之而来的是各种复杂问题。对于 RISC 处理器的电路模型，每周期的时钟门为 1 至 10k。另一方面，如果我们的 x86 处理器达到 10 万门级别，那么对于需要 10000 条指令才能完成的漏洞利用，ZK 证明会达到 48 GB。由于 x86 比 MSP430 复杂了几个数量级，因此即便把逻辑证明和存储器正确性证明分开，也无法天真地将其功能实现为布尔电路。

我们的解决方案基于一个显而易见的事实，即没有程序能完全用尽 x86。一个程序在理论上能用到 x86 所支持的全部 3000 条指令，但实际上，大多程序只用到了几百条。我们会使用程序分析技术来判断特定二进制所需的 x86 最小子集，并动态地生成能够验证其正确执行能力的处理器模型。

当然，我们无法支持部分 x86 指令，因为这些指令实现了数据依赖型循环。例如，repz 会重复后续指令，直至 rcx 为 0。对于这样的指令，只有在运行时才能确定其实际行为，而我们的处理器电路必须是组合电路，因此无法支持此类指令。为了处理这些指令，我们会把一个静态二进制转换器（binary translator）从普通 x86 转成特定于我们程序的 x86 子集。这样的话，我们就能够处理最复杂的 x86 指令，而无需将其硬编码到我们的处理器电路中。

新型的 bug 披露模式

能够与约翰斯·霍普金斯大学以及 DARPA SIEVE 项目的同仁共同启动这项工作，我们倍感兴奋。我们希望得到能够从根本上颠覆漏洞披露方式的工具，以便企业能够明确其 bug 悬赏范围，漏洞研究人员可以安全地提交能明确证明其掌握了漏洞利用情况的证明。而且，我们还希望 ZK 漏洞披露能成为消费者的保护伞。研究人员可以在不公布相关漏洞的情况下，警告用户特定设备存在潜在危险，这么做是在向企业施压，逼迫他们解决本不愿解决的问题。

更广泛地说，我们想把 ZK 证明从学术界带入产业界，使其更贴近当今的软件、更实际。关于此技术，若您有特定用途且未在本文中未提及，我们欢迎您来函。关于 ZK 证明方案与电路编译器的复杂生态系统，我们积累了相应的专业知识，可为您提供帮助！

在此我们要特别感谢 Colleen Swanson 和 Marcella Hastings，感谢他们的校对工作，以及他们关于本文的宝贵反馈。

来源链接：blog.trailofbits.com

—-

编译者/作者：币安研究院

玩币族申明：玩币族作为开放的资讯翻译/分享平台，所提供的所有资讯仅代表作者个人观点，与玩币族平台立场无关，且不构成任何投资理财建议。文章版权归原作者所有。