审计零知识证明（ZKP）应用

零知识（ZK）是过时的加密技术吗？是和不是。

围绕 ZK 的市场宣传将其提升为先进的加密技术，这在概念上是相当正确的。ZK 证明系统当然是非常优雅的加密构造。

另一方面，当涉及到一个有效的 ZK 产品时，它们只是半个全景。ZK 框架提供的接口很好地抽象了加密细节，帮助开发者专注于业务逻辑。

一个典型的 ZK 应用程序有两个主要组件。

1. 电路： 这是我们希望为其创建证明的程序的电路表示。这个前端组件编码了应用程序的业务逻辑。
2. 证明系统： 这是应用程序使用的 ZK 证明系统后端。证明系统和框架的选择取决于项目的需求，并影响所使用的前端。

电路实现带来了自身的一系列漏洞分类，与证明系统中可能发现的低级加密漏洞不相干。自然，最 大多数 ZK 团队不会构建自己的框架，而是专注于电路和业务逻辑。由于绝大多数 ZK 审计集中在电路上，且它也是现实中最容易出现漏洞的部分，因此这在很大程度上是我们在此帖子中关注的内容。

我们将描述 ZK 应用程序的审计过程，提出审计期间需要回答的重要问题，并以我们在继续完善审计 ZK 应用程序的过程中发现的一些通用建议作为结尾。

本文假设读者对 ZK 有适度的理解。虽然我们尽量在必要时提供技术背景，我们不会从头介绍诸如公共/私人输入、无效器等概念。这绝不意味着这是一个全面的审计检查列表（如果可能的话），而是一般性指导，可能对 ZK 安全研究人员有用，同时为开发人员提供一些有关我们审计方法的见解。

审计过程

在某种程度上，审计 ZK 电路就像反向思考编程。虽然它看起来类似于计算，但它实际上是一个完全不同的结构，因为 ZK 电路本质上是一组强加于程序执行轨迹的断言（约束）。

考虑以下伪代码：

a = 2
b = 4
c = a + b

让我们关注变量 c。将这一片段解释为伪代码，因为 c 被定义为 a + b，其值根据定义始终保证等于 a + b。然而，如果我们为这个程序编写电路，这种关系将被明确声明。问题是，即使我们跳过这条断言，电路仍然可以正常工作。但是，如果有人输入一个不等于 a + b 的 c 值到电路中会发生什么？由于没有约束强制执行这种关系，该轨迹也会产生有效证明。根据 c 后续的使用情况，轨迹中的其他元素可能完全是无效的，根本不依赖于 a 和 b。然而，验证者会查看证明以为输入必须是有效程序轨迹。换句话说，在 ZK 电路中，所有 必要的变量之间的关系必须明确声明。

考虑以下伪代码示例，

a = 0
b = sha256(a)

相比于以下作为一组断言表示的电路：

a == 0
b == e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855

从技术上讲，值 e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855 等于一个空字符串的 SHA-256 哈希。电路应该是正确的。然而，电路从未表达哈希的实际计算，因此输出的值是任意的。一个确保这种对于 a 和 b 的任意值的计算有效性的电路，不仅需要对哈希函数的输入和输出做出断言，而且对哈希计算过程的每一步都做出断言。

这些是 ZK 工程师在将计算转换为电路时必须牢记的考虑事项。审计涉及认真检查电路中定义的每个约束，以确保翻译是正确的。为此，审计员必须对电路表达的计算以及见证值之间的逻辑关系有深入的了解。

从高层次来看，审计 ZK 电路有两个阶段：

1. 协议设计： 调查电路设计问题以及它如何融入更大的协议。
2. 电路实现： 调查导致电路偏离规范或允许未定义行为的实现问题。

协议设计

对 ZK 应用程序的全面安全审查必须以对核心协议设计的检查为开端。

设计规范在加密上是否合理？

ZK 应用程序通常采用复杂的定制协议，这可能导致新型的加密漏洞。理想情况下，加密协议必须始终呈现出一组定义明确的假设及其附带的安全证明。然而，这对于早期阶段的项目或扩展现有协议的项目通常会被跳过。因此，审计员必须彻底检查所有加密原语的使用、协议中使用的任何固定参数，以及整个协议的合理性。

即使是安全原语，如果在 更大协议中使用不当 或以 不安全的方式配置，也可能引入漏洞。

证明是否泄露了过多的数据？

通过某些设计缺陷，公共输出可能被用来推断本应私有的值信息。这违反了电路的隐私保障，也就是零知识特性。

示例： 在 Aztec 2.0 预发布补丁 中发现了信息泄露。他们去除消费密钥的方法涉及一个账户无效器，破坏了该账户交易的发送者隐私。这是因为静态账户无效器可以被用来通过账户关联交易。此问题通过将密钥去除程序改为使用账户 nonce 代替无效器得以解决。

