在 ZK 电路中发现健全性错误的实用指南

在 ZK 电路中寻找可靠性 Bug 的实用指南

零知识证明是区块链扩展和隐私的核心构建块。在实际部署中，最脆弱的部分通常是电路：开发者编写的约束。小的疏忽或“显而易见”的假设会变成可靠性 Bug，让攻击者证明无效的计算。在本文中，我将介绍常见的电路 Bug 类型，以及如何发现它们。

ZK 电路基础知识

在深入研究实际的 Bug 之前，让我们回顾一下我们正在处理的内容。算术电路将计算编码为有限域上的多项式约束系统。电路有三种类型的值：

• 私有输入（见证）：只有证明者知道的值。这些是要证明的“秘密”。
• 公共输入/输出：证明者和验证者都可见的值。这些将证明锚定到具体的对象上。
• 中间信号：证明过程中计算的内部值。

证明者的工作是找到所有信号的值，以使每个约束都得到满足。验证者检查一个简洁的证明，证明这些值的存在，而无需了解私有输入。

编写电路的一种常用语言是 iden3 的 Circom。让我们从一个简单的 Circom 示例开始，该示例检查输入是否等于零（你可以将代码复制/粘贴到 zkREPL 中进行测试）。

pragma circom 2.1.6;

include "circomlib/poseidon.circom";

template IsZero() {
  signal input in;
  signal output out;
  signal inv;

  inv <-- in != 0 ? 1/in : 0;
  out <== 1 - in*inv;
  in*out === 0;
}

component main { public [ in ] } = IsZero();

/* INPUT = {
    "in": "0"
} */

这里有一个关键的区别：<!-- 仅在 witness 生成期间运行。它计算一个值，但不会以任何方式将该值绑定到电路。 相比之下，<== 和 ===确实发出多项式约束：它们将你的意图转化为证明者必须满足并且验证者最终执行的方程式。

可以这样理解：witness 生成为所有信号生成候选赋值。约束是使该赋值可检查的规则。如果在 witness 生成中计算出一个值但从未受到约束，则它实际上是未约束的自由度，因此恶意证明者可以换入任何方便的值，同时仍然满足电路的其余部分。

让我们来追踪一下 IsZero 的工作方式。该模板接受一个输入 in 并产生一个输出 out。还有一个中间信号 inv。

首先，witness 生成计算 inv。如果 in 非零，则 inv 变为其乘法逆元（字段中的 1/in）。如果 in 为零，则 inv 设置为 0。

然后我们有两个约束：

• out <== -in * inv + 1 约束 out 等于 -in * inv + 1
• in*out === 0 要求 in 或 out 之一为零

如果 in 非零，则 inv = 1/in，因此 out = -in*(1/in) + 1 = -1 + 1 = 0。满足第二个约束，因为 out = 0。

如果 in 为零，则 out = -0*inv + 1 = 1。满足第二个约束，因为 in = 0。

恶意的证明者不能在这里作弊，因为任何偏离正确值的偏差都会违反其中一个约束。例如，如果 in = 5 并且恶意的证明者试图设置 out = 1（声称 5 等于零），则约束 in*out === 0 将失败：5*1 = 5 ≠ 0。

约束不足的电路

常见的 zk 失败是开发者计算出了正确的值，但忘记添加显式约束。在这种情况下，证明仅显示“存在一些满足的赋值”，而有意义的输出仍然由攻击者控制。

这是一个基本的 Bug 提款电路示例。给定 oldBal 和提款 amount，电路的公共输出 newBal 应该完全是 oldBal - amount（并且还强制执行 amount <= oldBal）。陷阱是计算正确的新的余额，但从未将其绑定到公共输出。

pragma circom 2.1.6;

include "circomlib/comparators.circom";

template WithdrawBug(n) {
  // public inputs: oldBal, amount, newBal
  signal input oldBal;
  signal input amount;
  signal input newBal;
  // Enforce amount <= oldBal (so this isn't just "overdraft")
  component le = LessEqThan(n);
  le.in[0] <== amount;
  le.in[1] <== oldBal;
  le.out === 1;
  // Compute the correct next balance...
  signal computedNew;
  computedNew <== oldBal - amount;
  // BUG: computedNew is never constrained to equal newBal.
  // The prover can claim ANY newBal and still satisfy constraints.
}

component main { public [ oldBal, amount, newBal ] } = WithdrawBug(32);
/* INPUT = {
  "oldBal": "100",
  "amount": "40",
  "newBal": "100"
} */

由于缺少了一个等式，证明者可以在声称存储的余额保持在 100 的情况下提取 40。然后他们可以再次这样做，一次又一次。这是 zk 版本的在局部变量中计算正确的值，但将攻击者控制的值写入存储。

要解决此问题，我们添加实际的约束：

pragma circom 2.1.6;

