介绍zekrom：面向zk-SNARK电路的算术化结构库（第二部分：Halo2）

zekrom是一个面向zkSNARK电路的算术化结构的开源库，由Kudelski安全研究团队的Laurent Thoeny在其硕士论文工作中创建。zekrom的目标是双重的：分析使用现代库（如arkworks-rs和Halo2）的电路新结构的性能，并为隐私保护应用提供即用型结构。本文介绍了基于Halo2的zekrom，它提供了Griffin、Neptune、Rescue Prime和Reinforced Concrete哈希结构。此外，还包括认证加密原语Ciminion以及使用最近提出的SAFE API的Neptune和Griffin的相应AE结构。

引言

zk-SNARK是创建隐私保护应用的强大构建块，因为它们允许我们在不透露任何信息的情况下使他人相信某个陈述是真实的。因此，能够从zk-SNARK中受益的主要应用是那些涉及一方（通常不受信任）需要证明其采取的某种行动的责任或遵守强制执行策略的情况。最近涉及zk-SNARK的提案证明了漏洞的存在、机器学习模型的属性以及网络设备对加密策略的遵守。

在本文中，我们介绍了基于Halo2证明系统的zekrom。在撰写本文时，它提供了以下哈希结构：Griffin、Neptune、Rescue Prime和Reinforced Concrete。此外，它还使用最近提出的SAFE API提供了Neptune和Griffin的相应认证加密结构。请注意，SAFE API在本系列文章的第一部分中介绍。

基于zk-SNARK的典型应用需要专门为电路设计的哈希和/或加密原语。在设计zk-app时，我们可以决定使用低级库（如gnark或arkworks）自己编写电路。此外，我们可以使用DSL（如circom和Leo）。另一方面，我们可以依赖一个gadget库，如zekrom和circomlib。我们创建zekrom就是为了满足这一需求。此外，我们的库还用于研究实现这类新结构（即所谓的算术化导向原语）的复杂性，以及它们在Halo2等最先进库中的性能。

Halo2

过去，我们曾在提供Groth16、PlonK和Marlin证明系统的生态系统中实现了算术化导向的方案。在这篇博客文章中，我们介绍了基于Halo2的zekrom。

Halo2相对于上述证明系统具有许多优势：

1. TurboPlonK自定义门

在TurboPlonK中，作者提出了对PlonK原始约束的修改，以支持自定义门。在PlonK中，门由乘法和加法操作组成。电路约束被编码在所谓的vanilla PlonK约束中，定义为：

[ q_L \cdot a + q_R \cdot b + q_O \cdot c + q_M \cdot (a \cdot b) + q_C = 0 ]

在这种情况下，( q )-型多项式与选择器相关（即，它们允许我们在约束中切换和激活某个操作），而( a, b, c )-多项式与见证相关。创建加法门意味着将( q_M )设置为0，( q_L )和( q_R )设置为1，( q_O )设置为-1。这将允许我们检查输入( a )和( b )是否等于( c )：( a + b = c )。另一方面，乘法门通过将( q_M )设置为1，( q_O )设置为-1，( q_L )和( q_R )设置为0来实现。

相反，TurboPlonK提供自定义门作为原始PlonK门的线性组合，这些门一起被验证。

2. 支持查找参数

在zk-SNARK电路中使用诸如SHA-256等结构的一个限制是使用位操作，这些操作使用可用的场操作实现起来很昂贵。然而，我们可以依赖查找表来实现这类操作。首先，我们将值加载到与电路执行轨迹相关的表中。然后，我们证明一对值作为见证出现在表中，根据表中的其他列。这也可用于证明电路中使用的常量集是正确的。类似地，我们可以在电路中实现XOR操作。此外，我们可以证明我们使用了正确的哈希结构轮常量。此外，诸如Reinforced Concrete等结构依赖查找表的支持来优化性能方案和定义约束。

3. 证明递归

zk-SNARK领域的递归意味着在另一个zk-SNARK中验证zk-SNARK证明：我们证明我们知道一个zk-SNARK，其证明验证过程结果是正确的。zk-SNARK是简洁的（证明材料短且通常验证速度快），我们可以通过递归利用这一属性：递归zk-SNARK包含更多知识，其验证时间不昂贵。

为了支持递归，Halo2使用两条曲线（统称为Pasta曲线）：Pallas和Vesta。Halo2依赖在两条曲线但不同标量场中实例化的证明系统，创建一个2-循环。他们在曲线( E )上实例化Halo2证明系统，定义在域( \mathbb{F}_q )上。这允许使用( \mathbb{F}_r )算术的电路证明语句，也称为标量场。然而，由于验证器相关的算术通常在( \mathbb{F}_q )上执行，Halo2团队构建了另一条曲线，其标量场在( \mathbb{F}_q )中，并使用具有( \mathbb{F}_q )算术的电路来验证第一条曲线的证明。为了完成循环，第二条曲线有一个基域在( \mathbb{F}_r )上，用于生成可以在第一条曲线的( \mathbb{F}_r )电路中验证的证明。