证明如何融入更大的协议？

ZK 证明如何与电路外组件交互是确保协议端到端安全性的重要因素。电路得到安全实现以及证明验证器正确，这并不足以确保安全。

证明通常如何融入更大的图景？电路接受一些公共和私有输入。有效证明断言这些值之间某种关系。这将私有输入的有效性与公共输入的可公共验证性联系在一起。为了现在考虑一个陈述是有效的，验证者必须执行两个步骤：

1. 验证证明，确保公共输入和私有输入之间的正确关系。
2. 将公共输入与可公共验证值进行检查。这可能涉及对验证者已知值进行计算。

假设证明被正确验证，我们在第二步中仍可能遇到问题。这个步骤中可能遇到的一些主要问题是

• 对公共输入检查所使用的参数的管理员控制可能导致中心化风险。
• 对所有公共输出的验证不够充分。例如，在一电路中证明某个交易在一个块中的成员资格时，如果块哈希本身从未被检查以证明其对应于一个有效块，则证明变得毫无意义。从某种意义上说，公共输出必须充当所有私有输入的承诺，并限制其有效性。
• 如果验证涉及电路外的计算来验证公共输入，电路内外的计算之间可能会存在差异。有时，某些计算的子电路可能与电路外遵循的规范有轻微的偏差。这可能导致有趣的攻击向量。

示例： 这样的一个公共示例可以在 Polygon 的 zkEVM 审计 中找到。这一漏洞的原因是 EVM 和 zkEVM ROM 之间 RLP 解码算法的不一致。RLP 对短字符串和长字符串的解码方式如下：

• 如果字符串长度为 0-5 字节，RLP 编码由一个字节构成，该字节的值为 0x80（十进制 128）加上字符串的长度，后跟字符串。因此，第一字节的范围为 [0x80, 0xb7]（十进制 [128, 183]）。
• 如果字符串的长度超过 55 字节，RLP 编码由一个值为 0xb7（十进制 183）的单字节加上字符串长度的、以二进制形式表示的长度，后跟字符串。例如，1024 字节长的字符串将编码为 \xb9\x04\x00（十进制 185, 4, 0），后跟字符串。这里，0xb9（183 + 2 = 185）是第一个字节，后跟表示实际字符串长度的两个字节 0x0400（十进制 1024）。第一字节的范围因此为 [0xb8, 0xbf]（十进制 [184, 191]）。

然而，电路缺少一个由前缀字节范围实际对应于字符串长度的约束（即，一个字符串可以有一个长度 < 55 但具有 [0xb8, 0xbf] 范围内的前缀，反之亦然）。这个无效的 RLP 编码仍将导致有效证明，攻击将声称转让的资产。然而，协议中的其他契约将无法做到这一点，导致网络暂停。

电路审查

• 完整性问题： 存在有效输入使得电路语句无法证明。这可以被看作是不完整功能。这些问题通常以过度约束的形式出现。
• 健全性问题： 当两个或多个值之间的逻辑关系未被表述为约束时，会出现这种情况。未充分约束的见证值意味着我们可以为无效的见证值集产生有效证明。

完整性问题

过度约束会使电路无法证明，从而导致某些用户或查询的功能丧失。

示例： 在我们对 Scroll zkEVM 的审计期间识别的一个此类问题是在 Poseidon 哈希电路中的过度约束。

Poseidon 表支持两种哈希模式，由变量 mpt_only 表示。如果 mpt_only = true，则表示需要哈希两个字段元素；而 mpt_only = false 则表示变量长度输入。表格在开头有一些自定义行。自定义行被限制为用零填充。如果 mpt_only = false，则预计会有两行自定义行，反之则为一行。

config.s_custom.enable(region, 1)?;
if self.mpt_only {
return Ok(1);
}

这段代码片段的实质是，如果在电路合成期间设置 self.mpt 参数为 true，那么返回值将用于将第二行设置为自定义。

此处的过度约束在于，即使在 mpt_only = true 的情况下，第二行也被标记为自定义。此行本应包含哈希输入，现在被过度约束为零。

因此，任何非零输入的哈希尝试都会失败。

健全性问题

这些无疑是 ZK 电路中最常见的错误。它们难以发现且非常容易被忽视，尽管全面的安全检查清单可能无法做到，但对此采取系统化的处理会大有裨益。我们现在描述我们在审计中反复遇到的一些显著未约束类型，以及一些帮助我们全面有效检查电路的一般技术。

所有变量是否进行了范围检查？

任何不可以是任意字段元素的元素必须在电路中的某些时刻隐式或显式地进行范围检查。

