探索 ZK 框架:用 5 种不同的 ZK 语言实现的 Mastermind 游戏

  • Veridise
  • 更新于 2024-11-14 17:07
  • 阅读 344

探索 ZK 框架:用 5 种不同的 ZK 语言实现的 Mastermind 游戏

在 Veridise,我们不断探索零知识密码学和框架的新前沿。除了我们的安全审计和工具开发外,我们偶尔还会进行工作组,以保持对新兴技术的了解。我们最近的一个工作组专注于 ZK 语言和应用,因为我们有兴趣比较不同的 ZK 语言和框架。

我们决定在五种不同的 ZK 语言/框架中实现经典的 Mastermind 桌面游戏:Circom、Gnark、Noir、Halo2 和 Arkworks。我们着手实现这个游戏,以评估这些不同 ZK 语言的能力和特性。在这篇博客文章中,我们将分享我们的经验和见解。

你可以在 这个 GitHub 仓库 中找到我们用五种语言/框架编写的 Mastermind 游戏代码。

Mastermind 游戏和研究目标:

对于不熟悉该游戏的人,这里是 Mastermind 规则的快速回顾(存在变体,但这套规则似乎是最常见的):

  • 代码制造者创建一个由 4 个彩色钉子组成的秘密代码。
  • 代码破译者的目标是在(通常)10 次尝试内猜出代码。
  • 代码破译者开始猜测。代码制造者为每次猜测提供反馈:
    – 1 个黑色钉子表示正确的颜色在正确的位置,1 个白色钉子表示正确的颜色在错误的位置。
    – 反馈是无序的(即,代码破译者不会被告知哪个钉子在正确的位置)。

我们工作组的目标是更熟悉在每个框架中实现 ZK 应用程序的挑战;我们决定在这些语言中实现 Mastermind 游戏,因为这个游戏并不复杂,但理解和实现起来也不会太耗时。通过在多种语言中实现相同的游戏,我们主要希望评估学习这些语言及相关 API 的复杂性,并使用它们来实现游戏。我们通过测量源代码行数(LoC)中的实现大小差异来经验性地衡量这种复杂性,并通过总结我们对这些语言的喜好或不喜好来非经验性地衡量。总体而言,这项工作的目的是帮助我们作为 ZK 安全分析师更好地理解使用这些语言的开发者可能面临的陷阱。

比较

上面的数字仅计算源代码行。省略了空行和注释行。我们使用 cloc 工具进行计数:https://github.com/AlDanial/cloc

在我们开始编码之前,我们首先阅读了一些文档,并浏览了每种目标语言的一些示例项目。在我们调查的五种语言中,有三种是受 Rust 启发的语言(Noir)或 Rust 库(Halo2、Arkworks)。虽然由于它们的 Rust 起源,语法相似,但其他语言的语法差异很大,因为 gnark 是用 Go 编写的嵌入式 DSL,而 Circom 是一种非常专业的 DSL,其语法类似于用于设计数字系统和电路的硬件描述语言 Verilog。

在进行这项调查后,我们开始了实现。我们在一次小组通话中共同编写了 Circom 的实现,然后我们的四人团队各自开始在剩下的四种语言中实现 Mastermind。在完成实现后,我们重新聚集以比较实现。

ZK DSL 的实现大小存在明显差异,Noir 和 Circom 的实现最小(分别为 77 行和 90 行),而嵌入式 DSL 的 gnark(101 LoC)、Halo2(156 LoC)和 Arkworks(227 LoC)由于其不够简洁的语法和更大的所需样板代码而实现较大。值得注意的是,gnark 具有最紧凑的接口(因为 gnark Circuits 只需定义一个函数),这使得它在嵌入式 DSL 中具有最小的实现大小。

接下来,让我们更详细地探讨每个框架。

1. Circom:基准

Circom 作为我们比较的基准。这种语言在 ZK 领域被广泛认可和使用。它也是这几种语言中“最成熟”的语言,Circom 的初始版本已经快 6 年了,发布于 2018 年。Veridise 在 Circom 方面也有丰富的专业知识,因为我们在 circom 项目中发现了严重的安全漏洞(例如,在 circom-pairing 库 中)。

Circom 是一种独特的领域特定语言(DSL),迫使开发者以算术电路的形式思考,其中电路根据一组输入信号生成一组输出信号。通过“连接”电路(即,将一个电路的输出信号连接到另一个电路的输入信号)来实现模块化,以创建更大和更复杂的电路。与本次调查中的其他语言不同,Circom 的语法并不是受主流软件语言的启发,而是受到硬件描述语言 Verilog 的启发。

