了解 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
