Microsoft Research 推出通用零知识虚拟机 Magnetar

概览

• 一种新的计算形式。零知识证明让你运行一个工作负载，并在获得结果的同时，收到一份简短证明，证明程序运行正确。任何人都能在几毫秒内验证该证明，无需重新运行程序，无需信任运行程序的人，也无需获取程序运行所用的数据。
• 三大挑战阻碍了零知识证明的广泛应用：让证明的生成速度足够快，让普通程序无需密码学专业知识也能使用零知识证明，以及让其建立在数十年后仍值得信赖的密码学基础之上。
• Magnetar 在应对这三大挑战方面取得了重大进展。它可以为用 Rust、Go 或 C 编写的程序生成证明，平均运行速度比此前最快的同类系统快 10 至 39 倍，并且其安全性仅依赖标准哈希函数。这是 Microsoft Research 十多年来致力于让零知识证明变得实用的研究所取得的最新成果。

一种新的计算形式

计算机产生的每个结果都隐含着一个问题：程序是否如所声称的那样运行，并产生了正确的输出？如今，要回答这个问题，除了验证之外，往往还需要一定程度的信任。 我们信任运营方、供应商、交易对手或代理，并依靠合同、审计和日志来建立这种信任。 

零知识证明提供了一种根本不同的建立信任的方式。程序运行时，会在输出结果的同时生成一份简短证明——一种密码学证书，证明该程序在给定这些输入的情况下产生了该输出。该证明体积小、验证速度快。接收者无需重新运行程序，就能在几毫秒内确认结果，还可以将证明转交给任何需要同等保证的人。借助零知识属性，该证明也不会泄露应当保密的输入信息。

这改变了现实世界中对正确性的定义。我们不再需要因为结果由谁产生而信任它；只要检查随结果提供的证明即可。代表他人行事的 AI 代理可以附上证明，表明其每项操作都符合所遵循的策略。受监管的金融机构可以证明交易得到了正确处理，而无需公开交易信息。只要生成证明像运行程序一样成为常规操作，这些应用就都能实现。

三大挑战

零知识证明诞生于 20 世纪 80 年代，而证明程序执行的相关思想也几乎有同样长的历史。阻碍它成为通用工具的，是三个长期以来难以同时解决的挑战。

效率。过去，生成证明所需的计算量通常是运行程序本身的数百万倍。多年的研究已降低了这一开销，但最快的系统是通过在其他方面作出妥协来实现速度提升的。

通用性和易用性。许多证明系统要求开发人员手动将程序重写为密码学电路，也就是对该计算进行固定的算术描述。这需要数月时间。应用程序的每次改动都意味着要重新编写电路，而这种转换本身也经常会引入安全漏洞。通用替代方案是证明普通处理器的执行过程，这样任何编译后的程序都可以按原样进行证明。直到最近，这种通用性仍要付出高昂代价：速度或安全性难以兼顾。 

安全性。证明的强度取决于其底层密码学。许多证明系统基于椭圆曲线，而足够强大的量子计算机能够破解椭圆曲线。Microsoft 正通过其量子安全计划应对这一问题，该计划将 推动其产品和服务转向后量子密码学；Microsoft 最近将这一目标提前到了 2029 年。后量子证明系统已经问世，但有些基于格假设，大多数则依赖为降低证明成本而设计的新型密码函数。这些新型密码函数尚未经历保护当今互联网的密码学所接受的数十年审查，其中一些还基于有关纠错码的数学猜想，而这些猜想尚未得到证明。它们以强假设换取了速度。 

十余年的研究

十余年来，Microsoft Research 一直致力于让零知识证明和可验证计算变得实用。早期研究采用了两种方法，但都只适用于小型程序。第一种（在新标签页中打开） （在新标签页中打开）利用一种称为求和检查协议（在新标签页中打开）的技术，让验证者通过与证明者进行简短对话来检查长时间的计算，但这种方法只适用于具有特定分层结构的计算。第二种（在新标签页中打开） （在新标签页中打开）使用椭圆曲线密码学，为几乎任何计算生成非常小的证明 。但这种方法需要进行一次性的可信 设置，其中涉及秘密信息；如果这些信息泄露，任何人都可能伪造证明。这种方法也容易受到量子计算机攻击。

2019 年，一种名为 Spartan 的新型零知识证明系统重新采用求和检查方法，并使其适用于通用程序，且无需可信设置。Spartan 还可以使用不同的密码学构件来实现。正是这种灵活性，后来使该证明系统得以仅基于哈希函数构建。随后一系列研究成果补齐了其余部分： 