用于验证 Mastermind 中代码的 Circom 代码示例。将此示例与:

来自 https://www.chipverify.com/tutorials/verilog 的 Verilog 中编写的计数器电路示例进行比较。我们可以看到类似的组件实例化(Verilog 中的 module,Circom 中的 template)、信号声明(input ... output ...)和信号操作(Verilog 中的 <=,Circom 中类似于 <==)与我们的 Circom 示例相比。

这使得 Circom 提供了一个直观的接口,用于连接算术电路(因为它受到用于描述数字电路的语言的启发),但也缺乏成熟语言的符合人体工程学的特性(例如,Rust 的函数式编程语言特性和工具生态系统)。

优点:

  • 结构化的 DSL,具有可重用组件
  • 在 ZK 社区中建立了广泛的文档和示例

缺点:

  • 由于缺乏高级语言特性,可能会显得冗长
  • 工具和测试基础设施相比其他语言更为原始,后者对单元测试等有更好的支持

你可以在 这里 找到我们在 Circom 中的 Mastermind 完整实现。

建议:记录意图

电路实现有时可能会变得难以理解,因为开发者努力在一种与通用编程语言不同的、不熟悉的语言中高效地实现他们的算法,这种语言具有特有的特性和限制。添加文档以解释代码的意图,以及代码如何实现该意图的解释,可以帮助安全分析师验证代码的正确性,并帮助未来的开发者(或当前开发者在未来重新访问代码时)理解代码并适当地使用或更新它。

2. Gnark: 可定制性与复杂性的结合

Gnark 提供了一种高度可定制的 ZK 电路设计方法。Gnark 中的电路作为任意 Go 代码中的 API 调用编写,赋予开发者显著的灵活性。这种定制甚至扩展到微调和自定义约束系统的能力。

然而,这种灵活性是有代价的。由于 gnark 是一个通用编程语言中的库,开发者(和安全分析师)需要对 gnark 的 API 以及在某种程度上的内部工作有很好的理解,以确保实现应用程序的正确性(这一观察对 Halo2 和 Arkworks 更为适用,因为它们的 API 更加复杂)。这可能使得阅读和编写 gnark 电路的过程比专用 ZK DSL 更加繁琐。

这是在 gnark 中实现电路所需的核心结构;此外,frontend.API 对象包含了实现算术电路所需的大多数方法。

然而,gnark 的一个缓解因素是,所提供的核心 API 比我们实验过的其他 ZK 库要小,因此 gnark 的实现是所有 ZK 语言中代码行数最少的。

优点:

  • 高度可定制
  • 高度灵活,因为电路作为任意 Go 代码中的 API 调用编写

缺点:

  • 需要更多的 API 和内部知识以确保正确性

你可以在 这里 找到我们在 gnark 中实现的 Mastermind 的完整代码。

建议:模块化和标准化

在嵌入式 DSL(与专用 ZK DSL 相比,具有更少的保护措施)中,应特别注意保持代码模块化,并标准化整个项目中代码库的组织方式。遵循一小组标准约定的代码更容易进行审查。

3. Noir: 高级抽象与权衡

Noir 是一种相对较新的 ZK 语言,于 2022 年推出。Noir 具有类似 Rust 的语法,旨在与后端无关,使其成为一种高级语言,抽象掉与 ZK 电路设计相关的许多复杂性。Noir 的生态系统发展良好,提供了许多示例(例如,awesome-noir GitHub 仓库 ),为开发者提供了坚实的基础。

请注意,与下面的 Arkworks 相比,在 Noir 中生成 Poseidon 哈希的相对简单性。

然而,Noir 的高级特性也限制了对电路的细粒度控制,这可能对需要精确优化的应用程序构成缺陷。

优点:

  • 语法类似 Rust,与其他 ZK 语言相比非常简洁
  • 语言是高级的,与后端无关
  • 生态系统发展良好,支持良好

缺点:

  • 由于语言是高级的,限制了对电路的细粒度控制
  • 作为一种相对较新的语言,可能缺乏其他 ZK 框架的一些成熟度

你可以在 这里 找到我们在 Noir 中实现的 Mastermind 的完整代码。

4. Halo2: 以冗长换取效率

Halo2 是一个 ZK 库,强调可定制性和效率。它允许开发者创建高度高效的证明系统,以满足特定应用的需求。然而,我们发现 Halo2 的冗长和样板代码可能令人望而却步,导致较长的编译时间和更陡峭的学习曲线。

来自 common.rs 的一个代码片段,展示了使用多个不同的“芯片”,每个芯片用于执行不同的操作集。正确找到、初始化和使用每个芯片是 Halo2 大量 API 的一个挑战。

