Microsoft Research 发布 zkVM 系统 Magnetar：基于零知识证明的通用计算

概览

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

一种全新的计算形式

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

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

这改变了正确性在现实世界中的含义。一个结果不再因为生产者是谁而被信任，而是因为它所附带的证明而可以被验证。代表某人行事的 AI 智能体可以附上证明，说明其每项操作都符合被赋予的策略。受监管的金融机构可以在不公开交易的情况下证明交易处理正确。一旦生成证明变得像运行程序一样平常，这些都将成为可能。

三大重大挑战

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

效率。从历史上看，生成一个证明所需的计算量是运行程序本身的数百万倍。多年的研究已经降低了这一开销，但最快的系统是以在其他方面做出妥协为代价才获得速度的。

通用性与易用性。许多证明系统要求开发者手动将程序重写为密码学电路，即对该计算的确切算术化描述。这可能耗时数月。应用的每一次更改都意味着一个新电路，而这种转换本身就是安全漏洞的常见来源。一种通用的替代方案是证明普通处理器的执行过程，这样任何编译后的程序都可以按原样被证明。直到最近，这种通用性仍以极高的速度或安全性代价为代价。 

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

学术会议

微软亮相 SOSP 2026

学术界和产业界与会者将展示涵盖计算机系统软件理论与实践全部范围的研究论文和经验论文。

十余年的努力

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

2019 年，一种名为 Spartan 的新型零知识证明系统回归 sum-check 方法，并使其无需可信设置即可适用于通用程序。Spartan 还可以使用不同的密码学构建模块进行实例化。正是这种灵活性，后来使该证明系统能够仅基于哈希函数构建。随后的一系列研究成果补齐了其余的部分： 

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

这些工作各自解决了问题的一部分，而 Magnetar 则是这些碎片汇聚之处。

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

它是通用的。 Magnetar 可以证明 RISC-V 的执行，RISC-V 是一种开放处理器架构，拥有面向所有主流语言的成熟编译器。开发者用 Rust、Go 或 C 编写程序，照常编译，Magnetar 就能按原样证明它。想想这在实践中意味着什么：一条业务策略、一个数据管道，或者一个以太坊虚拟机（EVM）的解释器，都只是一个程序，而已经在维护它们的工程师可以按其原样证明执行结果。如此一来，证明不再是专家的专属活动。 

它比同类的既有系统更快。 Magnetar 在一台笔记本电脑上每秒可证明 720 万至 870 万条处理器指令。在从加密哈希到小型 EVM 解释器中的代币转账这 15 个基准程序上，它在同一台机器上平均比现有最快的 zkVM 快 10 到 39 倍，而在代币转账基准上比其中两个快 300 倍以上。经过优化的 Magnetar 每秒可证明 950 万至 1280 万个周期，这会使本文报告的每一项速度提升再提高约 1.3 倍。它的证明在大约 12 毫秒内即可完成核验。 

它的安全性建立在标准密码学之上。Magnetar 依赖于诸如 SHA-256 或 SHA-3 这样的标准哈希函数，与已经保护着每个组织系统的原语相同。它不需要椭圆曲线，不需要格，不需要专用哈希函数，不需要可信设置，也不需要任何关于纠错码的未证猜想。哈希函数是密码学工具箱中被研究得最透彻的原语，而且它们正是 NIST 将其标准化为自己的保守后量子选项的无状态基于哈希的签名的基础。对于一个必须在未来数十年仍然值得信赖的系统而言，仅依赖标准哈希函数可以从路线图中省去一次密码学迁移。 

同样的设计决策还带来了第二重收益。验证 Magnetar 证明主要包括对标准哈希函数和二元域算术的求值，而这些正是 Magnetar 能够高效证明的操作。因此，验证证明对它来说是一项普通的工作负载。这使得 Magnetar 能够证明任意规模的计算，方法是将计算分块证明，然后再合并各块。这也使 Magnetar 能够证明诸如账本或区块链这类长期运行的系统。

技术论文给出了完整的设计、安全性分析和测量数据。

展望未来

Magnetar 将零知识证明和可验证计算推进到了这样一个阶段：它们可以构建在组织已经信任的密码学之上，以使其可用的速度运行，并由编写普通代码的工程师来实现。Magnetar 开启了一个密码学证明成为计算常规输出的未来。我们预计，技术领导者将不再追问执行证明是否实用，而是聚焦于哪些结果他们更倾向于验证而非信任。

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