• Phalanx（在新标签页中打开）于 2021 年展示了如何利用重复性来加速证明，例如处理器在每一步都运行相同的指令周期，从而使计算证明速度比 Spartan 快一个数量级。Magnetar 的处理器描述便基于这一思路。  
• Nova（在新标签页中打开）、HyperNova（在新标签页中打开）、NeutronNova（在新标签页中打开）、Neo 和 SuperNeo（在新标签页中打开）表明，提前停止 Spartan 的证明过程，并将部分结果折叠在一起，就能以低得多的成本，实用地证明任意规模的计算。
• Brakedown（在新标签页中打开） 于 2021 年推出了一种基于哈希的快速承诺方案，并将其与 Spartan 结合，带来了首个安全性仅依赖标准哈希函数的 Spartan 变体。 
• Spice（在新标签页中打开）、Lasso（在新标签页中打开）、Nebula（在新标签页中打开），以及随后出现的 Twist and Shout（在新标签页中打开），让通用处理器核心的内存操作变得易于证明；而 Jolt（在新标签页中打开） 则展示了将这些操作与 Spartan 结合后，可以高效证明完整处理器的执行过程。
• 今年早些时候，Vega（在新标签页中打开） 将这项工作应用于数字身份，在不到十分之一秒的时间内证明了政府凭证中的事实。
• 最近，BinarySpartan（在新标签页中打开） 将 Spartan 引入二进制域，在那里可以高效表示处理器逻辑和标准哈希函数。BinarySpartan 还依赖于 Ligerito（在新标签页中打开）——一种 Brakedown 风格的承诺方案，能够生成短得多的证明——以及环切换（在新标签页中打开），后者能够高效地对比特向量作出承诺。 

这些方案分别解决了问题的一部分。Magnetar 让这些部分汇聚到了一起。

Magnetar

Magnetar 是一种零知识虚拟机（zkVM），同时在这三个挑战上都取得了重大进展。

它是通用的。 Magnetar 证明 RISC-V 的执行过程。RISC-V 是一种开放的处理器架构，所有主流语言都有成熟的编译器。开发者可以用 Rust、Go 或 C 编写程序，像往常一样进行编译，然后由 Magnetar 证明该程序的原样执行。看看这在实践中意味着什么：业务策略、数据管道，或 Ethereum Virtual Machine（EVM）的解释器，都只是一个程序；而已经负责维护这些程序的工程师，可以准确证明它们按照原样执行。因此，证明不再是一项只有专家才能从事的工作。 

它比同类的早期系统更快。 Magnetar 在笔记本电脑上每秒可证明 720 万至 870 万条处理器指令。在 15 个基准程序中，从加密哈希到小型 EVM 解释器中的代币转账，其平均速度是同一台机器上现有最快 zkVM 的 10 至 39 倍；在一项代币转账基准测试中，其速度更是另外两个系统的 300 多倍。经过优化的 Magnetar 每秒可证明 950 万至 1280 万个周期，使本文报告的每项加速比提高约 1.3×。其证明的验证时间约为 12 毫秒。 

其安全性基于标准密码学。 Magnetar 依赖标准哈希函数，例如 SHA-256 或 SHA-3，这些原语已经在保护每个组织的系统。它不需要椭圆曲线、不需要格、不需要专用哈希函数、不需要可信设置，也不需要任何关于纠错码的未经证明的猜想。哈希函数是密码学工具箱中经过最充分研究的原语，也是 NIST 将其标准化为保守型后量子选项的无状态基于哈希的签名的基础。对于必须在未来几十年仍值得信赖的系统而言，只依赖标准哈希函数，就能从路线图中移除一次密码学迁移。 

同一设计决策还带来了第二项收益。检查 Magnetar 证明主要包括计算标准哈希函数和二进制域算术，而这正是 Magnetar 能够高效证明的操作。因此，对 Magnetar 而言，验证证明就是普通工作负载。这使 Magnetar 能够通过分块证明再组合这些部分，来证明任意规模的计算。这也使 Magnetar 能够证明账本或区块链等长时间运行的系统。

技术论文介绍了完整的设计、安全性分析和测量结果。

展望未来

Magnetar 推动零知识证明和可验证计算发展到这样一个阶段：它们可以建立在组织已经信任的密码学之上，以足够快的速度运行，并由编写普通代码的工程师构建。Magnetar 开创了这样一个未来：密码学证明将成为计算的常规输出。我们预计，技术领导者将不再询问执行证明是否切实可行，而是转而关注哪些结果他们更愿意进行验证，而不是直接信任。

如果您有兴趣探索零知识证明如何支持您的使用场景，我们很乐意听取您的想法（在新标签页中打开）。

在新标签页中打开

文章基于证明的通用计算：Magnetar最初发表于Microsoft Research。