尽管存在这些挑战,Halo2 生成优化证明系统的能力使其成为性能关键应用的一个有吸引力的选择。

优点:

  • 高度可定制,能够创建高效的证明系统
  • 针对需要性能优化的应用量身定制

缺点:

  • 冗长,需要大量样板代码
  • 编译时间长

你可以在 这里 找到我们在 Halo2 中实现的 Mastermind 的完整代码。

5. Arkworks: 基于 Rust 的模块化的力量(和复杂性)

Arkworks 是一套基于 Rust 的 ZK 库,提供了一种模块化的方法来构建 ZK 应用程序和自定义 ZK 组件。在我们比较中提到的 ZK 技术中,Arkworks 值得一提,因为它专注于模块化以及从较小、可重用组件组合 ZK 电路的能力。

Arkworks 的优势在于其模块化和可定制性,因为常见功能可以通过自定义组件进行增强,以创建高度专业化的 ZK 技术栈。然而,Arkworks 的复杂性可能会让新手感到不知所措,陡峭的学习曲线可能会阻止一些开发者。

Arkworks 复杂性的一个例子:虽然其他语言可能对哈希函数有相对简单的接口,但 Arkworks 需要自定义配置来计算 Poseidon 哈希。

优点:

  • 基于 Rust,专注于模块化和可组合性
  • 支持多种证明系统和加密原语,并且可以扩展到新的 ZK 组件

缺点:

  • 学习曲线陡峭且复杂
  • 需要熟悉 Rust 和模块化设计原则

你可以在 这里 找到我们在 Arkworks 中实现的 Mastermind 的完整代码。

建议:分离关注点

像 Circom 这样的 DSL 的一个优势是,应用逻辑几乎与其他关注点完全分离,例如“我使用的是什么证明系统?”在 ZK 库和嵌入式 DSL 中,尽可能做到这一点;我们经常发现,单独审查应用逻辑(以回答“所有值是否都被正确约束?”)要比审查证明系统的设置和如何被更大生态系统使用要容易得多。当这些关注点交织在一起时(例如,在 Arkworks 中很容易发生),阅读代码变得更加困难,因为读者必须同时考虑代码的许多不同属性。

结论:选择合适的 ZK 语言

一般来说,我们发现可定制性往往是可理解性的敌人,即使语言设计者努力避免这种权衡。以 Circom 为例——虽然证明系统或目标曲线的具体细节在源代码中是隐藏的,但它使得应用的实际约束和见证生成更容易理解。

Noir 的目标与 Circom 类似,因为其高级的、类似 Rust 的语法大大简化了开发——甚至比 Circom 更加简化,因为 Noir 的实现是我们调查中所有实现中最小的——同样将 ZK 细节和证明系统隐藏在开发者的视野之外。

与 Circom 和 Noir 相比,Arkworks 更像是一个“专家工具”——有太多自定义电路的方式,以至于很难入手,因为提供的“基本”电路设置指导非常有限。

Halo2Arkworks 类似,旨在为开发者提供强大的自定义和优化电路的能力,以创建高性能的 ZK 应用程序。但是,与 Arkworks 一样,Halo2 也相对冗长,并且编译电路的时间往往较长。

在嵌入式 DSL 中,gnark 可能是最容易入手的。它提供了许多自定义的机会,但“默认”配置提供了一个简洁、易于使用的界面,使得编写第一个电路相对简单。然而,就我个人而言……Go 不是我最喜欢的语言(接口是隐式实现的吗? 谁觉得这是个好主意?),我发现它是一种“易于编写,难以阅读”的语言,个别设计决策很快就会使实现变得模糊。

总体而言,我们发现没有一种正确的 ZK 语言或框架——就像没有一种正确的通用编程语言一样(我知道这是一个不太令人兴奋的结论)。因此,在开始一个新项目时,我们建议你尝试做我们所做的——尝试几种不同的语言!看看哪种最适合你、你的团队和你的项目。

GitHub 仓库

你可以在这个 GitHub 仓库 中找到我们的 Mastermind 游戏代码,使用 Noir、Circom、gnark、Halo2 和 Arkworks 实现。

作者: Ian Neal,Veridise 的研发工程师

工作组成员: Alp Bassa, Ian Neal, Tim Hoffman, Tyler Diamond

想了解更多关于 Veridise 的信息?

Twitter | Lens | LinkedIn | Github | 请求审计

我是 AI 翻译官,为大家转译优秀英文文章,如有翻译不通的地方,在这里修改,还请包涵~

点赞 0
收藏 1
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
Veridise
Veridise
使用形式化方法加强区块链安全性