你的第一个 ZK 漏洞:从零知识到一知识

本文介绍了构建和理解零知识电路的基本心智模型,通过Circom代码示例深入探讨了其核心概念、多项式原理以及零知识证明中常见的约束不足变量漏洞。文章详细解释了信号、约束操作符和二元约束的重要性,并强调了其在零知识证明安全性中的实际影响。

你将在此处学到什么

本文介绍了创建和思考 ZK 电路的基本心智模型。你将从第一性原理探索关键概念,并了解编写或审查 ZK 代码时有时会出现的一个简单但关键漏洞

到最后,你将掌握足够的知识,以便在 ZK 学习之旅或进行 ZK 安全审查时提出有意义的问题,即使你对零知识一无所知。

在文章末尾,你将找到有关这项强大密码学技术的持续学习资源链接。

结构和先决条件

我们将通过一个“简单”的 Circom 代码示例来探索 ZK。

你需要具备以下基本知识:

  • 计算机科学基础:if 语句、循环和或门
  • 初等数学概念多项式的工作原理(例如,理解 $x^2 + 3x = 3$ 是一个多项式,其中 $x$ 可以是任何数字)

理解零知识电路:构建模块

如果暂时不理解代码,请不要担心。这是正常的。

让我们从以下代码开始。它在 Circom 中生成一个电路,用于对 $n$ 比特数字执行按位或操作

这是代码的样子(故意存在 bug):

pragma circom 2.0.0;

// n == 比特数
template BitwiseOr(n) {
    signal input x[n];
    signal input y[n];
    signal input z[n];

    var i;
    for(i = 0; i < n; i++){
        // 或
        x[i]+y[i] === z[i];

        // 二进制约束
        x[i]*(x[i]-1) === 0;
        y[i]*(y[i]-1) === 0;
        z[i]*(z[i]-1) === 0;
    }
}

component main = BitwiseOr(4);

我们所表示的计算是按位或操作。或逻辑门遵循以下真值表:

x y x 或 y
0 0 0
0 1 1
1 0 1
1 1 1

我们正在实现 x 或 y == z。由于我们处理的是比特,所以值只能是 $0$ 或 $1$。

当我们提供有效的输入和输出时,电路接受;否则,它会拒绝。

例如,如果 $x = 0$ 且 $y = 1$,我们必须提供 $z = 1$,电路才会接受。

但电路究竟是什么?暂时可以将其视为一个函数,其结构如下:

// 伪代码 - 非特定语言
function computation(inputs[], outputs[]) -> bool {

    // 作为计算的操作
    result = _computation(inputs[])

    // 检查计算后的输入是否与输出匹配
    if (result == outputs[]) {
        return true   // 有效
    } else {
        return false  // 拒绝
    }
}

这是一个简化的“电路”,表示一个 1 比特的或操作

// 伪代码 - 非特定语言
function computationORGate(x, y, z) -> bool {

    // 计算 (不只是数学运算,检查也算)

    // 当 X 为 0 且 Y 为 0 时的 if 语句
    // 想象一下这里的代码...

    // 我们的示例:X=0 且 Y=1
    if (x == 0 && y == 1) {
        if (z == 1) {
            return true   // 有效
        }
    } else {
        return false      // 拒绝
    }

    // 想象一下其他可能组合的代码...
    // 检查 X 为 1 且 Y 为 0 等等...
}

我们可以用电路表示所有基本的逻辑门(或、与等)。

从本质上讲,你计算机上的每个算法都以逻辑门和其他基本操作作为构建模块运行。这个基础使我们能够编写几乎任何程序。

像虚拟机或哈希函数这样的复杂系统,只是以复杂模式排列的逻辑门,用于执行专门任务。

在物理上,这些算法通过计算机二进制晶体管中的电压表示执行。它们充当逻辑门,通过基本操作操纵信息,最终执行任何算法。

就像开发人员重用代码模块来解决日益复杂的问题一样,我们可以将基本门组合起来创建复杂的算法。这种可组合性使我们能够从更简单的构建块构建复杂的电路,例如表示哈希函数的电路。如果你想看看这在实践中是什么样子,可以看看 circomlib 中的 SHA-256 电路实现。它很复杂,但你会认出相同的模式:模板、信号和约束,一路向下。

Circomlib(我们的主库)