include "circomlib/comparators.circom";

template WithdrawFixed(n) {
(...)
  computedNew <== oldBal - amount;
  // FIX: bind the public output the verifier/contract uses
  newBal === computedNew;
}

有限域中的算术边界情况

有限域算术不是整数算术。在 SNARK 内部，每个信号都存在于一个域中，并且相等性以素数为模进行检查。如果你的应用程序逻辑假定为整数（尤其是除法、比较、范围），则必须显式约束整数语义。否则，你证明的陈述与你想象的不同。

例如，一个非常诱人的“除法”小工具仅强制执行代数恒等式 a = b * q + r。但这是有限域中的一个陈述，而不是你可能想要的整数除法语义。在下面的 Bug 电路中，q 被表示为商，但证明者可以自由选择任何 r 使等式成立，即使 r 大于 b。

pragma circom 2.1.6;

template DivBug() {
  // public inputs: a, b, q
  signal input a;
  signal input b;
  signal input q;
  // private witness: r
  signal input r;

  // BUG: this alone does not define integer division
  a === b*q + r;
}

component main { public [ a, b, q ] } = DivBug();
/* INPUT = {
  "a": "13",
  "b": "5",
  "q": "1",
  "r": "8"
} */

例如，对于 a = 13 和 b = 5，witness q = 1, r = 8 满足 13 = 5·1 + 8，因此证明通过验证，尽管 q = 1 不是 floor(13/5)。

解决方法是约束缺少的语义：将值范围限制为预期的位宽，并强制执行 0 ≤ r < b（通常 b ≠ 0），以便 q 和 r 实际上代表整数除法。

pragma circom 2.1.6;

include "circomlib/bitify.circom";
include "circomlib/comparators.circom";

template DivFixed(n) {
  signal input a;
  signal input b;
  signal input q;
  signal input r;

  // Still required

  a === b * q + r;

  // Treat them as n-bit integers (common "bridge" to integer semantics)
  component aBits = Num2Bits(n); aBits.in <== a;
  component bBits = Num2Bits(n); bBits.in <== b;
  component qBits = Num2Bits(n); qBits.in <== q;
  component rBits = Num2Bits(n); rBits.in <== r;

  // Reject b = 0 (if required by spec)
  component bz = IsZero();
  bz.in <== b;
  bz.out === 0;

  // Enforce 0 <= r < b
  component lt = LessThan(n);
  lt.in[0] <== r;
  lt.in[1] <== b;
  lt.out === 1;
}

component main { public [ a, b, q ] } = DivFixed(32);
/* INPUT = {
  "a": "13",
  "b": "5",
  "q": "2",
  "r": "3"
} */

要点是：电路仅强制执行你显式约束的内容。 你忽略的每个“显而易见”的假设都会受到证明者的控制。

在普通代码中，你可以依赖类型、控制流和运行时的整数语义； 在 ZK 电路中，除非你将其编码为约束，否则这些都不存在。

真实案例研究：Kakarot

让我们看一个我在审计竞赛中提交的更复杂的例子。目标是 Kakarot，一个用 Cairo 编写的 zkEVM。 Cairo 的基本数字类型是 felt（一个域元素），因此代码库中充满了将 felts 转换为字节和 ABI-friendly 编码的转换例程。其中一个助手是 felt_to_bytes_little()，它将 felt 转换为小端字节数组，并被其他转换（felt_to_bytes()，各种 uint256_to_bytes*() 助手，bigint_to_bytes_array() 等）重复使用。这些助手出现在 get_create_address() / get_create2_address() 等位置，因此如果你可以欺骗它们的输出，你最终可以欺骗派生的地址。

核心循环如下所示：

body:
let range_check_ptr = [ap - 3];
let value = [ap - 2];
let bytes_len = [ap - 1];
let bytes = cast([fp - 4], felt*);
let output = bytes + bytes_len;
let base = 2 ** 8;
let bound = base;

%{
    memory[ids.output] = res = (int(ids.value) % PRIME) % ids.base
    assert res < ids.bound, f'split_int(): Limb {res} is out of range.'
%}
let byte = [output];
with_attr error_message("felt_to_bytes_little: byte value is too big") {
    assert_nn_le(byte, bound - 1);
}
tempvar value = (value - byte) / base;
tempvar bytes_len = bytes_len + 1;
jmp body if value != 0;

该函数使用证明者端的提示将下一个字节写入内存，范围检查它是否为一个字节（<= 255），然后更新 value = (value - byte) / 256 并重复，直到 value == 0。 错误在于电路永远不会强制执行提示的字节对于当前 value 是正确的字节。

我们现在可以触发有针对性的字段下溢。 在循环结束时，剩余的 value 很小。 如果剩余的值为 1，但证明者使提示返回 2，则 value - byte 会模 STARKNET_PRIME 包装成一个巨大的值。 循环条件是 value != 0，因此循环继续运行而不是终止。

