Circomlib中的AliasCheck和Num2Bits strict

在 Circom（或任何 ZK circuit 语言）中的别名错误发生在信号的二进制数组编码的数字大于场元素可以容纳的值时。我们在本文中将信号和场元素交替使用。我们将场的特征称为 p。宽泛地讲，p 是信号“溢出”的值。它是所有算术运算中的隐式模数的值。

默认情况下，Circom 将 p 设置为 21888242871839275222246405745257275088548364400416034343698204186575808495617，这需要 254 位来存储。然而，$2^{254} – 1 (\sim2.89\times10^{76})$ 大于默认的 p（$\sim2.18\times10^{76}$）。也就是说，254 位可以编码大于 Circom 信号可以存储的数字。

下面我们绘制数字线，显示这些值在数字线上的位置，近似按比例展示：

0 到 $p – 1$（绿色线段）是 Circom 场元素可以容纳的区间，而 p 到 $2^{254} – 1$（红色线段）是 254 位二进制值可以容纳的值，但场元素无法。

“危险区域”是大于 p - 1 的 254 位二进制值。这些数字位于区间 $[p, 2^{254} − 1]$。在 Circom（默认）的情况下，区间 $[p, 2^{254} − 1]$ 是

[21888242871839275222246405745257275088548364400416034343698204186575808495617, 28948022309329048855892746252171976963317496166410141009864396001978282409983]

为了获取规模的感觉，如果我们计算 $p / 2^{254}$，结果是 0.7561，这意味着一个 p 大约可以容纳 254 位数字可表示的四分之三的数字。

当二进制表示约束溢出时静默失败

为了约束一个二进制数字 $b₀, b₁, …, bₙ$ 等于一个字段元素 v，我们写出以下 算术电路:

$$ b₀ + 2b₁ + … + nbₙ === v $$

同时约束每个 $bᵢ$ 的值为 $0$ 或 $1$。

但是，计算 $v = b_0 + 2 b_1 + … + n b_n$ 是按模 p 进行的。因此，如果计算 $b_0 + 2b_1 + … + nb_n$ 溢出 p，那么我们可以呈现一个二进制数 $b_0, b_1, …, b_n$，其值不是 v ，并创建一个错误的证明。例如，如果我们的模数是 11，那么 2 和 13 被认为是“相等”的，因为 13 模 11 等于 2。

小示例

假设 $p = 11$ 并且我们使用四位表示一个字段元素。这些位可以编码最大为 15 的数字。如果我们将 12 编码为二进制 (1100)，这将在模 11 下评估为 12 mod 11 = 1。所以我们可以声称 1100 是 1 的二进制表示。

具体来说：

$8(1) + 4(1) + 2(0) + (0) == 1 (\mod 11 )$

在 Python 中演示

为了查看攻击者使用的值，下面我们在 Python 中重现 Circomlib 的 Bits2Num 和 Num2Bits 使用的约束，这样这些值就可以轻松打印出来：

p = 21888242871839275222246405745257275088548364400416034343698204186575808495617

## 复制 Num2Bits 和 Bits2Num 使用的约束
def constrain_modulo_p(bits, num, p):
    multiplier = 1
    acc = 0
    for i in range(len(bits)):
        assert bits[i] == 0 or bits[i] == 1
        acc = (acc + multiplier * bits[i]) % p
        multiplier = (multiplier * 2) % p

    # 二进制转换必须是正确的
    assert num == acc

## 这不能在 Circom 中完成，因为 `value` 需要大于 p
## 但小于 $2^{254} - 1$
def malicious_witness_generator(nbits, value):
    bits = []
    for i in range(nbits):
        bit = value >> i & 1

        bits.append(bit)

    return bits

## “正常”情况 -- 约束通过
constrain_modulo_p([1,1], 3, p)

## 对手情况 -- 约束通过，但二进制数不是 3
adversary_bits = malicious_witness_generator(254, 3 + p)
print(adversary_bits)

## 虽然 adversary_bits ≠ 3，但没有触发断言
constrain_modulo_p(adversary_bits, 3, p)

这里重要的是 constrain_modulo_p 接受两个代表 3 的二进制表示：3 的“正确”二进制表示（11），以及它的别名 $3 + p$ — 可以用一个 254 位数字编码。

