Verifieable FHE（VFHE）：使用Plonky2来证明Zama TFHE的“Bootstrapping的正确执行”

1. 引言

Zama团队2024年论文Towards Verifiable FHE in Practice: Proving Correct Execution of TFHE’s Bootstrapping using plonky2 中：

首次阐述了，在实践中，将整个FHE bootstrapping操作，使用SNARK来证明。
在其相应的https://github.com/zama-ai/verifiable-fhe-paper（Rust，Plonky2）开源代码实现中，为该bootstrapping操作设计了算术电路，并使用Plonky2进行了证明：
- 在保证功能完整和安全的情况下，对TFHE的programmable bootstrapping中的操作进行了少量调整，使其能在算术电路中更高效地表示。
- 在AWS C6i.metal实例上，证明该电路用时20分钟。
- proof size约为200kB。
- 验证该proof用时少于10ms。
- 为实现memory-efficient，利用了（bootstrapping操作）该计算的结构化优势，以及，Plonky2的递归IVC能力，实现了递归证明。

Fully Homomorphic Encryption (FHE) 全同态加密技术：

支持对密文输入做任意计算，生成密文输出。
对密文输出解密的结果，等于，直接对明文输入做相应计算的结果。

Succinct Non-interactive ARguments of Knowledge (SNARKs) 密码学技术：

支持Prover，让Verifier信服，某任意计算执行正确。【数据必须是明文的】

FHE和SNARKs各有所短：

FHE自身无法保证该计算的正确性，因此也无法提供任何计算完整性保证，使得在真实世界的FHE部署时，存在可疑的隐私攻击问题。
SNARKs可保证计算完整性，但需要知悉数据的明文信息，来证明基于这些数据的计算是正确的，对于某些特定隐私保护应用场景，是命令禁止提供数据明文信息的。

FHE和SNARKs相结合：

可获得verifiable FHE（VFHE）：支持Prover，让Verifier信服，基于密文数据的任意计算执行正确。

VFHE的迷人之处在于，可将该技术用于如下场景：

改进区块链协议，以支持私有交易。
解决计算外包中的安全问题，可用于替换安全硬件模块，将对硬件厂商的信任，转移至，对密码学假设的信任。

尽管这在理论上听起来不错，但实践中的核心问题在于：

相比于明文运算，FHE会引入大量的开销。
相比于待证明的计算本身，SNARKs Prover计算量要贵得多。

因此，核心在于：

如何让VFHE具备实用性

经典FHE方案包括：

1）密文操作：对明文的同态运算。通常可高效计算，且可使用SNARK证明。
2）bootstrapping操作：最昂贵的操作。

若不熟悉FHE，可能对bootstrapping操作不了解，详情可参看：

Zama团队2022年5月4日博客 TFHE Deep Dive - Part I - Ciphertext types

可简单将bootstrapping操作看成是：

一种密文管理操作。
支持某program基于密文数据做无限计算。

bootstrapping操作通常为FHE方案中最昂贵的操作，因此，实现真正实用VFHE系统的最大障碍在于：

bootstrapping操作。

因此，VFHE系统实用性的关键，在于：

对于FHE真实参数（而不是toy参数），使用SNARK，高效证明bootstrapping，的能力。

基于此动机，Zama团队2024年研究并发布了论文Towards Verifiable FHE in Practice: Proving Correct Execution of TFHE’s Bootstrapping using plonky2 。

Zama团队专注于TFHE：

TFHE提供了非常轻量级的programmable bootstrapping (PBS)。

尽管TFHE的bootstrapping，比其它FHE方案中的bootstrapping，计算开销更低，但其也足够复杂，使得若直观对其做SNARK-ifying操作，将导致Prover需要巨大的内存，对大多数应用来说是不切实际的。

Zama团队曾实践过，使用FHE toy参数（不是真实参数），在具有128GB RAM的AWS实例上运行，直接内存溢出。