示例： 我们在 Scroll zkEVM 审计期间发现了几项缺失的范围检查，其中一些产生了非常显著的后果。例如，在 RLP 电路中，输入字节未限制为 0-255 范围。

多阶段操作是否得到适当约束？

ZK 电路本质上是确定性的，但某些程序通常需要访问电路内的随机性。实现这种方式是通过将计算分为多个阶段。第一阶段完全确定性。此后每个阶段，我们通过对所有已计算的见证值应用哈希函数来推导一个随机元素（即 Fiat–Shamir 启发式）。

一开始所有纯粹被见证的东西必须在后续阶段受到约束。多阶段电路中推导的随机挑战对于字符串操作和将多列表压缩为单列特别有用。然而，这意味着值的约束必须在多个阶段间强加。

示例： 在我们的一次审计中，我们遇到了一种可能的错误，其中一组值是在第一阶段被见证的。将这些值连接起来必须等于另一个见证元素。此约束必须在第二阶段通过随机线性组合（RLC）强加，但从未执行，从而导致了健全性问题。

可变长度值是否正确处理？

在电路中处理可变长度值是一个棘手的事情。根据我们的经验，在处理可变长度输入的子电路上花时间是重要的。

示例： 我们在 Scroll 中识别到的 RLP 标签计算中的一个问题。RLP 标签的值是使用其组成字节的 RLC 计算的。计算的公式为 bytes_rlc(i+1) =) bytes_rlc(i) * r + byte_value(i+1)，其中 r 是用于计算 RLC 的挑战值。然而，由于它们未能跟踪标签长度，使用空字节填充 RLP 值会导致相同的标签。这是一个关键问题，因为它可以用来伪造 RLP 值之间的相等检查。

电路外计算是否存在逆约束？

往往那些难以在电路中表示的操作都是在电路外计算的，电路内反而断言它们的逆。这是一种优化电路大小的有效策略，但为疏忽创造了更多的表面面积。这里的一个可能性是在将值拿出后再放回电路内，而没有任何等式约束。

示例： 可以在对 Penumbra 的审计中找到一个示例。

impl IncomingViewingKeyVar {
pub fn derive(nk: &NullifierKeyVar, ak: &AuthorizationKeyVar) -> Result<Self, SynthesisError> {
// 省略...
let inner_ivk_mod_q: Fq = ivk_mod_q.value().unwrap_or_default();
let ivk_mod_r = Fr::from_le_bytes_mod_order(&inner_ivk_mod_q.to_bytes());
let ivk = NonNativeFieldVar::<Fr, Fq>::new_variable(
cs,
|| Ok(ivk_mod_r),
AllocationMode::Witness,
)?;

这里，ivk_mod_q 从电路中提取并作为 ivk 重新插入，而没有任何等式检查。这消除了先前施加于其上的任何约束。

未约束的表面区域以及它们常常多么微妙，使得寻找它们的任务非常艰巨。在没有更好的替代方案去遍历和重新遍历所有的约束的情况下，以下是一些有助于让这一过程稍微结构化的建议。

1. 跟踪值之间的直接逻辑关系。 这当然不言而喻，正如开头段落中所讨论的。跟踪逻辑关系是发现未约束关系的关键。
2. 为每个函数列出假设，并查看它们是否在每次调用中得到遵守。 每个函数对其输入都有一些假设。这可以是输入被期望遵循的结构，而没有在函数内部被限制。这些假设必须在对该函数的每次调用中从外部强制执行。
3. 仔细检查未经测试的代码。 虽然这一建议无疑不是 ZK 审计特有的，但缺乏全面测试的代码库部分往往更容易出现漏洞，需要深入查看。

结论

ZK 领域正在快速发展，事情随着时间的推移在所难免。ZK 电路通常是生态系统中非常关键的组件。由于仍然是相对小众的开发领域，审计这些电路往往和编写它们一样困难，因此使得缺乏经验的审计员很容易错过漏洞。高影响力以及对电路进行全面审计所需的高技术复杂性，使得进行全面审计在 ZK 场景中至关重要。在继续引领这一领域的努力中，我们非常高兴能够与更广泛的安全社区分享我们的见解。

关于我们

Zellic 专注于保护新兴技术。我们的安全研究人员发现了最有价值目标中的漏洞，从财富 500 强公司到 DeFi 巨头。

开发者、创始人和投资者信任我们的安全评估，以快速、可靠且没有重大漏洞的方式进行交付。凭借我们在现实世界的攻击安全研究中的背景，我们发现他人未能发现的问题。

‍ 联系我们 获取比其余更好的审计。真正的审计，而不是走过场。

• 原文链接： zellic.io/blog/what-is-a...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～