通过 AliasCheck 和 Num2Bits_strict 与 Bits2Num_strict 预防错误

Circomlib 的 bitify 库 中的“严格”版本位转换模板通过将二进制数组传递给 AliasCheck 模板来防止别名错误。

AliasCheck 模板 接受一个二进制数组，并断言编码的值小于场元素可以容纳的最大值。

pragma circom 2.0.0;

include "compconstant.circom";

template AliasCheck() {

    signal input in[254];

    component compConstant = CompConstant(-1);

    for (var i=0; i<254; i++) in[i] ==> compConstant.in[i];
    // 如果二进制输入大于提供的常量，
    // compConstant 返回 1
    compConstant.out === 0;
}

AliasCheck 使用 -1 来表示 p - 1。compConstant 接受一个二进制输入（可能编码一个大于场元素可以容纳的值），如果小于或等于某个阈值，则返回 0，否则返回 1。

通过将 compConstant 的输出约束为 0，并将比较常量设置为 -1，AliasCheck 禁止大于 p 的二进制数字。

如果二进制数组容纳的位数少于场可以编码的位数，则不存在别名错误的危险

将 Num2Bits 应用于一个场元素还对该数字实施了小于 $2^n$ 的范围检查，其中 n 是位数。例如，如果 n = 4 并且 p 是默认值，如果我们将输入信号设置为 17，则结果不会默默溢出为二进制 1（0001）—电路将不会被满足。

这就是为什么 Circomlib 中的 Num2Bits_strict 和 Bits2Num_strict 硬编码位数为 254 — 这是别名可能出现的值。

这也是为什么 LessThan 模板不允许开发者构建超过 252 位的比较器。这避免了别名错误的潜在误用。

template LessThan(n) {
    assert(n <= 252);
    signal input in[2];
    signal output out;

    component n2b = Num2Bits(n+1);

    n2b.in <== in[0] + (1<<n) - in[1];

    out <== 1-n2b.out[n];
}

如果你更改 Circom 编译器中的默认 p （ -p 选项 ），请确保检查 Num2Bits_strict 、 Bits2Num_strict 、 AliasCheck 和 CompConstant 仍然能防止你出现别名错误，因它们被硬编码以使用 254 位。

找出错误挑战

这是我们在 X 上发布的 CTF（前身为 Twitter），其包含本文描述的错误：

pragma circom 2.1.8;

include ".node_modules/circomlib/circuits/comparators.circom";
include ".node_modules/circomlib/circuits/poseidon.circom";

template UnsafePoseidon(n) {
    signal input in;
    signal output out;

    component n2b = Num2Bits(n);
    component b2n = Bits2Num(n);
    component phash = Poseidon(1);

    n2b.in <== in;
    for (var i = 0; i < n; i++) {
        b2n.in[i] <== n2b.out[i];
    }

    phash.inputs[0] <== b2n.out;
    phash.out ==> out;
}

component main = UnsafePoseidon(254);

上述代码的问题在于，存在多个证人导致相同的哈希，因为允许 254 位，最终导致溢出。

请记住，算术电路的输入不仅是标记为 input 的信号，它是 电路中的每个信号。 Circom 为我们提供了一种类似 C 的友好编程语言，用于根据提供在 input 信号中的值“填充”某些信号，但代码并不是最终约束系统的一部分。

在上述代码中，254 位二进制数组存储在 Num2Bits 的输出信号和 Bits2Num 的输入信号中。

要将错误值注入到用来编码二进制数组的信号中，我们需要使用我们在 破解欠约束 Circom 电路 指南中描述的技术。为了为上述代码生成概念证明，我们采取以下步骤。

1. 使用一个足够小以在范围内有别名的数字 u 生成哈希，即 $[p, 2^{254} − 1]$。
2. 使用相同的数字生成恶意证人并应用于 input in，但重新指定该二进制数组以保存值 u + p。
3. 这两种信号赋值生成的哈希将是相同的，但证人不同。

总之，挑战中的代码可能会因为存在别名错误而遭受第二次预影攻击。

最初发布于 7 月 13 日

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