在随后的迭代中，证明者可以继续返回基本上任意的字节。 它们不必对应于原始输入 felt; 它们只需要最终将 value 引导回某个点的零，以便该函数终止。

证明者可以根据需要进行多次迭代，但还有一个额外的障碍：bytes_len 必须以一个“特殊”值结束才能通过该函数的最终最小长度检查。 在这里，利用变得非常有趣。 该函数通过从偏移量为 bytes_len 的 pow256_table 读取边界来检查 bytes_len 是否为表示原始值所需的最小长度。 此表访问可以落在代码段中的某个位置，并且恶意证明者可以瞄准 Cairo 字节码恰好包含零的任何附近位置。 如果 pow256_table[bytes_len] 解析为 0，则对于几乎任何 initial_value，边界检查都变得很容易满足。

在概念验证中，我转储了部分内存段，并在代码段中找到了多个包含零的偏移量，然后暴力破解了停止点，直到最小长度检查可靠地通过。 如果你想要完整的 PoC，请参阅竞赛提交。

真实例子：zkSync Era

2023 年 9 月，ChainLight 披露了 zkSync Era 的 ZK 电路中的一个关键可靠性漏洞。 该 Bug 允许恶意证明者为无效执行的区块生成“证明”，L1 上的验证者合约会接受这些证明。 Matter Labs 部署了一个修复程序并向 ChainLight 奖励了 5 万美元 USDC。

zkSync Era 是一个 ZK-rollup，它运行一个 ZK-EVM：一个零知识电路，用于验证类似 EVM 的执行。 该电路必须确保每个状态转换都严格遵循 VM 语义。 任何偏差都可能允许攻击者执行无效的交易。

电路需要正确处理的一件事是内存。 在正常的 VM 上，当你存储一个值并在以后加载它时，你期望一致性。 在 zkSync 的 EraVM 中，内存操作表示为“内存查询”，并在以后打包并在电路中检查。

这里的 Bug 是约束不足值主题的另一个变体：电路构造了一个 LinearCombination，很明显是为了强制执行一种关系，但实际上从未将其转化为约束.

在处理内存写入指令时，zkSync 的电路代码从一个 256 位寄存器值构造一个 MemoryWriteQuery，然后将其转换为打包的 RawMemoryQuery。

一个 256 位的 Register<E> 存储为两个 UInt128<E> limbs (lowest_128 和 highest_128)。 当构造 MemoryWriteQuery 时，代码进一步将 highest_128 分成两个 u64 chunks (u64_word_2, u64_word_3)，然后构建一个线性组合，看起来它试图执行：

u64_word_2 + 2^64 * u64_word_3 == highest_128

以下是相关代码：

pub(crate) fn from_key_and_value_witness<CS: ConstraintSystem<E>>(
  cs: &mut CS,
  key: MemoryKey<E>,
  register_output: Register<E>,
) -> Result<Self, SynthesisError> {

  let [lowest_128, highest_128] = register_output.inner;

  let tmp = highest_128
    .get_value()
    .map(|el| (el as u64, (el >> 64) as u64));

  let (u64_word_2, u64_word_3) = match tmp {
    Some((a, b)) => (Some(a), Some(b)),
    _ => (None, None),
  };

  let u64_word_2 = UInt64::allocate_unchecked(cs, u64_word_2)?;
  let u64_word_3 = UInt64::allocate(cs, u64_word_3)?;
  let shifts = compute_shifts::<E::Fr>();
  let mut minus_one = E::Fr::one();

  minus_one.negate();
  let mut lc = LinearCombination::zero();

  lc.add_assign_number_with_coeff(&u64_word_2.inner, shifts[0]);
  lc.add_assign_number_with_coeff(&u64_word_3.inner, shifts[64]);
  lc.add_assign_number_with_coeff(&highest_128.inner, minus_one);
  // BUG: lc is never enforced
  ...
}

请注意，约束仅由采用 cs 参数并实际发出 gates 的函数生成。 这段代码永远不会这样做。 它永远不会调用类似 lc.enforce_zero(cs) 的东西，并且它永远不会将 lc 转换为约束值。 因此，“拆分正确性”关系没有被强制执行。

后来，MemoryWriteQuery::into_raw_query 将写入查询的各个部分打包到 RawMemoryQuery 中：

• lowest_128 和 u64_word_2 被打包到 value 中
• u64_word_3 存储为 value_residual

