Proof-based general-purpose computing with Magnetar

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

/.itemprop=publisher

/itemprop=image

基于证明的通用计算：Magnetar

发布于2026年10月15日

作者：Srinath Setty，高级首席研究员兼经理

分享本页

• 在Facebook上分享

• 在X上分享

• 在LinkedIn上分享

• 在Reddit上分享

• 订阅我们的RSS源

/#single-header

一目了然

• 一种全新的计算范式。零知识证明使您能够运行工作负载，并在结果一并获得一个简短的证明，证明程序正确执行。任何人都可以在毫秒内验证该证明，无需重新运行程序，无需信任执行者，也无需访问程序运行所需的数据。

• 广泛采用的三大障碍：使证明生成足够高效，使普通程序无需密码学专业知识即可使用证明，以及建立在即使数十年后仍受信任的密码学基础上。

• Magnetar在所有三个挑战上取得重大突破。它验证用Rust、Go或C编写程序，平均运行速度比之前最快的同类系统快10至39倍，且仅依赖标准哈希函数保障安全。这是微软研究院十余年关于使零知识证明实用化的研究最新成果。

一种全新的计算范式

计算机产生的每个结果都隐含一个问题：程序是否按声明运行并产生正确输出？目前，回答这个问题通常需要在验证的同时依赖一定程度的信任。我们信任操作者、供应商、交易对手或代理，并依靠合同、审计和日志来建立这种信任。

零知识证明提供了一种根本不同的信任建立方式。程序运行时，会连同输出一起生成一个简短的证明，这是一个密码学证书，证明在这些输入下该程序产生了该输出。证明体积小且验证速度快。接收证明者可以在毫秒内确认结果，无需重新运行程序，并可将证明传递给需要相同保证的任何人。凭借零知识特性，证明也不会泄露应保持私密的输入信息。

这改变了现实世界中正确性的含义。结果不再需要因为生产者是谁而被信任，而是可以通过伴随的证明进行验证。代表某人行事的AI代理可以附加证明，证明每个操作都符合其获得的政策。受监管的金融机构可以在不公开交易的情况下证明交易已正确处理。这些成为可能，只需生成证明像运行程序一样成为常规操作。

通用性与可用性。许多证明系统要求开发者手动将程序重写为密码学电路，这种电路是对特定计算的固定算术描述。这需要数月时间。每次应用程序的更改都意味着需要新的电路，而这种转换本身也是安全漏洞的常见来源。一种通用的替代方案是证明普通处理器的执行过程，从而使任何编译后的程序都能按原样进行证明。直到最近，这种通用性在速度或安全性方面都伴随着高昂的代价。

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

学术会议

微软在SOSP 2026

学术界和工业界参与者提交的研究论文和经验论文涵盖了计算机系统软件理论与实践的全貌。

了解更多

/.msr-promo__content

/.msr-promo__inner-wrap

在新标签页中打开

/.msr-promo

十余年的研究积累

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

2019年推出的Spartan零知识证明系统重新采用求和检查协议，并在无需可信设置的情况下使其适用于通用程序。Spartan还可以使用不同的密码学构建模块进行实例化。这种灵活性后来使证明系统能够仅基于哈希函数构建。随后一系列成果填补了剩余的空白：

• 2021年推出的Phalanx（在新标签页中打开）展示了如何利用重复性（如处理器在每一步执行相同的指令周期），使计算证明速度比Spartan快一个数量级。Magnetar处理器描述正是基于这一思路。

• Nova（在新标签页中打开）、HyperNova（在新标签页中打开）、NeutronNova（在新标签页中打开）、Neo和SuperNeo（在新标签页中打开）表明，提前终止Spartan证明过程并合并部分结果，可以以远低于现有成本证明任意规模的计算。

• Brakedown (opens in new tab) 于 2021 年提出了一种快速的基于哈希的承诺方案，并将其与 Spartan 结合，首次实现了安全性依赖于标准哈希函数的 Spartan 变体。

• Spice (opens in new tab) 、Lasso (opens in new tab) 、Nebula (opens in new tab) 以及后续的 Twist and Shout (opens in new tab) 使通用处理器核心的内存操作验证变得经济高效，而 Jolt (opens in new tab) 展示了将这些技术与 Spartan 结合后，可以高效验证完整处理器的执行过程。

• 今年早些时候，Vega (opens in new tab) 将这一研究方向应用于数字身份领域，仅用不到十分之一秒即可从政府凭证中验证事实。

• 最近，BinarySpartan (opens in new tab) 将 Spartan 扩展到二进制域，在该领域处理器逻辑和标准哈希函数可以被高效表达。BinarySpartan 还依赖于 Ligerito (opens in new tab) —— 一种类似 Brakedown 的承诺方案，其证明长度显著缩短 —— 以及 ring switching (opens in new tab) ，后者使对位向量的承诺变得高效。

这些成果分别解决了问题的不同部分。Magnetar 是这些拼图最终汇聚的地方。

Magnetar

Magnetar 是一种零知识虚拟机（zkVM），它在三个核心挑战上同时取得重大突破。

图 1. Magnetar 验证程序执行并生成任何人都可验证的小型证明，其安全性仅依赖于标准哈希函数。

它具有通用性。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 使密码学证明成为计算常规输出的未来成为可能。我们预计技术领导者将停止询问执行证明是否实用，而是专注于希望验证哪些结果，而不是依赖信任。

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

相关出版物

Card

Spartan：无需可信设置的高效通用型 zkSNARKs

Magnetar：基于标准哈希的高速后量子 RV64 zkVM

Neo 和 SuperNeo：小域上按位计费的后量子折叠方案

作者介绍

Card column wrapper

Card body

Srinath Setty

高级首席研究员兼经理

Card footer

研究领域

• 编程语言与软件工程

• 安全、隐私与密码学

相关实验室

• 微软雷德蒙德研究院