This blog post is a condensed version of our new work: “Towards Verifiable FHE in Practice: Proving Correct Execution of TFHE’s Bootstrapping using plonky2”. The full version is available on ePrint and the associated code is available on github. 

Fully Homomorphic Encryption (FHE) is a technology that allows arbitrary computations to be performed on encrypted inputs, producing encrypted outputs. Those results, when decrypted, are consistent with the results of the computation had it been performed on plaintext inputs.

Succinct Non-interactive ARguments of Knowledge (SNARKs) is another cryptographic technology that allows a prover to convince a verifier that some arbitrary computation has been performed correctly. 

FHE by itself does not provide guarantees about the correctness of the computation and so does not provide any guarantees on integrity, making it even susceptible to attacks on privacy in some real-world deployments. On the other hand, SNARKs guarantee the integrity of computation but require plaintext knowledge of the data for which the computation is proven correct, which can be prohibitive in certain privacy-preserving applications.

By combining FHE and SNARKs, we obtain verifiable FHE (VFHE) where a prover can convince a verifier that some arbitrary computation over encrypted data has been performed correctly. This is quite appealing as there are numerous applications of this technique. For example, it may improve blockchain protocols that support private transactions. It can also address security issues when outsourcing computation, where it may be used to replace secure hardware modules, thereby shifting trust from hardware vendors to cryptographic assumptions. 

While this all sounds nice in theory, the core issue of this approach is the practicality: not only does FHE incur a significant overhead compared to the plaintext operations, SNARKs themselves typically are much more expensive to compute than the computation being proven. The aim of this project is to explore how practical VFHE can actually be.

A typical FHE scheme consists of ciphertext operations implementing the homomorphic arithmetic on the plaintext and a bootstrapping operation. If you are unfamiliar with FHE, then it might be unclear at first sight what the bootstrapping operation is for. We don’t go into detail here (see our previous blog post for more details), but simply remark that it is a ciphertext management operation that allows a program to compute over encrypted data indefinitely. While the arithmetic operations are typically quite efficient to compute (and also to prove using a SNARK), the by far costliest operation is usually the bootstrapping. As such it presents the biggest obstacle towards a true VFHE system, since the practicality of such a scheme will depend mostly on the ability to efficiently prove a bootstrapping using a SNARK. So we set out to do exactly this and see if we could do it for realistic parameters as one may use in the wild.

Naturally, we focused on TFHE, which offers a very lightweight programmable bootstrapping (PBS). Even though TFHE’s PBS is less costly than bootstrapping in other FHE schemes, it is complex enough that naively SNARK-ifying it leads to a prover that would likely be considered wildly impractical in most applications, mostly due to the enormous memory requirements. We don’t base this statement on pure estimations, we actually tried this. An AWS instance with 128GB of RAM ran out of memory when even just playing with moderate toy parameters. 

When it became clear that this straight-forward approach would not yield an efficient scheme, we focused on exploiting the structure of the bootstrapping operation. The upshot is that the PBS essentially consists of a loop with many iterations (think of 600-700), and indeed the literature on SNARKs has produced several techniques to prove such a loop more efficiently than naively rolling it out into a large circuit. Such techniques are summarized under the term Incrementally Verifiable Computation, which allows to prove the loop iterations one at a time instead of all at once. We implemented a recursion based IVC scheme using plonky2 (which supports very efficient recursion and is thus suitable for this purpose) and applied it to the PBS. This works as follows. On each iteration, a single proof is generated for 1) the actual computation in this iteration and 2) the verification of the proof from the previous iteration. At the end of the loop, the final proof convinces the verifier that intermediate proofs have been properly generated and verified.

So we transformed the loop operation of the traditional PBS computation into uniform arithmetic circuit form so that it could be proven using IVC. We tweaked TFHE in a few places to make it more suitable for the arithmetic circuit model over a finite field. For example, we changed the ciphertext modulus to be the prime natively used by plonky2 and modified the key switch so that it can be performed by the external product. This required adjusting the parameters, but we ensured that the parameters are still correct and secure (targeting 128 bits). The circuit of a loop iteration of the PBS then looks like so (without the verifier circuit that checks the proof of the previous loop):

The circuit receives as inputs the loop counter and the result from the previous iteration. The loop counter value determines what function is applied to the result of the previous iteration. This function is either a simple negacyclic polynomial rotation (“Rotate Poly”), a ciphertext multiplexer between the input and its negacyclic rotation (“Rotate Poly” + “External Product”) or a key switching operation (via “External Product”). The PBS is composed of these three operations. The subcircuits for negacyclic polynomial rotation (“Rotate Poly”) and the external product dominate the size of the circuit and thus the cost of the prover. We refer to the paper for details on how exactly they are implemented.

As expected, using this IVC based implementation, the memory requirement was reduced to a degree that even commodity laptops can now run this prover. The running time is still fairly high – on a typical AWS instance it requires about 20 minutes to compute the proof – but close to something that could be used in practice, as shown in the following table.

We also compared our approach to simple implementations on general purpose zkVMs (Risc0 and SP1), which perform at least two orders of magnitude slower than our scheme.

We conclude from our work that VFHE is on the verge of practicality. We demonstrated that the hardest part of an FHE scheme can be proven using a SNARK with very reasonable computational resources. While we believe that this is an important milestone, this is, of course, just the beginning. There are many avenues to explore. Here is a (non-exhaustive) list of questions that we would love to know the answers to: 

• How do we extend our prover from a PBS to a full FHE circuit? 
• Are there techniques to improve the zkVM-based implementations? Are there zkVMs more suitable for our purposes? 
• Can we obtain better results using folding-based IVC instead of recursion?
• Are there any other ways to improve the efficiency of our prover?

We are excited to see what answers we and the community as a whole will find. We believe that a practical VFHE scheme will have a high impact on privacy technologies and will unlock a multitude of applications benefiting everyone. 

Additional links

• Check out Louis Tremblay Thibault's interview on the FHE Onchain podcast about: Building Verifiable FHE using ZK.
• Read the paper on ePrint: Towards Verifiable FHE in Practice: Proving Correct Execution of TFHE's Bootstrapping using plonky2.
• Watch Michael Walter's presentation at the Zero Knowledge Summit 12 : Towards Verifiable FHE in Practice.
• Follow Zama on Twitter to get the latest news.