微软研究院发布 Magnetar:基于标准哈希函数的通用零知识证明 zkVM
Proof-based general-purpose computing with Magnetar
微软研究院发布零知识虚拟机 Magnetar,可证明用 Rust、Go 或 C 编写的程序执行,在笔记本上每秒证明 7.2 至 8.7 百万条 RISC-V 处理器指令,15 项基准上平均比现有最快的 zkVM 快 10 至 39 倍。
微软研究院给出 MagneTar 的技术设计与实测数据,读者可了解零知识证明在通用程序证明上如何摆脱椭圆曲线与可信设置。

概览
- 一种全新的计算形式。零知识证明让你在运行某个工作负载后,除了得到结果之外,还能获得一个简短的证明,表明该程序运行正确。任何人都能在毫秒级时间内验证这个证明,无需重新运行程序,无需信任运行程序的人,也无需获取程序运行所依据的数据。
- 三大挑战一直阻碍着零知识证明的广泛采用:让证明的生成速度足够快;让普通程序无需密码学专业知识即可使用;以及让其所依赖的密码学在几十年后依然值得信赖。
- Magnetar 在这三大挑战上都取得了重大进展。它能证明用 Rust、Go 或 C 编写的程序,平均运行速度比此前最快的同类系统快 10 到 39 倍,并且其安全性仅依赖于标准哈希函数。这是 Microsoft Research 十多年来致力于让零知识证明走向实用化的最新成果。
一种全新的计算形式
计算机产生的每一个结果都伴随着一个隐含的问题:程序是否如所称那样运行并产生了正确的输出?如今,回答这个问题往往需要在验证之外还依赖某种程度的信任。我们信任运营方、供应商、交易对手或代理,并依靠合同、审计和日志来建立这种信任。
零知识证明提供了一种从根本上不同的建立信任的方式。程序运行时,除了输出之外还会生成一个简短的证明——一份密码学证书,表明该程序在这些输入下产生了这个输出。证明很小,验证速度很快。收到证明的人可以在毫秒级时间内确认结果,而无需重新运行程序,并且可以将证明转交给任何需要同样保证的人。借助零知识特性,证明也不会泄露任何应当保密的输入信息。
这改变了现实世界中正确性的含义。一个结果不再因为它由谁产生而必须被信任,而是因为随附的证明而可以被验证。代替某人行事的 AI 代理可以附上证明,表明每个操作都符合赋予它的策略。受监管的金融机构可以证明交易得到了正确处理,而无需公开其交易。一旦生成证明变得像运行程序一样平常,这些都将成为可能。
三大挑战
零知识证明发明于 20 世纪 80 年代,而证明程序执行背后的思想也几乎同样古老。阻碍它们成为通用工具的,是三大难以同时解决的挑战。
效率。生成一个证明在历史上所需的计算量是运行程序本身的数百万倍。多年的研究已经降低了这一开销,但最快的系统是通过在其他方面做出妥协才达到这样的速度的。
通用性与易用性。许多证明系统要求开发者手动将程序改写为密码学电路,即对该具体计算的固定算术描述。这需要数月时间。应用程序的每一次更改都意味着一个新电路,而这一转换本身就是安全漏洞的常见来源。一种通用的替代方案是证明普通处理器的执行过程,这样任何已编译的程序都可以按其编写的样子被证明。直到最近,这种通用性在速度或安全性方面都付出了高昂代价。
安全性。证明的强度取决于其底层密码学。许多证明系统依赖椭圆曲线,而足够强大的量子计算机可以破解椭圆曲线。Microsoft 正在通过其 Quantum Safe Program 解决这个问题,该计划将把其产品和服务迁移到后量子密码学,这一目标最近被加速到 2029 年。后量子证明系统已经存在,但有些依赖于格假设,而大多数依赖于为降低证明成本而发明的新密码学函数。这些新密码学函数尚未经历保护当今互联网的密码学所受到的数十年审视,而且有些依赖于关于纠错码的尚未被证明的数学猜想。它们以强假设换取了速度。
十多年的工作
十多年来,Microsoft Research 一直致力于让零知识证明和可验证计算变得实用。早期研究沿两条路线展开,二者都只对小程序实用。第一种(在新标签页中打开) (在新标签页中打开)让验证者通过一种称为求和检查协议(在新标签页中打开)的技术,与证明者进行简短对话来检查长计算,但这仅适用于具有特定分层结构的计算。第二种(在新标签页中打开) (在新标签页中打开)使用椭圆曲线密码学,为几乎所有计算创建非常小的证明。但这需要一次性可信设置,涉及秘密信息,一旦泄露,任何人都可以伪造证明。这种方法也容易受到量子计算机的攻击。
2019 年,一个名为 Spartan 的新零知识证明系统重新采用了求和检查方法,并使其无需可信设置即可适用于通用程序。Spartan 还可以用不同的密码学构建模块来实例化。正是这种灵活性,后来使该证明系统能够仅基于哈希函数构建。随后的一系列成果填补了其余部分:
- 2021 年的 Phalanx(在新标签页中打开)展示了如何利用重复性,例如处理器在每一步运行相同的指令周期,以比 Spartan 快一个数量级的速度证明计算。Magnetar 的处理器描述就建立在这一思想之上。
- Nova(在新标签页中打开)、HyperNova(在新标签页中打开)、NeutronNova(在新标签页中打开)、Neo 和 SuperNeo(在新标签页中打开)表明,提前停止 Spartan 的证明,并将部分结果折叠在一起,使得以低得多的成本证明任意规模的计算变得实用。
- 2021 年,Brakedown(在新标签页中打开) 提出了一种基于哈希的快速承诺方案,并将其与 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 进行基于证明的通用计算 首次发表于 Microsoft Research。
来源:Microsoft Research · microsoft.com