pub(crate) fn into_raw_query<CS: ConstraintSystem<E>>(
  &self,
  cs: &mut CS,
) -> Result<RawMemoryQuery<E>, SynthesisError> {
  let shifts = compute_shifts::<E::Fr>();
  let mut lc = LinearCombination::zero();

lc.add_assign_number_with_coeff(&self.lowest_128.inner, shifts[0]);
  lc.add_assign_number_with_coeff(&self.u64_word_2.inner, shifts[128]);

  let value = lc.into_num(cs)?;

  let new = RawMemoryQuery {
    timestamp: self.timestamp,
    memory_page: self.memory_page,
    memory_index: self.memory_index,
    rw_flag: Boolean::constant(true)
    value_residual: self.u64_word_3,
    value,
    value_is_ptr: self.value_is_ptr,
  };
  Ok(new)
}

由于先前的重组约束不存在，证明者可以有效地篡改由这些拆分组件表示的高位，同时仍然生成验证的证明。 这个 Bug 允许证明者任意更改由存储指令存储在内存中的任何值的高 128 位，而不会更改证明的有效性。

在 L2 上，zkSync 燃烧 msg.value，然后构造一个字节消息来编码提款并将其发送到 L1：

function withdraw(address _l1Receiver) external payable override {
  uint256 amount = _burnMsgValue();
bytes memory message = _getL1WithdrawMessage(_l1Receiver, amount);
  L1_MESSENGER_CONTRACT.sendToL1(message);
  emit Withdrawal(msg.sender, _l1Receiver, amount);
}
function _getL1WithdrawMessage(address _to, uint256 _amount) internal pure returns (bytes memory) {
  return abi.encodePacked(IMailbox.finalizeEthWithdrawal.selector, _to, _amount);
}

关键的细节是 abi.encodePacked(...) 将消息物化在内存中。 编译后的 EraVM 代码使用 st.1 内存存储将选择器、_to 和 _amount 写入堆内存。 在存储 _amount 时，VM 执行未对齐的存储，EraVM 将其转换为两个对齐的 MemoryWriteQuery:

/// store `_amount` parameter into memory at `r1+56`
st.1    r2, r5

// misaligned store -> translated into two aligned write queries:
{
  memory_page: CUR_HEAP_PAGE,
  memory_index: (r1 + 56) // 32,
  value: (uint256(_to) << 64) | (_amount >> 192)
},
{
  memory_page: CUR_HEAP_PAGE,
  memory_index: (r1 + 56) // 32 + 1,
  value: (_amount << 64)
}

一旦你可以篡改由存储指令写入的值的高位，你就可以直接瞄准编码的 _amount。 有关完整的利用细节，请参阅 ChainLight 的文章。

结论和 ZK 电路审计清单

我们现在已经看到相同的故障模式以不同的变体出现：代码计算出某些东西但没有将其绑定到输出，依赖于“显而易见”的属性（如整数除法语义）而没有定义显式约束。 在普通软件中，缺少检查可能会导致恢复或奇怪的边缘情况，你可以在事后进行修补。 在电路中，情况恰恰相反：证明者可以选择 witness，因此缺少检查就变成了自由度，它可能变成无效计算的可伪造证明。 作为审计员，请务必检查以下事项：

• 首先编写证明应该建立的确切陈述。 明确什么是公共的，什么是私有的，以及有效的含义（状态转换、签名有效性、余额更新、Merkle 包含等）。 大多数电路 Bug 发生的原因是作者只确保“程序运行”，而验证者实际上检查“某些 witness 满足这些约束”。
• 端到端绑定每个安全关键值。 跟踪验证者/合约使用的任何内容（公共输出、根、哈希、calldata/消息字节、amount、to、index、nullifier 等），并确保它显式地约束到内部计算。 危险信号是永远不会等于公共值的计算值，或者来自仅进行范围检查的 witness 的“输出”。
• 假设所有 witness 和提示都是恶意的，然后消除自由度。 对于每个 witness 派生的中间值，询问“证明者可以在不违反约束的情况下随意设置此值吗？”。 这是你捕获丢失的相等性、构建但从未强制执行的线性组合以及对于某些选择器值或排序边缘情况不触发的条件约束的地方。
• 使语义与现实世界相匹配：整数、字节和控制流不是免费的。 只要应用程序逻辑假定为整数（范围、比较、除法/模数/余数、字节打包、ABI 编码），你就必须显式地范围限制和约束语义（r < b，除非允许，否则没有除以零，正确的字节序/规范编码）。 同样，任何选择器/标志/操作码都必须是布尔约束的，并且必须正确地门控约束，因此攻击者无法“关闭”检查。
• 用英语攻击电路，然后将其映射到丢失的约束。 对于每个高风险区域（输出、哈希/Merkle、状态链接、算术边缘情况、填充/最后一行逻辑），尝试描述一个伪造的 witness，它可以在改变含义的同时通过（“提取更多”、“欺骗地址”、“重用 nullifier”、“读取写入 A 后的值 B”）。 如果你可以清楚地表达作弊行为，你通常可以找到使其成为现实的一个缺失的约束或门控条件。

• 原文链接： muellerberndt.medium.com...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～