跳到正文
原文
Microsoft Research· Srinath Setty·· 24 天前精选AI 评分78

Microsoft Research 推出 Magnetar zkVM:直接证明 Rust/Go/C 程序执行,速度提升 10–39 倍

Proof-based general-purpose computing with Magnetar

AI 摘要

Microsoft Research 发布 Magnetar,一个基于 RISC-V 的零知识虚拟机(zkVM),可直接证明用 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.

一览无余

  • 一种新的计算形式。零知识证明允许你运行工作负载,并在结果旁边接收一个简短的证明,证明程序运行正确。任何人都可以在毫秒内检查证明,而无需重新运行程序,无需信任运行程序的人,也无需知道程序运行的数据
  • 有三个重大挑战阻碍了其广泛采用:使证明足够快以生成,使它们对普通程序可用而不需要密码学专业知识,以及使它们基于几十年后仍然可信的密码学
  • Magnetar 在所有三个挑战上都取得了重大进展。它证明 Rust、Go 或 C 编写的程序,平均比最快的同类系统快 10 到 39 倍,并且其安全性仅依赖于标准哈希函数。这是微软研究院在十多年关于使零知识证明实用的研究中的最新成果

一种新的计算形式

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

零知识证明提供了一种根本不同的方法来建立信任。程序运行,并与其输出一起产生一个简短的证明,一个加密证书,证明这个程序,在这些输入下,产生了这个输出。证明很小,检查速度快。收到证明的人可以在毫秒内确认结果,而无需重新运行程序,并且可以将证明传递给任何需要相同保证的人。凭借零知识特性,证明也不会透露应该保持私密的输入信息

这改变了现实世界中正确性的含义。结果不再因为生产它的原因而需要信任。它之所以可以检查,是因为它伴随的东西。一个代表某人行动的 AI 代理可以附加一个证明,证明每个行动都符合它收到的政策。受监管的金融机构可以证明交易被正确处理,而无需公开其交易。一旦生成证明和运行程序一样常规,这些就成为可能

三个重大挑战

零知识证明是在 20 世纪 80 年代发明的,证明程序执行背后的思想几乎和它一样长。是什么让它们没有成为通用工具,是三个挑战,这些挑战一直难以同时解决

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

通用性和易用性。 许多证明系统要求开发人员手动将他们的程序重写为加密电路,这是一种对该特定计算的固定算术描述。这需要花费数月时间。应用程序的每次更改都意味着一个新的电路,而翻译本身就是一个频繁产生安全漏洞的来源。一种通用的替代方案是证明普通处理器的执行,以便任何编译的程序都可以按原样证明。直到最近,这种通用性是以速度或安全性的巨大代价为代价的。

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

十多年的工作

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

2019年,一种名为 Spartan 的新型零知识证明系统回归求和检查方法,并使其适用于无需可信设置的通用程序。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的执行,这是一种具有成熟的主流语言编译器的开放处理器架构。开发者用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 证明像账本或区块链这样的长期运行的系统。

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

展望

Magnetar 将零知识证明和可验证计算推进到可以建立在组织已经信任的密码学之上的阶段,速度使其可用,由编写普通代码的工程师来实现。Magnetar 使加密证明成为计算常规输出的未来成为可能。我们预计技术领导者将停止询问 执行证明是否实用,而是关注 他们宁愿验证哪些结果 而不是信任。

如果您有兴趣探索零知识证明如何支持您的用例,我们很乐意 与您联系(在新标签页中打开)。

在新标签页中打开

基于证明的通用计算 Magnetar 一文首先出现在 Microsoft Research。

来源:Microsoft Research · microsoft.com

00