粗棉布：现实世界漏洞的零知识证明

《ACM Transactions on Privacy and Security》：Cheesecloth: Zero-Knowledge Proofs of Real-World Vulnerabilities

零知识证明工具链Cheesecloth实现软件漏洞的隐私安全验证，支持内存越界、数据泄漏、交互攻击及拒绝服务等类型，通过优化电路生成和运行时检查提升效率，实际案例验证了其在OpenSSL、FFmpeg等系统中的有效性。

　　在现代软件开发中，安全性问题一直是一个重要挑战。当安全分析师发现关键软件系统中的漏洞时，他们面临着一个两难的局面：立即公开漏洞可能会对用户造成伤害，而仅向软件供应商披露则可能导致供应商忽视或优先级较低地处理安全风险，从而损害无意中受影响的用户。为了解决这一问题，近年来的研究工作提出了使用零知识（Zero-Knowledge，ZK）协议的方法，使得分析师可以在不透露漏洞细节或利用输入的情况下，证明他们知道漏洞的存在。然而，现有的ZK漏洞证明方法在规模和表达能力方面仍存在局限，主要是由于生成能够准确建模现实软件的证明语句以及直接表述违反性质的挑战。

本文介绍了一种名为Cheesecloth的新颖证明语句编译器，它通过在公共输入上对程序进行预处理，选择性地揭示执行控制段的信息，并采用一种新的存储标签方案来形式化信息泄露，从而实现了在ZK中证明实际漏洞。Cheesecloth的实用性得到了实际测试的验证，它成功生成了知名漏洞的ZK证明，包括OpenSSL的Heartbleed信息泄露、FFmpeg多媒体编码框架中的内存漏洞、Secure Scuttlebutt去中心化社交网络中的密码实现错误以及OpenSSL的拒绝服务漏洞。其中，针对OpenSSL的拒绝服务漏洞，Cheesecloth能够证明程序执行过程需要数万亿次循环，这是目前所知的最长的ZK程序执行证明。

为了实现这一目标，Cheesecloth引入了一系列优化措施，以高效地编码实际软件中的漏洞。这些优化包括对程序结构的利用，而不泄露额外的执行信息。具体而言，公共程序计数器（Public-PC）段能够为程序的基本块构建高效的电路，使得在程序计数器公开的情况下，可以进行激进的常量折叠，而不泄露整体执行轨迹。此外，执行频率较低的指令被稀疏支持，使得证明语句的规模减小。这些优化措施显著提升了ZK证明的效率和实用性。

Cheesecloth还对内存错误进行了高效的ZK编码，特别是针对常见且关键的软件漏洞，如越界访问、使用后释放、释放后释放以及未初始化访问。与之前的工作相比，Cheesecloth的编码方法在内存模型上更加高效。此外，Cheesecloth还引入了一种新的网络通信模型，使得ZK证明可以涵盖多个交互程序的执行情况。该模型确保了数据在通信通道中的正确传递，并且在程序执行过程中对通信模型的内部状态进行了验证，从而防止程序在通信过程中被篡改。

在证明漏洞方面，Cheesecloth还引入了一种创新的符号执行框架，该框架能够高效地验证程序的执行属性。这种技术允许ZK证明验证显著更长的程序执行，从而突破了之前最先进的技术。符号执行框架的核心在于其对程序执行轨迹的抽象和推理，使得可以验证程序的执行属性而不必关注具体的执行细节。

为了生成ZK证明，Cheesecloth首先将软件的源代码（支持C、C++和Rust）与一个标记为漏洞类别的标志结合起来，然后结合运行时环境的模拟（包括操作系统和库），应用上述技术生成可以直接在ZK中验证的语句。ZK证明可以通过提供具体的利用输入作为见证者，向验证者展示漏洞的存在，而不会泄露漏洞本身或触发输入的细节。

