使用零知识证明重新定义漏洞披露 - Trail of Bits博客

Trail of Bits博客
使用零知识证明重新定义漏洞披露
Trail of Bits
2020年5月21日
密码学、DARPA、新闻发布、零知识证明

我们与约翰斯·霍普金斯大学的合作伙伴Matthew Green正在使用零知识（ZK）证明来建立一个可信的环境，使科技公司和漏洞研究人员能够合理沟通，而不用担心被破坏或嘲笑。在接下来的四年里，我们将推动ZK证明的技术水平超越理论，为漏洞研究人员提供能够生成可利用性ZK证明的软件。这项研究是DARPA计划"加密验证与评估信息安全"（SIEVE）资助的更大努力的一部分。

近期许多ZK工作集中在区块链应用上，参与者必须向网络证明他们的交易遵循底层共识规则。我们的工作将大幅扩展ZK中可证明陈述的类型。到项目结束时，用户将能够证明关于在x86处理器上运行的程序的陈述。

为什么需要可利用性的ZK证明？

软件制造商和漏洞研究人员在发现和报告漏洞方面存在着紧张的关系。披露过多关于漏洞的信息可能会破坏第三方研究人员的奖励，而过早披露漏洞可能会永久损害软件公司的声誉。这些各方之间的沟通经常破裂，技术行业因此受到影响。

此外，在许多情况下，公司不愿意与安全团队合作，并对用户隐私的潜在危险置之不理。在这些情况下，漏洞研究人员陷入困境：尽管知道用户面临风险却保持沉默，或者公开披露漏洞以迫使公司采取行动。在后一种情况下，研究人员通过告知攻击者潜在的利用路径，可能使用户陷入危险。

可利用性的ZK证明将彻底改变漏洞的披露方式，使公司能够精确定义漏洞赏金范围，研究人员能够明确证明他们拥有有效的漏洞利用方法，而无需冒公开披露的风险。

设计ZK证明

在ZK证明中，证明者使验证者相信他们拥有某条信息，而不透露信息本身。例如，Alice可能想说服Bob她知道某个值Y的SHA256原像X，而不实际告诉Bob X是什么。（也许X是Alice的密码）。也许ZK证明最著名的工业应用是在像Zcash这样的隐私保护区块链中，用户希望提交交易而不透露其身份、接收者身份或发送金额。为此，他们提交一个ZK证明，表明交易遵循区块链的规则，并且发送者有足够的资金。（查看Matt Green的博客文章，了解带有示例的ZK证明的良好介绍。）

现在您知道ZK证明为什么有用，但这些算法是如何开发的，需要评估哪些权衡？开发高效系统需要考虑三个指标：证明者时间、验证者时间和带宽，即各方在整个协议中必须发送给对方的数据量。一些ZK证明不需要证明者和验证者之间的交互，在这种情况下，带宽就是证明的大小。

现在是困难的部分，也是阻止ZK证明在实际中使用的主要障碍。许多经典的ZK协议要求底层陈述首先表示为没有循环的布尔或算术电路（即组合电路）。对于布尔电路，我们可以使用AND、NOT和XOR门，而算术电路使用ADD和MULT门。正如您可能想象的那样，将您希望证明的陈述转换为这样的电路可能具有挑战性，如果该问题没有清晰的数学表述，则尤其具有挑战性。例如，任何具有循环行为的程序在电路生成之前必须被展开，当程序包含数据依赖循环时，这通常是不可能的。

布尔和算术电路示例

此外，电路大小对ZK协议的效率有影响。证明者时间通常与电路大小至少呈线性关系（通常每个门有较大的常数开销）。因此，漏洞披露中的ZK证明要求底层漏洞利用能够被合理大小的电路捕获。

证明可利用性

由于ZK证明通常接受写为布尔电路的陈述，挑战在于通过将漏洞利用表示为仅在漏洞利用成功时返回"true"的布尔电路来证明漏洞利用的存在。

我们想要一个电路，当证明者对程序有某些输入导致漏洞利用时接受，例如导致攻击者获得程序执行控制的缓冲区溢出。由于大多数二进制漏洞利用既特定于二进制文件也特定于处理器，我们的电路必须准确模拟程序编译到的任何架构。最终，我们需要一个电路，在程序成功运行且在执行过程中触发漏洞利用时接受。

采用一种简单的方法，我们将开发一个代表我们想要模拟的任何处理器的"一步"的电路。然后，我们将初始化内存以包含我们想要执行的程序，将程序计数器设置到我们希望程序执行开始的任何地方，并让证明者在他们的恶意输入上运行程序——即，只需重复处理器电路直到程序完成，并在每一步检查是否满足漏洞利用条件。这可能意味着检查程序计数器是否设置为已知的"坏"值，或者是否写入了特权内存地址。关于此策略的一个重要警告：整个处理器电路需要在每一步运行（即使实际上只执行一条指令），因为挑出某一块功能会泄露关于轨迹的信息。

