了解 ZK 证明的安全特性是一项艰巨的挑战。既然我们正在建一个 通用型 zkVM (称为 zkMIPS,因为它将零知识证明与 MIPS 指令集相结合),我们必须考虑开发的每行代码的安全性。
使所有这一切复杂化的是一个更基本的问题,这个问题是区块链技术的核心,尤其是ZK证明:我们首先如何定义安全性?
模糊的描述对任何严格的安全分析都构成威胁。因此,在分析系统的安全性时,我们应该经常问一些基本问题:
除此之外,我们还必须问:我们想要维护的安全特性是什么?这是保密吗?诚信?正确性?不可否认?
下面我们解决第一组问题。我们将在本文的第二部分中回答第二组问题,即将在本频道中发布。
问题 1:关于设置
在 ZKM 白皮书的背景下 (最近发表在 ETHResearch),《零知识》涉及的场景是 可验证的计算 在两方之间,称为 V(验证器)和 P(证明者)。
在这里,验证器有一些计算资源(例如简单的可穿戴设备、智能锁或以太坊第 1 层),而 Prover 代表一个非常大、非常强大的实体(计算机集群,甚至云本身)。
在这种设置下,验证器希望外包计算是很自然的。假设验证器要求验证器计算结果 y 正在运行的程序 F 在输入时 x,如 y=f (x)。但是,验证器不信任验证器,因为验证器可能会发送错误的结果 y',在声称这是正确的同时,为所做的工作收钱,然后消失。
图 1:V 希望将输入为 x 的程序 F 的计算外包。
为了避免这种情况,验证者和证明者同意在外包计算中增加验证。除了结果 y,Prover 还将提供证据(名为 Z) 那个 y 确实是运行程序的结果 C 上 x。
此外,Prover 将进行大量额外计算,以确保 1) 这个证据 Z 很简短,而且 2) 验证了以下内容的正确性 Z 是一种非常有效的算法,这意味着即使是资源很少的验证器也可以轻松执行此项检查。
实现这种可验证计算场景有多种技术,历史上是概率可检查证明(PCP),最近使用SNARKs和STARKs。这些技术的一个共同特征是,它们将计算转换为高度和复杂的多项式,并且验证器只需要对该多项式进行简单的验证即可确信Prover的性能正确。
因此,总体设定是,Prover 想向验证器证明它正确地执行了计算,即 y=f (x)。注意这一点 F、x、y 是协议的输入,为证明者和验证者都知道。请确保不要混淆程序的输入 F,即 x,其中包含协议的输入,即 C、x 和 y。
因此,如果所有这些价值观都是公开的,你可能会问:Prover 的秘密是什么?或者,用ZK术语来说,什么是证人,即证明者拥有的可以证明其主张正确性的数据?在可验证计算的背景下,该见证由证明验证器实际执行了整个计算的数据组成 F 在输入时 x 导致 y,通常称为执行跟踪 T。
图 2:P 通过显示自己知道相应的执行轨迹,向 V 证明其正确计算 F (x),从而得出答案 y。
那么什么是执行追踪呢?在我们正在构建的 zkVM 的上下文中,计算是分步进行的,其总体状态可以通过有限变量列表的值来定义。有效计算是一系列状态,从明确定义的初始状态到某种最终状态,其中每个状态转换都代表一个有效的计算步骤。
它可以表示为一个表,其列代表变量列表,其行代表计算的每个步骤。此表被称为执行跟踪;下图显示了一个玩具示例。
本文的作者杰罗恩·范德格拉夫是ZKM的高级研究顾问。
稍后再回来看看这篇文章的第 2 部分,我们将解答第二组问题,即我们想要在 zkVM(我们称之为 zkMips)中维护的安全属性。
你读过 ZKM 白皮书了吗?在以下地址查看 https://ethresear.ch/t/zkmips-a-zero-knowledge-zk-vm-based-on-mips-architecture/16156
想和我们的核心 ZKM 团队讨论这个话题和其他与 ZK 相关的话题吗?加入我们的 Discord 频道: Discord.gg/bck7HDGCNS
了解 ZK 证明的安全特性是一项艰巨的挑战。既然我们正在建一个 通用型 zkVM (称为 zkMIPS,因为它将零知识证明与 MIPS 指令集相结合),我们必须考虑开发的每行代码的安全性。
使所有这一切复杂化的是一个更基本的问题,这个问题是区块链技术的核心,尤其是ZK证明:我们首先如何定义安全性?
模糊的描述对任何严格的安全分析都构成威胁。因此,在分析系统的安全性时,我们应该经常问一些基本问题:
除此之外,我们还必须问:我们想要维护的安全特性是什么?这是保密吗?诚信?正确性?不可否认?
下面我们解决第一组问题。我们将在本文的第二部分中回答第二组问题,即将在本频道中发布。
问题 1:关于设置
在 ZKM 白皮书的背景下 (最近发表在 ETHResearch),《零知识》涉及的场景是 可验证的计算 在两方之间,称为 V(验证器)和 P(证明者)。
在这里,验证器有一些计算资源(例如简单的可穿戴设备、智能锁或以太坊第 1 层),而 Prover 代表一个非常大、非常强大的实体(计算机集群,甚至云本身)。
在这种设置下,验证器希望外包计算是很自然的。假设验证器要求验证器计算结果 y 正在运行的程序 F 在输入时 x,如 y=f (x)。但是,验证器不信任验证器,因为验证器可能会发送错误的结果 y',在声称这是正确的同时,为所做的工作收钱,然后消失。
图 1:V 希望将输入为 x 的程序 F 的计算外包。
为了避免这种情况,验证者和证明者同意在外包计算中增加验证。除了结果 y,Prover 还将提供证据(名为 Z) 那个 y 确实是运行程序的结果 C 上 x。
此外,Prover 将进行大量额外计算,以确保 1) 这个证据 Z 很简短,而且 2) 验证了以下内容的正确性 Z 是一种非常有效的算法,这意味着即使是资源很少的验证器也可以轻松执行此项检查。
实现这种可验证计算场景有多种技术,历史上是概率可检查证明(PCP),最近使用SNARKs和STARKs。这些技术的一个共同特征是,它们将计算转换为高度和复杂的多项式,并且验证器只需要对该多项式进行简单的验证即可确信Prover的性能正确。
因此,总体设定是,Prover 想向验证器证明它正确地执行了计算,即 y=f (x)。注意这一点 F、x、y 是协议的输入,为证明者和验证者都知道。请确保不要混淆程序的输入 F,即 x,其中包含协议的输入,即 C、x 和 y。
因此,如果所有这些价值观都是公开的,你可能会问:Prover 的秘密是什么?或者,用ZK术语来说,什么是证人,即证明者拥有的可以证明其主张正确性的数据?在可验证计算的背景下,该见证由证明验证器实际执行了整个计算的数据组成 F 在输入时 x 导致 y,通常称为执行跟踪 T。
图 2:P 通过显示自己知道相应的执行轨迹,向 V 证明其正确计算 F (x),从而得出答案 y。
那么什么是执行追踪呢?在我们正在构建的 zkVM 的上下文中,计算是分步进行的,其总体状态可以通过有限变量列表的值来定义。有效计算是一系列状态,从明确定义的初始状态到某种最终状态,其中每个状态转换都代表一个有效的计算步骤。
它可以表示为一个表,其列代表变量列表,其行代表计算的每个步骤。此表被称为执行跟踪;下图显示了一个玩具示例。
本文的作者杰罗恩·范德格拉夫是ZKM的高级研究顾问。
稍后再回来看看这篇文章的第 2 部分,我们将解答第二组问题,即我们想要在 zkVM(我们称之为 zkMips)中维护的安全属性。
你读过 ZKM 白皮书了吗?在以下地址查看 https://ethresear.ch/t/zkmips-a-zero-knowledge-zk-vm-based-on-mips-architecture/16156
想和我们的核心 ZKM 团队讨论这个话题和其他与 ZK 相关的话题吗?加入我们的 Discord 频道: Discord.gg/bck7HDGCNS