4. 可信设置

零知识证明协议通常需要可信设置过程，其中生成协议的标准参数。通常，这涉及某种类型的多方计算协议，其中生成随机性（也称为有毒废物）。如果随机性没有相应删除并被攻击者捕获，它可以创建将被接受为有效的假证明。

Halo2通过使用内积论证（IPA）多项式承诺方案（PCS）消除了可信设置的需要。多项式承诺方案用于证明多项式在特定点的值通过证明满足( P(z) = y )，而不揭示完整多项式，即我们可以在不揭示整个多项式的情况下打开多项式的某些评估。这在zk-SNARK中对于证明语句的有效性至关重要，该语句被转换为电路（给定一组公共和私有输入）并编码为一组多项式。

尽管IPA产生更大的证明（特别是对数复杂度与PlonK使用的KGZ PCS中的1个群元素相比），但这一缺点在Halo2中通过证明系统聚合许多证明打开的能力得到平衡。

在Halo2中定义电路

过去，我们看到了如何在DSL（如Circom）和嵌入式DSL（如gnark）中定义电路。通常，我们从根据公共和私有输入以及我们执行的操作类型（门）来描述电路开始。

在Halo2中，这个过程是不同的。我们需要使用执行轨迹的概念，即电路从输入到输出生成的所有步骤。执行轨迹表示为( n )列和( m )行的矩阵。每个单元格中的元素属于有限域元素。我们可以将此表的列视为我们在电路中使用的输入类型。Halo2定义了不同类型的列：

• 实例列：它们是证明者和验证者共享的输入，也称为公共输入。
• 建议列：它们包含证明者选择的私有输入（见证）。
• 固定列：它们包括常量等值，并且可以定义电路的逻辑。

例如，我们可以定义基于Griffin的认证加密方案的列如下：

1
2
3
4
5
6
7

pub struct GriffinAECircuitVestaConfig {
    pub message_input: Column<Advice>,
    pub key_input: Column<Advice>,
    pub nonce: Column<Advice>,
    pub output: Column<Advice>,
    pub config: GriffinConfig<Fq>,
}

对于我们电路中涉及的每个操作，我们创建自定义门，其中涉及不同的选择器并具有某些约束。我们通过Rotation类型访问表中的不同单元格。例如，我们可以为Griffin的M层创建自定义门：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

meta.create_gate("M layer of Griffin", |meta| {
    let s = meta.query_selector(m);
    let x = state.map(|v| meta.query_advice(v, Rotation::prev()));
    let y = state.map(|v| meta.query_advice(v, Rotation::cur()));
    let c = round_constants.map(|c| meta.query_fixed(c, Rotation::prev()));
    let sum = x[0].clone() + x[1].clone() + x[2].clone();
    vec![
        s.clone() * (y[0].clone() - (x[0].clone() + sum.clone() + c[0].clone())),
        s.clone() * (y[1].clone() - (x[1].clone() + sum.clone() + c[1].clone())),
        s * (y[2].clone() - (x[2].clone() + sum + c[2].clone())),
    ]
});

Reinforced Concrete

Reinforced Concrete（RC）是一种用于电路和本机架构的哈希函数，它利用了诸如Halo2等新型证明系统提供的查找优势。它依赖三个组件或层：Bars（一个可以使用查找表表示的非线性层）以及Concrete和Bricks组件用于创建扩散。

RC置换处理3元素状态（( s_0, s_1, s_2 )）对于素数( p )。

RC置换对状态应用以下操作：Concrete → Bricks → Concrete → Bricks → Concrete → Bricks → Concrete → Bars → Concrete → Bricks → Concrete → Bricks → Concrete → Bricks → Concrete。

RC置换的不同组件是：

• Bricks：Bricks定义如我们在Griffin中看到的：Bricks ( (s_0, s_1, s_2) = (s_0^5, s_1^5, s_2^5) ) 其中( 5 )不是二次剩余。在这种情况下，( 5 \in \mathbb{F}_p )，其中( p )如我们过去已经看到的。
• Concrete：它包括将状态乘以3×3维的MDS矩阵，即循环矩阵( M )，随后添加一个（伪随机）向量轮常量( c )。
• Bars：定义为Bars ( (s_0, s_1, s_2) = ) (Bar(( s_0 )), Bar(( s_1 )), Bar(( s_2 )))。在Bar函数中，每个域元素被分解并应用替换盒，然后再次组合结果。在这方面，RC提供表和一组查找约束，因此可以证明给定( y = ) Bar(( x ))当且仅当满足约束集。

zekrom for Halo2的性能

为了获得zekrom for Halo2的性能，我们使用了具有32.0 GiB内存的Linux笔记本电脑，配备i5-8250U CPU，使用criterion-rs。

性能结果以毫秒为单位，针对一条、两条和三条消息（m）。

哈希函数

证明性能

验证性能

认证加密函数

证明性能

验证性能

zekrom for Halo2可以从我们的Github仓库下载。

致谢

• 0xPARC基金会
• Dmitry Khovratovich和Roman Walch