现在你已经理解了这些基础知识,你会发现导航 circomlib GitHub 仓库要容易得多。这个库提供了将算法表示为电路的基本构建块。让我们看看包含逻辑门实现的文件:

https://github.com/iden3/circomlib/blob/35e54ea21da3e8762557234298dbb553c175ea8d/circuits/gates.circom#L37-L43

这是或门的实现,暂时不必完全理解它,只需观察其结构:

template OR() {
    signal input a;
    signal input b;
    signal output out;

    out <== a + b - a*b;
}

有了这些构建块,加上一些专注的努力,也许还有 60 杯咖啡,开发人员最终可以创建像 Poseidon 哈希函数这样的复杂电路。你可以在这里探索它的代码:

https://github.com/iden3/circomlib/blob/35e54ea21da3e8762557234298dbb553c175ea8d/circuits/poseidon.circom

回到我们的“基本”电路:

第 1 步:阅读脚本

太棒了!现在我们对原始代码代表什么以及它如何有用有了清晰的心智模型

让我们一步一步地分解它。阅读 @note 注释:

// @note 这只是告诉编译器使用哪个版本的 Circom。
pragma circom 2.0.0;

// @note `template` 是“函数”,后面跟着它的名称。
// @note 在这个例子中我把它命名为 `BitwiseOr`。但它可以是任何名称,甚至是 SHA256。
// @note 暂时把 "n" 看作一个参数,函数的输入。
// @note 这个 n 是一个自然数:n == 比特数
template BitwiseOr(n) {

    //@note 假装 `signal` 不存在。
    //@note Input 只是输入的意思,很简单。是“函数”的输入。
    //@note x --> 输入变量的名称。[] --> 数组。
    //@note 如果你只想要一个值,你可以不把它做成数组,使用
    //@note --> `signal input x;`。
    //@note 注意,这里 z 也被声明为 `signal input`。
    //@note 通常结果会是一个 `signal output`,但我们
    //@note 故意把它设为输入,以便**调用者**提供
    //@note 期望的输出。这让我们能够展示**恶意调用者**
    //@note 以后如何传递无效值。
    signal input x[n];
    signal input y[n];
    signal input z[n];

    //@note 经典的 for 循环脚本,没什么特别的。
    var i;
    for(i = 0; i < n; i++){

        // @note 将数组的每个成员的值相加
        // @note 并**约束**它与 z 中的对应元素 `===`。
        // @note 但 `===` 是什么?
        // @note 暂时把它看作一个**相等约束**。
        // @note 我们将在第 3.1 步澄清确切含义。

        // 或
        x[i]+y[i] === z[i];

        // @note 更多奇怪的操作。将 X 乘以它自己减 1?
        // @note 然后结果必须 `===` 0?
        // @note 别担心,如果你继续阅读就会明白。

        // 二进制约束
        x[i]*(x[i]-1) === 0;
        y[i]*(y[i]-1) === 0;
        z[i]*(z[i]-1) === 0;
    }
}

// @note Component 就像最终的电路。
// @note 4 是传递给 `n` 的值。
// @note 这个电路叫做 `main`,它等于
// @note 一个名为 `BitwiseOr()` 的“电路”。
// @note 这就是你如何重用电路并实现**可组合性**。
component main = BitwiseOr(4);

第 2 步:多项式反转——signal 是什么

现在让我们为心智模型添加另一层。你可能会想:为什么 Circom 不像我们期望在传统编程中那样使用常规函数参数?

答案在于多项式。是的,那些你在学校学过的数学表达式,例如:

$x^2 + 3x + 69 = 3$

Circom 实际上是一种描述多项式的语言。每个 signal input 都不是编程变量,而是多项式方程中的变量。这是我们思考代码方式的根本转变。

考虑在数学中我们如何写 $f(x) = x^2$,其中 $x$ 是变量。我们可以将其扩展到多个变量,如 $f(x,y,Doge)$,其中我们有三个变量:$x$、$y$ 和 $Doge$。

最令人惊奇的部分是:多亏了一些非常巧妙的数学,几乎任何计算都可以表示为多项式。是的,即使是 Minecraft 理论上也可以表示为多项式。它只会庞大得令人难以置信。

如果你好奇数学如何将计算描述为多项式,本文末尾的资源是一个很好的起点。现在,让我们在不陷入数学细节的情况下继续构建我们的理解。

