本文介绍了零知识证明（ZK）领域的最新进展，重点分析了Ulvetanna发布的Binius方案。Binius通过使用二进制域、针对小域的承诺方案以及基于HyperPlonk的SNARK，能更有效地处理位运算，降低内存占用，提高硬件友好性，从而加速可验证计算，并可能在软件工程和金融领域引发变革。
介绍
零知识和有效性证明，通常缩写为 ZK，代表了密码学、数学和计算机科学领域中一个引人入胜的领域。它们允许一方（即证明者）以时间和空间上高效的方式说服其他方（即验证者）某个特定陈述（例如计算机程序的执行）是真实的。这意味着验证证明的速度比验证者直接执行计算的速度要快得多，并且需要更少的信息，并且该证明可能不会泄露敏感数据。
正如我们在之前的博客文章中讨论的那样，实际零知识证明对工程的影响是多方面的且影响深远。其中一个领域是加密货币（参见我们的加密货币原则）。尽管如此，它还扩展到内容创建平台、身份和身份验证、国家安全、分布式计算等。
ZK 的当前发展
为了证明任意计算机程序的执行，我们需要将它们转换为适合 ZK 的形式；这个过程称为算术化，包括将程序表示为在一系列整数/有限域上定义的一堆方程。在计算机程序中，我们如何表达和思考存在差异，我们使用字节和二进制运算。例如，如果我们的程序有一个布尔变量，我们必须确保该变量仅取值 0 或 1。由于我们处理的是整数，因此该条件会添加一个 b(1−b)=0b(1−b)=0 形式的方程。问题是这个变量用一个大整数表示（至少 64 位长），这增加了内存使用和计算时间的显著开销，因为我们现在处理的是有限域上的运算（而不是位）。诸如按位运算或显示整数的二进制分解之类的操作成本很高。
由于 ZK 的性能涉及与普通编程不同的权衡，因此开发人员需要更深入地了解密码学并学习以不同的方式进行编码。开发人员的工具仍在创建中，在某些情况下，取决于直接编写算术电路，这既耗时又容易出错。此外，证明增加了大量的开销，包括内存和时间的使用。因此，ZK 给开发人员和用户体验都带来了困难。这意味着需要花费更多的时间和金钱来培训开发人员，并且熟练程序员的可用性会降低。
在过去的几年里，zk 领域发展非常迅速，我们已经看到各个方向都在努力提高证明系统的性能：
- STARK 使用小字段大小，例如 mini-Goldilocks 和 31 位梅森素数。
- Folding 方案，例如 Nova、Protostar 和 Protogalaxy。
- 查找参数，Jolt 旨在将所有内容简化为仅查找预先计算的有效输入/输出对表上的任何操作。
每个系统在证明大小、证明者时间、验证者时间和可以轻松支持的计算类型方面都有优点和缺点。在硬件方面已经有人努力加速这些证明系统，但它们都为用字段元素表示位付出了代价。
Binius 和二进制字段的使用
在 STARK 中使用较小的字段减少了表示变量的开销，并减少了证明时间。问题自然而然地出现了：我们能做得更好吗？ 接近年底，Ulvetanna 发布了一篇论文，表明我们可以使用更小的字段，并开源了一个实现 Binius。可以在这里找到对 Binius 的初步分析。我们将很快发布这篇文章的第二部分，深入探讨其结构和用途。
Binius 的贡献可以概括为以下三个要点：
- 使用二进制字段——这本质上是使用各种大小的位串。可以调整大小以表示变量，而不会产生开销。
- 适用于小字段的承诺方案。它基于哈希函数，该函数比基于椭圆曲线的哈希函数更快，并且不需要可信的设置。它大量借鉴了 Brakedown。
- 基于 1 和 2 之上的 SNARK，基于 HyperPlonk 的思想，但可以扩展到其他算术化方案。
整个结构的主要优点是它可以更自然地处理位操作（例如，两个位串之间的异或只是字段上的加法），并消除了与数据类型表示相关的开销。例如，布尔变量可以仅由大小为 1 位的 1 个字段元素表示！这减少了整个证明系统的内存占用（尽管我们需要使用更大的字段来实现密码安全）。
另一个优点是操作非常快速并且对硬件友好。在添加字段元素的情况下，它只是 XOR 运算，避免了进位和溢出。还有非常有效的算法可以处理二进制字段，例如加性快速傅里叶变换 (FFT)，用于生成 Reed-Solomon 编码。
主要的缺点与证明大小有关（它比大多数 SNARK 和 STARK 大得多，约为几 MB）和验证者时间。但是，验证者的时间与大多数证明系统相当，并且证明者明显更快。此外，SNARK 中较小的证明大小是以可信设置为代价的，这使得整个系统依赖于参数初始化仪式的完整性，通常使用几 GB 的内存。
应用
最初的论文展示了如何对 Keccak 和 Grøstl 哈希函数进行算术化，这些哈希函数涉及许多按位运算，这使得使用其他证明系统很难处理它们。性能分析提供了对新结构的能力以及采用它可以获得什么的想法。更自然地处理按位运算的能力还允许我们使用这些哈希函数进行承诺并轻松证明它们。
我们可以构建一个虚拟机并使用 Binius 证明其执行的正确性。这可以使证明通用计算机程序非常有效，至少在生成证明所需的时间方面是这样。 我们可以通过使用 SNARK/STARK 包装证明来解决证明大小的问题，SNARK/STARK 只需要验证 Binius 的证明，从而产生更轻量级和高效的结构。
减少证明者的内存和时间使用可以实现可证明的全同态加密 (FHE)，这允许用户将昂贵的计算委托给不受信任的服务器，而不会泄露数据。FHE 允许用户在加密数据上进行计算，而无需先对其进行解密。
结论
我们认为，在扩展可证明的计算方面，Binius 可能会改变游戏规则，这可能会在软件工程和金融的不同领域引发重大变化。操作的内存使用和硬件友好性的降低以及虚拟机的开发可以使消费级硬件中的可证明计算成为现实，同时增强开发人员的体验，并减少所需的资源和培训。我们离大规模采用 zk 技术又近了一步。Lambdaclass 对这种新的证明系统及其功能很感兴趣，我们希望在 2024 年开始实施和开发它。
