微软研究院发布 Magnetar：基于证明的通用计算 zkVM

概览

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

一种全新的计算形式

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

零知识证明提供了一种建立信任的根本不同的方法。程序运行后，除了输出之外，还会生成一份简短的证明——一份密码学证书，证明这个程序在这些输入下产生了这个输出。该证明体积小、验证快。收到它的人可以在毫秒级内确认结果，无需重新运行程序，并且可以将证明转交给任何其他需要同样保证的人。借助零知识特性，该证明也不会泄露任何应当保密的输入信息。

这改变了现实世界中“正确性”的含义。一个结果不再需要因为由谁产生而被人信任，而是可以因为随附的证明而被验证。代表某人行事的 AI 代理可以附上一份证明，表明每个操作都符合其被赋予的策略。受监管的金融机构可以证明交易被正确处理，而无需公开其交易内容。一旦生成证明变得像运行程序一样常规，这些都将成为可能。

三大挑战

零知识证明发明于 20 世纪 80 年代，而证明程序执行背后的思想也已存在了几乎同样长的时间。阻碍它们成为通用工具的，是三大难以同时解决的挑战。

效率。生成一份证明历来需要比运行程序本身多出数百万倍的计算量。多年的研究已经降低了这一开销，但最快的系统是通过在其他方面做出妥协才达到其速度的。

通用性与可用性。许多证明系统要求开发者手动将其程序重写为密码学电路，即对该精确计算的固定算术描述。这需要数月时间。应用程序的每一次更改都意味着一个新的电路，而翻译本身也是安全漏洞的常见来源。一种通用的替代方案是证明普通处理器的执行过程，这样任何已编译的程序都可以按其编写的样子被证明。直到最近，这种通用性在速度或安全性上都付出了高昂的代价。 

安全性。证明的强度取决于其底层的密码学。许多证明系统依赖于椭圆曲线，而足够强大的量子计算机可以破解椭圆曲线。微软正在通过其量子安全计划解决这个问题，该计划将把其产品和服务迁移到后量子密码学，这一目标最近被加速到2029年。后量子证明系统已经存在，但有些依赖于格假设，而大多数依赖于为降低证明成本而发明的新密码学函数。这些新的密码学函数尚未经历保护当今互联网的密码学所受到的数十年审视，而且有些依赖于关于纠错码的尚未被证明的数学猜想。它们用强假设换来了速度。 

十余年的工作

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

2019年，一个名为Spartan的新零知识证明系统回归了求和校验方法，并使其无需可信设置即可适用于通用程序。Spartan还可以用不同的密码学构建块来实例化。正是这种灵活性，后来使得该证明系统可以仅建立在哈希函数之上。随后的一系列成果填补了剩余的拼图： 

• 2021年的Phalanx（在新标签页中打开）展示了如何利用重复性，例如处理器在每一步运行相同的指令周期，来以比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 风格的承诺方案，其证明要短得多——以及 ring switching（在新标签页中打开），后者使得对位向量进行承诺变得高效。 

这些工作各自解决了问题的一部分。Magnetar 则是将这些部分汇聚在一起的地方。

Magnetar

Magnetar 是一个零知识虚拟机，即 zkVM，它同时在全部三项挑战上取得了重大进展。

它是通用的。Magnetar 证明 RISC-V 的执行过程，这是一种开放的处理器架构，为所有主流语言都拥有成熟的编译器。开发者用 Rust、Go 或 C 编写程序，像平常一样编译它，Magnetar 就能按原样证明它。想想这在实践中意味着什么。一条业务策略、一条数据流水线，或一个以太坊虚拟机（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 进行基于证明的通用计算最初发表于微软研究院。