Cheesecloth的实现不仅限于理论上的创新，还通过实际案例研究验证了其有效性。例如，在OpenSSL的Heartbleed漏洞证明中，Cheesecloth成功生成了ZK证明，展示了程序在1.3百万次执行步骤中泄露任意用户信息。此外，Cheesecloth还证明了FFmpeg、GRIT和Scuttlebutt中的漏洞，展示了其在实际软件系统中的应用潜力。

Cheesecloth的实现包括多个关键组件：MicroRAM汇编语言、MicroRAM编译器和见证者检查生成器。MicroRAM汇编语言是Cheesecloth的核心中间表示语言，它基于TinyRAM，但进行了优化，以支持更高效的ZK验证。MicroRAM编译器将LLVM或RISC-V程序编译为MicroRAM汇编代码，而见证者检查生成器则生成ZK电路，用于验证程序执行的轨迹。

在证明内存不安全漏洞时，Cheesecloth采用了动态内存分配的编码方式，通过跟踪内存的有效性，检测程序对非有效内存的访问。该方法能够检测多种内存错误，如未初始化访问、使用后释放、释放后释放和越界访问。这些检测方法不仅能够捕获漏洞，还能够确保程序执行的正确性。

在检测数据泄露时，Cheesecloth采用了一种新颖的标签系统，该系统能够跟踪程序存储中可能和必须包含的秘密数据。通过在程序执行过程中标注敏感源和汇，Cheesecloth能够检测数据泄露，而不会泄露敏感输入的细节。这种标签系统能够有效区分程序在不同执行路径中可能泄露的信息，从而确保验证的准确性。

在处理交互式网络攻击时，Cheesecloth能够验证程序在与攻击者进行网络交互时是否存在漏洞。这种方法需要对攻击程序和受害程序进行联合验证，确保攻击程序能够动态与受害程序交互并执行攻击。为了防止攻击程序泄露受害程序的敏感信息，Cheesecloth引入了特权内存的概念，并通过Fiat-Shamir协议来确保攻击程序无法获取受害程序的敏感信息。

在处理拒绝服务攻击时，Cheesecloth能够验证程序在特定输入下是否会进入无限循环或执行大量步骤，从而导致拒绝服务。这种方法通过构建一个包含足够步骤的执行轨迹，并使用符号执行框架来验证程序的执行属性，从而确保验证的准确性。

通过这些优化和编码方法，Cheesecloth不仅能够高效地生成ZK证明，还能够确保证明的隐私性，即不会泄露漏洞或触发输入的细节。这种方法为安全分析师提供了一种安全且有效的工具，使他们能够在不公开具体漏洞信息的情况下，证明软件系统的漏洞存在。此外，Cheesecloth的实现还展示了其在实际软件系统中的应用潜力，包括对大规模程序和复杂漏洞的处理能力。

Cheesecloth的贡献不仅在于其技术实现，还在于其对实际软件漏洞的验证能力。通过实际案例研究，Cheesecloth证明了其在不同软件系统中的有效性，包括OpenSSL、FFmpeg和Scuttlebutt等。这些案例研究不仅展示了Cheesecloth的实用性，还验证了其在实际应用中的性能和效率。

Cheesecloth的实现还考虑了安全性问题，确保生成的ZK证明不会泄露额外的信息。为此，Cheesecloth采用了多种安全措施，包括对内存访问的严格验证、对程序执行的保密性处理以及对网络通信的验证。这些措施确保了生成的ZK证明的保密性，使得安全分析师能够在不泄露漏洞和触发输入的情况下，证明软件系统的漏洞存在。

总的来说，Cheesecloth是一种创新的工具，它通过一系列优化和编码方法，使得在ZK中证明实际软件漏洞成为可能。这种方法不仅提高了ZK证明的效率，还确保了证明的隐私性，为安全分析师提供了一种安全且有效的工具，以验证关键软件系统中的漏洞。Cheesecloth的实现展示了其在实际软件系统中的应用潜力，为未来的安全研究和实践提供了重要的参考。