不幸的是，这种方法将产生不合理的大电路，因为程序执行的每一步都需要一个模拟核心处理器逻辑和整个RAM的电路。即使我们将自己限制在具有50 MB RAM的机器上，生成关于轨迹使用100条指令的漏洞利用的ZK陈述也会使电路至少为5 GB。这种方法对于有意义的程序来说效率太低。关键问题是电路大小随轨迹长度和RAM大小线性扩展。为了解决这个问题，我们遵循C语言的SNARKs方法，将程序执行证明分为两部分，一部分用于核心逻辑，另一部分用于内存正确性。

为了证明逻辑有效性，处理器电路必须应用于程序轨迹中的每个顺序指令对。电路可以验证一个寄存器状态是否可以合法地跟随另一个。如果每对状态都有效，则电路接受。但请注意，内存操作被假定为正确。如果转换函数电路包含内存检查器，它将产生与所用RAM大小成比例的开销。

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

可以通过让证明者也输入一个内存排序的执行轨迹来验证内存。如果第一个访问的内存地址比第二个低（时间戳打破平局），则此轨迹将一个轨迹条目放在另一个之前。这个轨迹让我们可以对内存排序的指令进行线性扫描，并确保一致的内存访问。这种方法避免了创建大小与所用RAM量成比例的电路。相反，这个电路在轨迹大小上是线性的，并且只执行基本的相等性检查，而不是在每一步显式写下整个RAM。

检查内存排序的轨迹

我们需要解决的最终问题是，没有什么能阻止证明者使用与原始轨迹不对应的内存排序轨迹并创建虚假证明。为了解决这个问题，我们必须添加一个"排列检查器"电路，验证我们实际上已按内存位置对程序轨迹进行了排序。更多关于此的讨论可以在C语言的SNARKs论文中找到。

建模x86

既然我们知道如何在ZK中证明漏洞利用，我们需要将相关的处理器架构建模为布尔电路。先前的工作已经为名为TinyRAM的RISC架构完成了这一点，该架构设计为在ZK上下文中高效运行。不幸的是，TinyRAM未在商业应用中使用，因此对于在真实世界程序中提供可利用性的ZK证明不现实，因为许多漏洞利用依赖于架构特定的行为。

我们将通过建模一个广泛使用的相对简单的微处理器来开始我们可利用性ZK证明的开发：MSP430，一种在各种嵌入式系统中发现的简单芯片。作为额外的奖励，MSP430也是Microcorruption CTF运行的系统。我们的第一个主要目标是为每个Microcorruption挑战生成ZK证明。完成这个"可行性演示"后，我们将把目光投向x86。

从简单的RISC架构转向 notoriously复杂的CISC机器带来许多复杂性。RISC处理器的电路模型每周期在1-10k门之间。另一方面，如果我们的x86处理器结果包含大约100k门，那么一个需要10,000条指令完成的漏洞利用的ZK证明将产生大小为48千兆字节的证明。由于x86比MSP430复杂几个数量级，天真地将其功能实现为布尔电路将不切实际，即使在分离逻辑和内存正确性证明之后。

我们的解决方案是利用一个有些明显的事实：没有程序使用x86的全部功能。理论上，程序可能使用x86支持的所有大约3,000条指令，但实际上，大多数只使用几百条。我们将使用程序分析技术来确定给定二进制文件所需的最小x86子集，并动态生成能够验证其正确执行的处理器模型。

当然，有一些x86指令我们无法支持，因为一些x86指令实现数据依赖循环。例如，repz重复后续指令直到rcx为0。此类指令的实际行为在运行时之前无法确定，因此我们无法在处理器电路中支持它，该电路必须是组合电路。为了处理此类指令，我们将生成一个从普通x86到我们程序特定x86子集的静态二进制翻译器。这样，我们可以处理最复杂的x86指令，而无需将它们硬编码到我们的处理器电路中。

新的漏洞披露范式

我们非常兴奋能与约翰斯霍普金斯大学以及参与DARPA SIEVE计划的同事开始这项工作。我们想要生产工具，彻底改变漏洞的披露方式，使公司能够精确指定其漏洞赏金的范围，漏洞研究人员能够安全地提交明确证明他们拥有有效漏洞利用的证明。我们还预计，漏洞的ZK披露可以作为一种消费者保护机制。研究人员可以警告用户给定设备的潜在危险，而不公开该漏洞，这给公司施加压力，修复他们可能原本不愿意解决的问题。

更广泛地说，我们希望将ZK证明从学术界过渡到工业界，使它们对当今的软件更易访问和实用。如果您有我们这里未提到的该技术的特定用途，我们希望能听到您的意见。我们在导航复杂的ZK证明方案和电路编译器生态系统方面积累了专业知识，可以提供帮助！

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News

页面内容
为什么需要可利用性的ZK证明？
设计ZK证明
证明可利用性
建模x86
新的漏洞披露范式
近期文章
Trail of Bits的Buttercup在AIxCC挑战赛中获得第二名
Buttercup现已开源！
AIxCC决赛：记录
攻击者的提示注入工程：利用GitHub Copilot
作为新员工发现NVIDIA Triton中的内存损坏
© 2025 Trail of Bits。
使用Hugo和Mainroad主题生成。