这是关于"可验证计算"的三部分系列文章的第二篇,涵盖了该领域的一些最新研究成果以及可能存在的陷阱。本文单独阅读可能不太容易理解,因此我建议您从第一部分开始阅读。
在之前的文章中,我们介绍了一些概念,包括:(1)“可验证计算"证明系统(以太坊社区有时不准确地称之为"ZK”),(2)哈希函数,(3)我们用于安全证明的一些理想模型,以及(4)这些"理想模型"是虚假的观点——有时它们会让我们对在现实世界中完全不安全的方案充满信心。
今天我想继续推进,并(更接近地)实际讨论标题中暗示的最新研究成果:Khovratovich、Rothblum和Soukhanov最近发表的题为"如何证明虚假陈述:对Fiat-Shamir的实际攻击"的论文(以下简称KRS)。这篇论文表明,在某种设置下看起来安全的证明方案,实际上可能并不安全。
讨论这篇论文的一种方法是从论文的开头开始,然后向结尾推进。我们不会这样做。相反,我计划采用一种涉及大量跳跃的方法。我的疯狂是有方法的。
在我们到达那里之前,我们需要涵盖一些更重要的背景知识。
背景第一部分:交互式证明系统
我通过重申对称为随机预言机模型范式的某种东西的批评来介绍这些文章,在这种范式中,我们假装哈希函数实际上是随机函数。深思熟虑的密码学家无疑会对此感到不安,因为事实上KRS论文根本不是关于随机预言机的!相反,它展示了密码学家无处不在使用的另一种"启发式方法"的问题:这被称为Fiat-Shamir启发式方法。
虽然Fiat-Shamir与随机预言机模型不同,但两者住在同一个社区,并送他们的孩子去同一所学校。我的意思是:Fiat-Shamir(在非常有限的理论意义上)可以在没有随机预言机模型的情况下存在,但在实践中,两者通常是相互依存的。
因此,为了解释这个新结果,我需要解释Fiat-Shamir的作用。在我能做到这一点之前,我需要解释什么是交互式证明。(如果您已经了解这部分,请随时跳过。)
我们今天使用的许多可验证计算"证明系统"是一类称为交互式证明的协议的成员。在这些协议中,两方,即证明者和验证者,交换消息,以便证明者能够使验证者相信某个给定陈述的真实性(例如"我知道一个输入x能使这个特定程序满意。",并且可能有一个见证w来帮助我证明这一点)在许多情况下,这些协议遵循一种交互模式,形式如下:
- 证明者发送一条"承诺"输入和见证的消息,可能还有其他一些东西。这条承诺消息被发送给验证者。
- 然后验证者生成一个或多个证明者必须回应的挑战。这里发生的确切情况可能因方案而异。
- 然后证明者计算对每个挑战的响应,验证者检查每个响应是否有效(同样,方式高度特定于证明方案)。如果任何响应检查不通过,它会拒绝该证明。
- 双方可能多次重复上述步骤——顺序或并行进行。
是的,我知道我对这些挑战和响应的处理方式非常模糊!事实是,目前我们并不关心。您只需要知道,如果证明者是诚实的——也就是说,如果见证(输入)确实满足程序——那么挑战/响应部分应该对证明者来说很容易回应。如果证明者作弊,即它没有适当的见证,那么它能够正确回应随机挑战的可能性应该很小。
(请注意,我们并不要求作弊的证明者完全无法通过挑战!这就是为什么证明系统经常多次重复挑战/响应阶段:即使作弊的证明者有一次机会以很小的概率作弊成功,我们认为他们多次作弊的概率要低得多。)
您可能会注意到整个设置是:(1) 交互式证明需要大量的(废话)交互。可能不那么明显的是 (2) 它们假设一个诚实的验证者来制定"良好"的挑战。
这种对交互的需求在许多应用中相当烦人。对于像区块链这样的系统来说,这尤其令人恼火,因为可能有数千(或数百万)台计算机都需要验证某个给定陈述(例如,一笔交易)是否正确。如果证明者只能与单个验证者运行一次证明,然后双方可以只发布它们交互的记录,那将容易得多!任何人都可以检查记录以确保证明者正确回答了所有挑战!
不幸的是,这个想法存在一个关键问题!这些协议的安全性依赖于验证者的挑战是随机的,或者至少对证明者来说是高度不可预测的。如果证明者能够以某种方式在步骤(1)中承诺其输入之前预测它将被挑战的值,它通常可以通过在第一条消息中改变其方法来作弊。更具体地说:不诚实的验证者可以通过偷偷地提前让证明者知道挑战来"串通"帮助它证明一个虚假的陈述。因此,至关重要的是:验证者必须是诚实的,并且不与证明者串通。
但这些系统的全部意义在于我们根本不应该信任任何个体!如果我们只是信任人们的行为是诚实的,那么这一切的意义何在?
更多背景:Fiat-Shamir
现在我想带您回到很久以前。一直回到20世纪80年代中期。
早在1986年,两位名叫Amos Fiat和Adi Shamir(上图)的密码学家遇到了一个非常类似的问题。他们有一个交互式证明系统——一个简单得多的系统,毕竟那是20世纪80年代——他们想将他们的交互式证明转变为任何一方都可以验证的非交互式证明。他们考虑了上面描述的记录想法,并意识到它行不通——验证者可以简单地与证明者串通帮助它作弊。为了解决这个问题,他们想出了一个巧妙的解决方案,这个方案优雅、简单,同时也打开了一个我们今天仍在努力填补的理论深渊。
Fiat转向Shamir(我想象)概述了整个问题。Fiat(或Shamir)说:“也许我们可以找到一种方法,让验证者以某种随机但可复现的方式选择挑战——这种方式允许任何人确保挑战实际上是随机和不可预测的。“然后其中一个人说:这听起来很像哈希函数。
Fiat-Shamir启发式方法就这样诞生了。
Fiat和Shamir提出,不是随机选择挑战值,而是"验证者"通过哈希证明者发送的"承诺"消息来选择挑战值,可能还附带其他杂项(例如被证明的"程序"或电路)。然后证明者将回应这些挑战消息,并输出整个证明的记录。
就是这样。这就是整个技巧。
尽管简单,但这种Fiat-Shamir方法有一些明显的吸引人之处:
- 良好的哈希函数通常输出看起来相当"随机"的东西,这正是我们想要的挑战。
- 任何第三方都可以轻松检查记录,只需验证挑战值是否与证明者"承诺"消息的哈希匹配。(换句话说,验证者没有串通或作弊的空间了,因为它现在完全是确定性的。)
关键的是,这里存在一个很酷的"循环"悖论。一个作弊的证明者可能会尝试以下技巧来预测它将被挑战的值。具体来说,它可能 (1) 选择一个承诺消息,然后 (2) 哈希该消息以找到挑战。一旦它知道了挑战值,它可能会尝试改变它在步骤(1)中的输入,以便它更容易在这些特定的挑战点上作弊。但关键的是,这种方法产生了一个悖论……!如果证明者改变了它在步骤(1)中的输入,那将导致一个全新的"承诺"消息!一旦被哈希,那个新的承诺消息将产生一组非常不同的挑战消息,我们的作弊者就陷入了一个它永远无法逃脱的无限时间循环!¹
Fiat-Shamir的伟大之处在于,一旦您的(挑战生成)验证者完全是确定性的,就没有理由甚至让那段代码由一个单独的方运行。证明者可以自己运行所有确定性的挑战生成代码,即执行所有必要的哈希来生成挑战,然后输出最终记录。因此,证明者和(原始)“验证者"代码合并为一个方(我们现在就称之为证明者),而新的验证者是一个检查记录的算法——执行所有必要的哈希和挑战/响应检查以确保一切正常。
由此产生的证明(“记录”)不需要任何交互来验证,因此我们甚至可以将它们发布在区块链上。它们可以被数千或数百万人验证,我们现在准备在上面挂上大笔的钱。
Starknet只是将真钱挂在Fiat-Shamir风格证明系统上的加密货币系统之一。还有其他的!
我打赌你现在要喋喋不休地谈论Fiat-Shamir的可证明安全性了,对吧?
等等,你怎么知道我要谈那个?哦,对了:“你"就是我,所以我只是在回答我自己的问题。(这不是对Fiat-Shamir帮助解决的悖论的一个可爱说明吗!)
我将尽可能快速且无痛苦地完成这部分,但事情是这样的。Fiat-Shamir看起来像个古怪的把戏。我们甚至称它为启发式方法,这实际上就是承认这一点。然而。 literally 有数百篇论文写了关于Fiat-Shamir及其使用方案的可证明安全性。
一般的TL;DR是,Fiat-Shamir通常可以被证明是安全的(对于各种"安全"的定义),如果我们做出一个有用的假设。具体来说:我们使用的哈希函数实际上是一个随机预言机(请参阅此脚注了解更多学究内容!²)我不会深入探讨这个论点,但我只想让你记住随机预言机是如何工作的:
- 在随机预言机模型中,哈希函数是一个随机函数。不精确地说,这意味着(当查询某个新值时)它输出与输入完全无关的随机位。
- 哈希函数"存在于"一个完全独立的称为预言机的方内部。您发送要哈希的东西,如果输入之前没有被哈希过,您会得到不可预测的随机值。
这看起来很像交互式证明设置!简而言之(无意的双关):如果一个适当的方案可以在证明者与诚实验证者(选择随机挑战)交互的设置中被证明是安全的,那么似乎该协议的Fiat-Shamir版本也应该与随机预言机一起工作。随机预言机本质上就像原始交互式方案中的验证者:它生成每个人都可以"信任"是真正随机的随机挑战,然而任何第三方也可以在以后想要检查记录时要求它重现相同的挑战!
对于许多目的,这种随机预言机方法通常工作得还可以。有些人提出了疯狂的理论反例(意思是,精心设计的交互协议在随机预言机模型中是安全的,但在与真实哈希函数一起使用时却崩溃了。)但实践者大多忽略这些,因为它们显然充满了奇怪的废话。
在应用密码学家每天设计新证明系统的现实世界中,我们采用了一种相当标准的模式。一个新的证明系统将首先被指定为一个交互式协议。最终每个人都知道这个证明系统不会以交互方式使用,它将被Fiat-Shamir扁平化并在区块链上使用。然而,作者不会花很多时间争论Fiat-Shamir部分。他们只会描述一个具有正确结构的交互协议,然后他们说类似"当然,这可以通过Fiat-Shamir扁平化,如果我们假设一个随机预言机或类似的东西"的话,然后每个人都点头并在上面存入十亿美元。
但是有一个陷阱,不是吗?
确实,关于这个整个策略有一个主要的星号(*)我现在必须提出。
尽管我们有时可以证明Fiat-Shamir协议是安全的,通常是在ROM中,但这些ROM证明的一个关键特征是,我们(协议的参与者)不知道哈希函数的紧凑描述。这是不可避免的,因为在随机预言机模型中使用的哈希函数是一个巨大的随机函数,不可能以紧凑的形式表达。
在现实世界中,我们自然会用像SHA-3或更令人兴奋的哈希函数(如Poseidon)来替换随机预言机。突然之间,协议中的每个人都会知道哈希函数的一个紧凑描述。正如我上面提到的,这可能导致理论问题。早在2004年,Goldwasser和Tauman(现为Kalai)设计了一个特定的交互协议,当哈希用任何具体哈希函数实例化时,该协议就会爆炸。
但是Goldwasser/Tauman协议非常人为。它在协议描述中做了愚蠢的事情。所以很明显,只要我们不做那些事情,我们可能就没事,也许?
现在的问题是,我们正在部署可以证明 literally 任何合理程序(或"NP关系”)满足性的证明系统。这些程序可能包含Fiat-Shamir哈希函数的实现。在随机预言机模型中,这 literally 是不可能的——所以我们只是假设它不会发生。在现实世界中,这完全可能发生,我们 kind of 必须假设它能够并且将会发生。
事实上,有些电路确实很可能包含Fiat-Shamir哈希函数的实现!原因是因为我在上一篇文章中提到的那些递归证明。
假设我们想构建一个递归证明系统来验证我们的一个扁平化的Fiat-Shamir证明。回想一下,要做到这一点,我们必须获取检查Fiat-Shamir记录的Verify算法,并在一个程序(或电路)中实现它。然后我们需要运行那个程序并生成一个证明,证明我们成功运行了那个程序!而为了让这一切工作,我们确实需要在我们的程序中包含一份Fiat-Shamir哈希函数的副本——这根本不是可选的。
疯狂的是,我们甚至无法在随机预言机模型中证明这些基于Fiat-Shamir的递归证明是安全的!在随机预言机模型中,没有哈希函数的紧凑描述,因此没有我们可以编写的紧凑递归Verify程序/电路。这种递归是完全不可能的。确实,递归的Fiat-Shamir证明只能存在于随机预言机模型之外,在那里我们使用像SHA-3这样的东西来实现哈希函数。但当然,在ROM之外,我们无法证明关于它们安全性的任何东西。结果就是:任何时候你看到一个递归的Fiat-Shamir证明,我们基本上就是把可证明安全性扔出窗外,完全是在YOLO(你只活一次)式地冒险。
这种情况非常糟糕,许多理论家(内心)已经死在了思考这个问题上。
我现在已经写了整整第二篇文章,却还没有谈到我来这里要讨论的KRS结果!还有人读吗?这东西还在运行吗?我真希望如此。
我们现在准备讨论KRS,我将在下一篇文章中立即进行。在我结束这篇文章并为下一篇要解决的大问题做准备之前,请允许我回顾一下我们目前的位置。
- 我们知道Fiat-Shamir可以被证明是安全的,但通常(对于完全的SNARKs来说)只在随机预言机模型中。²
- 一旦我们实际用真实的哈希函数实例化Fiat-Shamir,任何奇怪的事情都可能发生:特别是如果相同的哈希函数在我们想要证明的事情的程序/电路中实现。
- 递归的(Fiat-Shamir)证明实际上要求我们在我们要证明的程序内部实现哈希函数,所以这非常令人担忧。
然而,剩下的是要证明Fiat-Shamir在实践中实际上可能是不安全的。或者更具体地说:存在"邪恶的"程序/电路,可以以某种方式破坏一个使用Fiat-Shamir的完全良好的证明系统。
在下一篇文章中,我将最终讨论这个问题。
注释:
¹ Fiat-Shamir技术当然不能免疫一些明显的攻击。例如:一个作弊的证明者(通常也是"验证者”)可以"研磨"证明——通过尝试第一条消息的许多不同输入,然后对每一个,测试产生的挑战,看看它们是否易于作弊。如果存在小的作弊概率,这种"多次尝试游戏"的方法可以显著提高作弊者在挑战/响应上幸运作弊的概率,因为他们现在有数百万(或数十亿!)次尝试来找到一个幸运的挑战。然而,这里的一个现实假设是,现实世界中的作弊证明者只有有限的计算能力。即使一个证明者可以尝试大量的哈希尝试(比如2^50),你也可以轻松设置你的方案,使得他们成功的概率仍然任意小。当然,不是每个人都完美地做到这一点:我的博士生Pratyush最近合著了一篇很好的论文,关于一些现实世界区块链证明系统所做的参数选择。
² 当我说Fiat-Shamir的可证明安全性依赖于随机预言机模型时,我有点不精确。随机预言机模型通常足以证明关于Fiat-Shamir的声明。但事实上,有一些(相对)近期的结果表明,如何为非常特定的交互协议构建Fiat-Shamir,使用不是随机预言机的哈希函数:这些被称为相关不可约函数。据我所知,不可能使用这些函数来证明基于Fiat-Shamir的、适用于任意(自适应选择)程序/电路的SNARKs。但在这个细节上,我乐于接受指正。