这就意味着，直接对TFHE的bootstrapping做SNARK-ifying操作，不是高效的方案。为此，Zama团队专注于利用bootstrapping操作中的结构化特性：

TFHE的PBS中，包含一个具有多次（约600到700次）迭代的循环
SNARKs技术可使用Incrementally Verifiable Computation（IVC）来高效证明该循环，而不是将该循环展开为一个大的电路。所谓IVC，是指一次证明一个迭代，而不是一次证明所有迭代。

Zama团队开源代码https://github.com/zama-ai/verifiable-fhe-paper（Rust，Plonky2）中，使用Plonky2实现了基于递归的IVC方案，并将该IVC方案用于了TFHE PBS。其中Plonky2支持非常高效的递归，适用于本场景。

1）每次迭代中，会生成单个proof，该单个proof对应为：
- 1.1）该次迭代的实际计算
- 1.2）之前迭代的proof的verification
2）在循环的最后一次迭代，所生成的final proof，可让Verifier信服，之前的中间态proof均是正确生成和验证通过的。

因此，可将传统PBS计算的循环操作，转换为统一算术电路格式——可使用IVC来证明该统一格式的算术电路。

Zama团队对其TFHE进行了少量调整，使其更适合于基于有限域的算术电路模型。如：

将密文的modulus，修改为Plonky2原生使用的素数
修改了key switch，使得可通过external product来执行

需要调整参数，但确保这些参数仍是正确的且是安全的（目标是128-bit安全性）。PBS的循环迭代电路，如下图所示：【其中忽略了检查之前迭代proof的verifier电路】
在这里插入图片描述
该电路会从前一迭代中接收loop counter $n$ ，以及前一迭代的结果，作为输入。该loop counter $n$ 值，决定了对前一迭代结果应用什么函数。该函数：

要么为：简单的negacyclic polynomial rotation (“Rotate Poly”)
要么为：在该input及其negacyclic rotation 之间有一个密文multiplexer（“Rotate Poly” + “External Product”）
要么为：某key switching操作（通过“External Product”）。

该PBS中包含了以上3种操作。其中：

对negacyclic polynomial rotation (“Rotate Poly”) 的子电路，以及，对external product的子电路，支配了整个电路size，从而支配了Prover开销。

详细的实现，可参看论文Towards Verifiable FHE in Practice: Proving Correct Execution of TFHE’s Bootstrapping using plonky2。

借助基于IVC的实现，所需内存量降了一个量级，使得消费级笔记本也可运行该Prover。在经典AWS示例中，计算proof需约20分钟，仍相对较长，但已接近实用水平了。

System	Prover Time (min)	Verifier Time (ms)
M2 MacBook Pro - 8 cores, 24GB	48	5
Hpc7a.96xlarge - 192 cores, 768GB	18	8

同时，Zama团队将其Plonky2 IVC实现，与通用zkVMs（RISC0和SP1）对比发现，Zama团队的IVC方案性能要高2个数量级。

因此，Zama团队认为：

VFHE处于实用化的边缘。
证明FHE方案中最困难部分（bootstrapping），可使用具有非常合理计算资源的SNARK来证明。
这是一个重要的里程碑，也是一个开始。
仍有许多途径待探索，如：
- 如何将Prover，由PBS电路，扩展到，完整的FHE电路？
- 是否有改进基于通用zkVM的实现的技术？是否有更适合FHE的zkVM？
- 使用基于folding的IVC（如见2024年论文Mangrove: A Scalable Framework for Folding-based SNARKs），而不是基于递归的IVC，能否获得更好的效果？
坚信VFHE方案将对隐私技术产生巨大影响，并将解锁众多惠及所有人的应用程序。

参考资料

[1] Zama团队2024年5月5日博客 Verifiable FHE Bootstrapping using SNARKs
[2] Zama团队2024年论文Towards Verifiable FHE in Practice: Proving Correct Execution of TFHE’s Bootstrapping using plonky2