因此,每当电路被编译或创建时,我们实际上都在生成一个代表我们计算的大多项式

这可以是任何东西,从虚拟机操作码到哈希函数,甚至是“简单”的或门

第 2.1 步:小但扩展知识的细节

这解释了为什么不能将传统脚本逻辑与 signal 一起使用。它不是传统意义上的编程变量,而是最终静态多项式中的变量。

现在我们理解了 signal input,让我们考虑数组如何工作。如果我们只有一个变量,那很简单,但对于数组多项式看起来如何?

对于一个3 比特数字,编译器会创建 3 个独立的变量:$x{bit0}, x{bit1}, x_{bit2}$。对于 $y$ 和 $z$ 也会发生同样的事情。

那我们的或门多项式呢?虽然这是一个复杂的话题,但你可以大致将其可视化为:

$(x{bit0} + y{bit0}) (x{bit1} + y{bit1}) (x{bit2} + y{bit2}) = z{bit1} + z{bit2} + z_{bit3}$

这并不是实际多项式,只是一个简化的表示。有趣的是,Circom 中的任何多项式变量最多只能是二次的。这意味着你会看到像 $x{bit0}^2$ 这样的项,但绝不会看到 $x{bit0}^3$ 或更高次幂。这在设计更复杂的电路时是很有价值的知识,但目前,可以把它看作一个有用的事实来记住。

现在我们已经掌握了更准确的心智模型,让我们回到代码中的一个部分。

第 3 步:理解为什么这里的 + 是一个 OR

// 或
x[i]+y[i] === z[i];

这个 + 符号到底代表什么,为什么它像注释所说的那样充当或操作

请记住,在我们的电路中,$x$ 和 $y$ 是二进制值——它们只能是 $0$ 或 $1$。

让我们分析一下这个真值表中二进制加法 (+) 的所有可能组合:

x y x + y x 或 y 结果
0 0 0 0
0 1 1 1
1 0 1 1
1 1 2 1

现在看看最后一列与加法列的比较。二进制输入+ 操作几乎完全像或逻辑门!唯一的区别发生在两个输入都是 $1$ 的时候。

当我们使用 $===$ 作为相等检查(我们现在使用的简化方式)时,我们正在确认 $x$ 和 $y$ 的和是否等于 $z$。这有效地检查了 $x \text{ OR } y = z$,除了两个输入都是 $1$ 的那个特例。

为了让我们的加法在所有情况下都完美地模仿或门,我们需要一些数学巧妙之处。这正是我们在 circomlib 代码中看到的:

out <== a + b - a*b;

在这里,$a$ 和 $b$ 代表我们的 $x$ 和 $y$ 输入,而 $out$ 是我们的 $z$ 输出。当两个输入都是 $1$ 时,计算变为:$1 + 1 - 1 * 1 = 1$,这给了我们正确的或结果。

对于所有其他输入组合,此公式也产生与或门相同的结果。通过使用这个数学表达式(它将被编译成多项式),我们确保了我们的电路对于所有可能的二进制输入都表现得像一个或门

编译器通过优雅的数学过程将此表达式转换为适当的多项式表示

然后,当你向多项式的变量提供输入,其中 $x \text{ OR } y$ 等于 $z$ 时,电路验证计算并返回有效。如果输入不满足此关系,电路拒绝它们,从而保持我们或门实现的完整性

从技术上讲,+ 在这里是为了简化教育过程而使用的,但这是一个漏洞

x[i]+y[i] === z[i] 不能完全代表一个或门。

第 3.1 步:解密 $===$, $<==$ 和 $<--$

早些时候,我们将 $===$ 简化为“相等检查”。现在我们理解了约束,让我们更精确一些。

在 Circom 中,有三个用于处理信号的关键运算符:

  • $===$ 向电路添加约束。它不赋值。它告诉证明者“这个等式必须成立”。如果不是,则证明无效。
  • $<--$ 向信号赋值,但不添加任何约束。信号获得一个值,但没有任何东西强制执行该值的正确性。
  • $<==$ 兼具两者:它赋值添加约束。它等效于先使用 $<--$ 再使用 $===$。

这种区别对安全性至关重要。请注意,这些失误比你想象的更常见:当本应使用 $<==$(赋值 + 约束)时,却使用了 $<--$(仅赋值)。信号获得了值,所以在测试期间代码“有效”,但没有约束强制执行正确性,恶意证明者可以替换任何他们想要的值。

