How SNARKs fall short for FHE

This is part i of a two part series! In this article, we’ll be motivating the need for new ZK tools when working with fully homomorphic encryption (FHE).

At Sunscreen, we’re working to bring FHE to the masses, starting with web3. As part of our mission, we’ve been thinking about the infrastructure needed to support FHE in decentralized, trustless environments.

In web2, when we ask for a computation to be performed, we often rely on the reputation of the company charged with the task. When we ask AWS to run a benchmark, we implicitly trust that Amazon has run the computation we asked them to on the machine we requested. When we use ChatGPT, we implicitly trust that OpenAI has used their advanced learning model behind the scenes. But, how do we know that Amazon or OpenAI has actually done what we asked? The answer is we don’t. We’re trusting these organizations based on their reputation.

In web3, things change. We’re now in a trustless environment where we might not trust the user or the computing party.

How ZKPs and FHE fit together

As a refresher, fully homomorphic encryption (FHE) is the next generation of public key cryptography, allowing anyone to perform computations directly on encrypted data. Zero knowledge proofs (ZKPs), on the other hand, allow one to prove a statement is true without revealing any information (beyond the correctness of that statement). So how do these two fit together?

ZKPs are useful and often necessary when building FHE-enabled applications in a trustless environment. By trustless, we’re referring to one of two scenarios–in which we cannot fully trust (1) the user providing FHE-encrypted data or (2) the third party responsible for performing the computation on the encrypted data.

Let’s consider how these scenarios might arise in practice.

For the former, imagine a user wants to withdraw some encrypted amount enc(amt) from her encrypted account balance enc(bal). The user may (innocently or maliciously) try to send more money than she actually owns (such that amt > bal ). How can the implementation enforce that amt <= bal while keeping these two values private to other parties? Using a ZKP, the user can prove that amt <= bal without revealing to anyone what these values actually are. User-provided ciphertexts must also be “well-formed”—meaning that they obey the requirements of the underlying encryption scheme and aren’t just random strings of data. If we don’t trust the user, how can we ensure this is indeed the case? With ZKPs! The user can provide a ZKP along with her ciphertext, proving the ciphertext’s validity without revealing any of the underlying values.

For the latter, let’s take a step back and think about how things work in web3, where the maxim is “don’t trust, verify.” When validating transactions on a blockchain, we assume there’s an honest majority of miners/validators. When using rollups, we often rely on rollup providers to prove they’ve faithfully executed the given transactions. FHE computations are no different than any other computation. How do we know a third party ran the FHE computation we asked? If a large number of parties perform the computation, we might assume there’s an honest majority to ensure correctness. However, if only one party runs the FHE computation, things get a bit sticky. Similar to the validity proofs needed for rollups, the computing party must prove they’ve faithfully executed the FHE computation. We refer to this setup as “verifiable FHE” (in which we can verify the FHE computation was performed correctly, often via ZKPs).

Verifiable FHE is very difficult in practice. Some research has been done on this topic but it turns out that proving even simple FHE computations were performed correctly (say verifying a single homomorphic addition and homomorphic multiplication operation) can take on the the order of minutes even with highly efficient proof systems like Groth16.

Shortcomings of existing SNARKs

Regardless, we still need to tackle the first issue—verifying that conditions on user (FHE encrypted) inputs have been met. The question we often get asked at Sunscreen is “can’t we just use one of the popular SNARKs to accomplish this task?”^[1] After all, so much work has been done in the past decade on SNARKs (Groth16, STARKs, PLONK to name a few) with plenty of existing infrastructure provided by a variety of projects.

Unfortunately, the answer is no.

FHE relies on lattice-based cryptography, whereas the most efficient ZKPs utilized in the web3 space don’t. To prove an FHE ciphertext is well-formed, we need to show that it satisfies a certain matrix-vector equation, with entries from particular mathematical “spaces” (called rings), and that these entries are “small”. Proving the entries are “small” is the most expensive part in zero knowledge land.^[2] If we want to show this in an efficient way (with compact proofs that are fairly fast to create), we need a proof system meant for handling lattice-based relations.^[3] The first idea that might come to mind is to use a lattice-based proof system. After all, what better way to prove statements about lattice-based relations than with a lattice-based proof system? If we take that route, we’ll have proofs that are easily hundreds of kilobytes in size (it’s also unclear how competitive proof verification times would be).^[4]

