Microsoft Research更新于

基于证明的 Magnetar 通用计算

微软研究院推出零知识证明虚拟机Magnetar,可直接证明Rust、Go或C程序的执行,平均比现有最快zkVM快10到39倍。它是可验证计算研究,AI代理仅作为潜在应用被提及。

Magnetar proves a program's execution and returns a small proof that anyone can check, with security resting only on standard hash functions.
配图来源 · Microsoft Research
Magnetar proves a program's execution and returns a small proof that anyone can check, with security resting only on standard hash functions.

概览

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

一种全新的计算形式

计算机产生的每一个结果都伴随着一个隐含的问题:程序是否如声称的那样运行并产生了正确的输出?如今,回答这个问题往往需要一定程度的信任以及验证。我们信任操作者、供应商、交易对手或代理,并依靠合同、审计和日志来建立这种信任。

零知识证明提供了一种从根本上不同的建立信任的方式。程序运行后,除输出之外还会生成一个简短的证明,一份密码学凭证,表明该程序在这些输入上产生了这个输出。该证明体积小且验证迅速。收到它的人可以在几毫秒内确认结果,无需重新运行程序,还可以把证明传递给任何需要同样保证的人。凭借零知识特性,该证明还不会泄露任何应保持私密的输入信息。

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

三大重大挑战

零知识证明诞生于 1980 年代,而证明程序执行背后的思想几乎同样历史悠久。使它们一直无法成为通用工具的,是三个始终无法同时解决的挑战。

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

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

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

PODCAST SERIES

Illustration of Doug Burger

The Shape of Things to Come

欢迎收听 Microsoft 的 Doug Burger 与嘉宾深入探讨关于 AI 的基本真理以及它将如何重塑未来。

立即收听

十余年的努力

十多年来,微软研究院一直致力于让零知识证明和可验证计算走向实用。早期研究沿两条路线展开,但都只对小型程序实用。 第一种方法(在新标签页中打开) (在新标签页中打开)让验证者通过与证明者的简短对话来检查一段冗长的计算,所用的技术称为 sum-check协议(在新标签页中打开),但这仅适用于具有特定分层结构的计算。 第二种方法(在新标签页中打开) (在新标签页中打开)使用椭圆曲线密码学为几乎任何计算创建非常小的证明。但这需要一次性的可信设置,其中涉及秘密信息,一旦泄露,任何人都可以伪造证明。这种方法还容易受到量子计算机的攻击。

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

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

Magnetar

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

Figure 1. Magnetar proves a program's execution and returns a small proof that anyone can check, with security resting only on standard hash functions.
图1. Magnetar证明程序的执行并返回一个任何人都可以检查的小型证明,其安全性仅依赖于标准哈希函数。

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

它比同类先前系统更快。 Magnetar 在一台笔记本电脑上每秒可证明 7.2 至 8.7 百万条处理器指令。在从密码学哈希到小型 EVM 解释器内代币转移的 15 个基准程序上,在同一台机器上,它平均比现有最快的 zkVM 快 10 至 39 倍,在一个代币转移基准上比另外两个快 300 多倍。优化后的 Magnetar 每秒可证明 9.5–12.8 百万个周期,这将本文报告的每一项加速提升约 1.3×。它的证明可在约 12 毫秒内完成验证。 

其安全性建立在标准密码学之上。 Magnetar 依赖于标准哈希函数,如 SHA-256 或 SHA-3,这些正是已经在保护每个组织系统的原语。它不需要椭圆曲线、不需要格、不需要专用哈希函数、不需要可信设置,也不需要关于纠错码的未证明猜想。哈希函数是密码学工具包中被研究得最透彻的原语,而且它们是无状态基于哈希的签名的基础,NIST 已将后者标准化为其保守的后量子选项。对于一个在几十年后仍必须值得信赖的系统而言,仅依赖标准哈希函数就免除了路线图上的一次密码学迁移。 

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

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

展望未来

Magnetar 将零知识证明和可验证计算推进到一个新阶段:它们可以构建在组织已经信任的密码学之上,速度足够快因而实用,并且能由编写普通代码的工程师使用。Magnetar 开启了一个未来,密码学证明将成为计算的常规产出。我们预计技术领导者将不再追问 执行证明是否实用 ,而是专注于 哪些结果 他们更愿意 通过验证而非信任来接受.

如果您有兴趣探索零知识证明如何支持您的用例,我们很乐意 听到您的声音(在新标签页中打开).

原始出处

Microsoft Research

内容说明

原始发布及相关权利归来源方。

机器翻译 · 请以原文为准