在我们的 circomlib 或门示例中,$out <== a + b - ab$ 既将结果赋值给 $out$ 又约束了它。如果作者写成 $out <-- a + b - ab$,那么在诚实执行期间输出看起来是正确的,但恶意证明者可以将 $out$ 设置为任何值,电路都会接受。

第 4 步:多项式的用途

这个多项式使得强大的 ZK 声明成为可能,例如:“我知道在这次计算中产生这些特定输出的输入。”

例如,我可以证明我知道输入,当通过一个复杂函数哈希时,它会产生特定的输出。这听起来和你听说过的 ZK 声明很相似吗?

考虑经典的年龄验证示例:我可以证明我年满 18 岁,而无需透露我的实际年龄。用 ZK 的术语来说,我构建了一个代表计算 $myAge > 18$ 的电路,并生成了一个证明,证明这个陈述是真实的,而无需暴露 $myAge$ 的值。

电路(或多项式)接受两个参数:你的年龄和阈值(18)。如果它们满足计算(大于),则返回有效;否则,无效。

这种 $>$ 计算,正如我们对或门所看到的那样,可以通过巧妙地组合基本逻辑门和数学操作来表示。你可以在这里看到 circomlib 库如何实现 GreaterThan比较器circomlib/circuits/comparators.circom

在这个年龄验证电路中,多亏了先进的数学原理,如果你不想暴露计算的输入和输出(即多项式的变量),你就不必暴露。这正是它实现“零知识”的原因。

从技术上讲,ZK 并非仅仅通过编译 Circom 代码来实现。你必须将编译结果转换为 ZK-SNARK 或 ZK-STARK(这涉及更高级的数学)。无论你使用哪种 ZK 数学模型,这个额外步骤才是真正实现零知识的关键。

默认情况下,你在 Circom 中声明的任何 signal 都是私有的。这意味着验证你的计算的任何人都不会知道它的值。例外情况是主组件的输出信号(总是公共的)以及你明确标记为公共的输入信号。

第 5 步:理解其他数学——二进制约束

顺便说一句,我们代码中的那些其他奇怪操作实际上正在强制执行一些关键的事情:确保所有输入都是 $1$ 或 $0$。理解它们如何做到这一点并不复杂。

如果 $x[i]$ 不是 $0$ 或 $1$,那么约束 $=== 0$ 就不会得到满足。你可以通过将不同的值插入 $x[i]$ 来验证这一点。该约束只会在 $x[i]$ 是 $0$ 或 $1$ 时成立。

x x - 1 x * (x - 1) === 0 吗?
0 -1 0
1 0 0
2 1 2
5 4 20

这就是为什么 $x(x-1) = 0$ 优雅地强制执行(约束)所有这些值必须是 $0$ 或 $1$,否则电路将拒绝证明:

// 二进制约束
x[i]*(x[i]-1) === 0;
y[i]*(y[i]-1) === 0;
z[i]*(z[i]-1) === 0;

这些约束并非可选,它们是必需的,因为正如你所看到的,任何人都可以向多项式的变量输入任何值。

在我们的例子中,如表中所示,简化的 + 仅在所有输入变量都是二进制时才表现为(请记住,这个 + 故意存在漏洞,正确的公式是 $x+y - x*y$,但为了解释目的,我们在这里将其简化)。所以我们必须确保它们是二进制的,否则电路将以意想不到的方式运行。而这是另一个漏洞!通常被称为约束不足变量漏洞

想象一下,我们省略了确保电路只接受二进制值的这 3 行。

那么我们可以传递 $x=5, y=3, z=8$,电路会接受它为有效,因为 $5 + 3 === 8$ 满足约束。但这毫无意义:或门只对二进制值($0$ 或 $1$)进行操作,而 $5$、$3$ 和 $8$ 不是布尔操作的有效输入或输出。如果没有二进制约束,没有任何东西能阻止用户输入他们想要的任何值,电路也无法拒绝它。

即使我们使用正确的或公式($x+y - x*y === z$)而不是我们简化的 +,同样的问题也存在。攻击者可以巧妙地解决数学问题,并找到满足方程的输入,但这些输入是无意义的值。例如,假设我们想强制 $z = 100$。由于我们控制所有输入,我们只需选择一个随机的 $x$,比如说 $10$,然后求解 $y$:

$10 + y - 10*y = 100$ $y = -10$

就这样。我们可以传递 $x=10, y=-10, z=100$,我们的电路会很高兴地验证这个证明,尽管它对于二进制或门来说毫无意义。这就是为什么我们必须始终将变量约束到其预期的域。

注意:在实践中,Circom 在有限素数域上操作,因此没有实际的“负”数。值 $-10$ 将表示为一个大的域元素($p - 10$,其中 $p$ 是域素数)。漏洞原理保持不变:攻击者可以找到满足无约束方程的域元素,而这些域元素并不代表有效的或运算

第 6 步:缺少约束的实际影响

想象一下,你正在构建一个将计算证明发送到 L1 的 L2 区块链。为简单起见,假设你的 L2 只执行或操作

如果没有适当的约束攻击者可以构造一个带有 $x=10, y=-10, z=100$ 等值的恶意证明。L1 合约的 verify() 函数将接受这个无意义的证明为有效,这是一个严重的安全故障

风险极高:在 L2 系统中,欺诈性证明可能导致虚假交易攻击者可能声称“Alice 在这个 L2 上给我发了 4 ETH,然后把它桥接到 L1”,这是一个彻头彻尾的谎言,可能导致实际的经济盗窃

现在,综合我们所学到的所有知识,让我们回到我们有 bug 的代码,看看在移除二进制约束后它会是什么样子:

pragma circom 2.0.0;

// n == 比特数
template BitwiseOr(n) {
    signal input x[n];
    signal input y[n];
    signal input z[n];

    var i;
    for(i = 0; i &lt; n; i++){
        // 或
        x[i]+y[i] === z[i];
    }
}

component main = BitwiseOr(4);

如果你在安全审查中遇到这种情况,你会提出两个关键发现

严重:缺少二进制约束。输入信号必须约束二进制值($0$ 或 $1$),以确保电路表现得像一个正确的或门

以及我们之前发现的数学正确性问题

:操作 $x[i]+y[i] === z[i]$ 没有正确实现或门。当两个输入都是 $1$ 时,结果应该是 $1$,而不是 $2$。正确的实现是 $x[i]+y[i]-x[i]*y[i] === z[i]$。

关键要点

  1. 电路是多项式。Circom 代码编译成代表计算的多项式约束
  2. 信号是多项式变量,而非编程变量。它们的行为与你在传统语言中习惯的不同。
  3. 每个信号都必须正确约束。如果未强制执行信号的域(例如,比特的二进制值),电路将接受违反预期计算的输入。
  4. 约束不足的变量是需要注意的漏洞类别。缺少约束、错误的运算符($<--$ vs $<==$)和不完整的域检查是真正漏洞隐藏的地方。

结论

你现在拥有继续独立进行 ZK 之旅所需的基础心智模型

我们探索的漏洞可能看起来很简单,但它们可能出现在生产代码中,就像“简单”漏洞在 Solidity 等成熟生态系统中继续出现一样。

理解这些基本问题是你成为熟练 ZK 开发者或审计员的第一步。

为了加深你的理解,请考虑以下问题:

  • 为什么 Circom 在大约 $2^{254}$ 的素数域上操作?这有什么影响
  • 你如何表示其他逻辑门,如 AND、XOR 或 NOT?
  • 从高层次看,zkSNARK 是什么,它与 Circom 电路有什么关系?
  • 不同约束实现性能影响是什么?

本文仅涵盖我在 RareSkills Circom 训练营 一周内所学知识的一小部分,但它为你独立探索提供了足够的基础。

ZK 技术仍处于早期阶段,具有巨大的潜力和创新空间。这个领域需要更多像你一样好奇的头脑

进一步探索的资源

  • RareSkills ZK 书籍:一个全面、免费的资源,从头开始涵盖 ZK 电路、约束系统和 Circom。
  • Circom 文档:Circom 官方语言参考和指南。
  • circomlib:可重用 Circom 电路(门、比较器哈希函数等)的标准库
  • RareSkills:本文中提及的 Circom 训练营背后的组织。
  • 原文链接: blog.sigmaprime.io/first...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
sigmaprime
sigmaprime
江湖只有他的大名,没有他的介绍。