Our team has been working on implementing a specialized proof system for this task ("Short discrete log proofs for FHE and Ring-LWE ciphertexts" aka SDLP); you can track our progress here. SDLP is a fairly recent proof system (from 2019) that leverages a trustless setup to show user inputs from a lattice-based cryptosystem are well-formed using elliptic curve-based cryptography. One of the key insights the authors make is recognizing that there is indeed a connection between the polynomial operations in the lattice scheme and the inner product proofs of Bulletproofs, which is why they transform the lattice relation into a Pedersen commitment. This allows the authors to obtain fairly small proofs (single digit kilobyte range for showing an FHE ciphertext is well-formed) with decent proving and verification times.^[5]

While SDLP will allow users to prove that their inputs are well-formed, this proof system won’t be good for much else as SDLP breaks everything down into a matrix-vector equation. Ignoring the fact that this severely restricts what we can prove, there’s also much more efficient proof systems for general arithmetic circuits.

So what will existing SNARKs be good for?

Once the user shows their ciphertext is in the correct format, they can utilize popular SNARKs to prove more general relations about their inputs (allowing us to make use of existing libraries and infrastructure for SNARKs).

To do this, we’ll need to “link” the two proof systems together. Otherwise, imagine a malicious user creates a proof that their ciphertext c corresponding to plaintext value p is in the correct format and then instead proves that the plaintext p’ is less than the amount a. How can we detect this and ensure the user’s inputs are the same to both proof systems (SDLP and the SNARK)?

What Sunscreen is working on

In terms of using FHE in a trustless setting, the user will usually have to (a) encrypt her inputs, (b) prove these input ciphertexts are “well-formed,” and finally (c) prove that her plaintext inputs satisfy any application-dependent conditions.

To tackle (a), we have our FHE compiler which we’ve released an initial version of.

To tackle (b), we’ve developed a GPU-accelerated library for the SDLP proof system.

Tackling (c) is where things get tricky. As mentioned earlier, there are better proof systems than SDLP for general arithmetic circuits so we’ll want to use SNARKs for (c). However, we need to ensure the prover has “committed” to the same inputs across the two proof systems.

To make matters worse, ZKPs are quite difficult for non-experts to work with. As part of creating a ZKP, the developer needs to translate their program (written in some high level programming language like Rust or Python) into a system of circuits and constraints in a particular format, depending on the chosen arithmetization scheme. Doing this conversion by hand is both tedious and highly error-prone. That’s where ZKP compilers come in–they help the developer with this translation, setting up circuits and constraints in the correct format behind the scenes.

Plugging SDLP into existing ZKP compilers did not provide either the performance or developer experience we wanted.

Thus, to fully address (c), we’re working on a ZKP compiler that supports SNARKs and will plug into our SDLP library (i.e. allow the prover to show they’ve committed to the same inputs across the two proof systems). In linking together our FHE and ZKP compilers, SDLP will serve as the glue that holds them together.

Continue on to part ii if you’d like to learn about Sunscreen’s ZKP compiler!

What's next for us

In the next two months, you’ll be able to sign up for access to our private testnet. So far, our priority has been on developers, but we don’t want to leave anyone out! We’ll also be providing a demo suite of apps to try out.

We’ll be sponsoring ETHGlobal New York, with $5000 worth in prizes available from Sunscreen. Hackers will get first access to our private testnet and our demo suite of FHE apps. Ravital, Rick, and Ryan will be at Sunscreen’s own cocktail table so come say hi!

Finally, we’ve been working on our own custom implementation of TFHE to provide ultra fast comparisons and enable new applications. If you’re a developer interested in using FHE in your project, feel free to reach out to us for first access.