ZK9: Building an FHE compiler for the real world - Ravital Solomon and Rick Weber (Sunscreen)

Transcript

foreign [Music] so the motivation of this talk is for you as the audience to be able to answer at the end of it out of these three things which of them are truths and which is a lie so to start us off let's tell you a little bit about what fully homomorphic encryption is so you can think of it as an extension to public key cryptography the idea here is you have the usual algorithms key generation encryption decryption but now you have these additional functionalities like being able to add and multiply ciphertext together there are usually some additional operations when you actually go into an fhe scheme and these tend to allow you

to do additional operations on encrypted data stuff like relinearization modulus switching and bootstrapping so in terms of fhe and how it's evolved as a technology the very first scheme was 2009 Craig Gentry incredibly slow I've heard all kinds of estimates on time but roughly speaking it took somewhere between 10 minutes and 30 minutes to multiply two encrypted numbers together using Gentry's original fhe scheme second generation of fhe started 2011 2012 much more efficient so now we're down to milliseconds to multiply encrypted numbers together third generation of fhe which is the generation we're on currently that is fairly fast as well a little bit

different than the second generation so rather than prioritizing best arithmetic it prioritizes fast comparisons and also allows for fast bootstrapping the idea here is you can do truly arbitrary computation on encrypted data whereas the second generation of fhe you generally set up the scheme to do a certain amount of computation and then you stop in terms of the work being done on fhe most of the initial work was focused on performance in the last five seven years it's transitioned more to usability if you want a rough idea of the overhead from using fhe we're roughly looking at about 10 to the 5 10 to the 6 versus doing the computation in the clear and that's with regards to

both space and time so what does fhe have to do with web3 I wouldn't say that's the focus of this talk but to give you some motivation people are interested in private smart contracts so smart contracts that operate directly on encrypted data some folks are interested in private auctions and dark pools like we heard in the previous talk and some folks are also interested in constructing some notion of private shared state but that requires a little bit more than just single key fully homomorphic encryption in terms of how exactly you use fhe to do these applications you can imagine that the user needs to encrypt their inputs via some sort of fhe scheme and then they will need to prove that their inputs satisfy some application

dependent conditions via zero knowledge proofs so how does fhe and zero knowledge proofs fit together here we're looking at an example of a private transaction so imagine Alice Alice is the sender Bob is the recipient she wants to send some encrypted amount of currency using the account model so if we're assuming there's an honest majority of validators the validators will check the proofs produced by Alice and then they will perform the computation directly on the encrypted data so they'll update Alice's encrypted account balance and Bob's encrypted account balance there is a different way of thinking about fhe in web3 that's if you're looking to do something more roll-up style the

difference here is that the validator will check Alice's proofs they will perform the computation directly on the encrypted data but since there's only one of them potentially they will need to prove that they've done these updates correctly I would say the roll-up style use of fhe is not the focus of our talk it is incredibly expensive probably not feasible for the next one to two years so let's say you're an engineer and you want to use fhe in your web3 application what is the experience like so the very first step is to figure out which fhe scheme makes the most sense for you you have a couple different choices here there is the BFE scheme that uses arithmetic circuits it supports exact

arithmetic there is the ckks scheme which also uses arithmetic circuits but only supports approximate arithmetic and finally there's the tfhe scheme which works with binary circuits and therefore could support more general purpose computation and it supports comparisons on encrypted data in terms of these three different schemes we can look at some of the trade-offs here since most applications of fhe and web3 are related to financial data and financial transactions approximate arithmetic is generally not suitable so we can immediately cross that scheme off in terms of the two remaining schemes BFE and tfhe the major trade-offs there is that BFE supports

super fast arithmetic it supports very high Precision so you can easily do 64-bit computation it has relatively small keys in ciphertext in comparison to tfhe the downsides with BFE is that it's very difficult if not impossible to compare encrypted data and you generally have slow bootstrapping so here you might not be able to do truly arbitrary computation on encrypted data tfhe on the other hand offers super fast comparisons very fast bootstrapping you generally bootstrap with every single operation the downsides is that arithmetic particularly multiplications on encrypted data is incredibly slow the ciphertext and keys tend to be quite

large particularly in comparison to BFE and finally there are some serious Precision issues with using this scheme so it's often hard to do 32 64-bit computation when you look at tfhe so we figured out two fhe schemes that might be suitable for us we'd be looking at either the bfv scheme or the tfhe scheme if we're interested in applying it to web3 so what actually happens in setting up an fhe scheme so we're going to focus on BFE but you can imagine there are similar considerations in setting up the tfhe scheme so BFE works with polynomials and particularly plain text are polynomials of less than degree n with coefficients mod P ciphertext are polynomials of less

than degree n with coefficients mod q p needs to be much smaller than Q for security reasons the first step you as an engineer will need to think about is how are you going to translate from numbers into polynomials there are actually a number of different encoding techniques with very different trade-offs so we have the scalar encoder so essentially a trivial encoding taking a number to some constant polynomial you have slightly fancier encodings like the integer encoding that's similar to doing like a binary decomposition or a binary expansion and you have fancier techniques like using the Chinese remainder theorem to essentially vectorize the computation after you figure out which data encoding technique you'd like to use you now need

to pick the scheme parameters so particularly you're going to have to figure out how to pick the degree n the plain text modulus p and the ciphertext modulus Q the sorts of considerations you'll need to ask yourself in choosing these parameters are what kinds of computations are you looking to do what sorts of ciphertext and key sizes are you okay with and finally what sort of performance are you looking to get another question you have to ask yourself is there's a special ciphertext maintenance operation called re-linearization do you want to use it if not that might save you a little bit of time so for the first truth and lie is fhe fast or slow I would say that fhe is actually pretty fast but the speed of

the various operations are highly scheme dependent and the speed of various operations is also highly parameter dependent another issue with fhe is that you really need to know how to effectively translate your program into a circuit so let's look at how different schemes perform we're going to focus on doing 32-bit computation these are the two major schemes we've identified as being most suitable for web3 you can see there is a very significant difference in terms of key generation time multiplication time and comparisons so for BFB if you're wondering why there's question marks for comparisons that's just because it is unclear whether or not you can actually do comparisons it

depends a little bit more on the exact computation as we mentioned earlier the performance of fhe also depends quite a bit on the parameters you choose so if we look at the BFE scheme one of the biggest factors in performance is the degree of the polynomial so you can see here there's a pretty significant difference in terms of key generation time if you go up two parameter sets very significant difference also for decryption time and multiplication time if you go up to parameter sets there is a similar issue for the tfhe scheme not necessarily as Extreme as for the BFE scheme here we're focused mostly on what sort of precision do you need

that really tends to affect the performance the most so you can see that multiplication is quite slow in both schemes but there's about 2x increase in time if you want to go from 32 to 48-bit computation so to sum up what's challenging for fhe well you need to figure out the right data encoding technique you need to figure out what the right scheme parameters are you need to determine if you want to insert in the special ciphertext maintenance operation if you're working with BFE if you're working with tfhe you have to manually manage Precision issues and finally regardless of which scheme you choose you need to know how to translate from programs to circuits effectively a question you might ask is can you

create a compiler that handles these things for us the answer is yes but for the somewhat hot take of this talk I would say that many fhe compilers do a serious disservice to fhe when it comes to Performance let's look at what happens if we want to do a chi-square test on encrypted data this application was chosen based on a recent sok on fhe compilers from Oakland s p 2021 we're going to look at how long it takes to generate Keys encrypt data perform the computation and decrypt so if you're an expert who knows what they're doing you can work with some super low level Library like Microsoft seal you can write this yourself and you

can manually optimize it this will take you about .053 seconds to do everything from Key generation down to decryption together so how did the fhe compiler stack up you can see that most fhe compilers do a pretty bad job they increase they add a huge overhead to the overall computation the only two compilers that I would say have a reasonable overhead are Microsoft's Ava and sunscreens compiler so for compilers to really be useful in this space we really need for them to marry performance with usability so we've narrowed down our fhe scheme options we have figured out how exactly

to set up our fhe scheme now we need to figure out how to prove stuff on our fhe encrypted data so there will be two things we need to prove about our fhe encrypted data you will need to prove that your encrypted inputs are valid I.E the ciphertext are well formed you will also need to prove that your encrypted data satisfies whatever application or contract specific conditions you're looking at so to go back to our motivating example of a private transaction Alice the sender may need to prove that the amount she's sending to Bob is greater than zero she'll need to prove that she has enough money in her account to make this transaction she'll need to prove that she's encrypted the same amount with

respect to both both public keys and finally she'll need to prove that the ciphertext are well formed for our second truth and lie a question a lot of people ask is fhe useful or useless on its own I would say that fhe without zero knowledge proofs in the web 3 space is frankly useless you really need these two technologies to work together to do anything meaningful there is a very large compatibility issue between these two technologies fhe uses something called lattice based cryptography the most efficient zero knowledge proof constructions do not use lattices how do you combine these two technologies and get good performance that is an open question it also turns

out that in combining fhe and zkps it is not fhe that's the expensive part it is ZK piece so the expensive part of the solution is proving you have a valid encryption it turns out this is very expensive with regards to both prover and verifier time you might consider using a lattice based proof system but you are likely to end up with gigantic proofs we're talking hundreds of kilobytes to megabytes in size it's also unclear if prover and verifier times will be that much better than using something based on elliptic curve or hash based cryptography and Rick will tell you all about the proof system we're currently looking at at sunscreen

thank you robital my name is Rick and I'm working on some of the zero knowledge proof stuff that I'm going to tell you about so the first thing we have to do is we have to show that a ciphertext is well formed and when we're doing that using something called the short discrete log proof whereby you set up your lattice relation as equals T where a is a matrix that contains your public key among other things T is your ciphertext and S is the witness known to the prover which contains the message the noise and some other things kind of intrinsic to the proof the prover then decomposes the coefficients in their polynomials into binary to show that they are

sufficiently small this is going to show that you're not making a ciphertext with an immense amount of noise that won't decrypt properly then the approver has to make a commitment to it a Patterson commitment to it and shows in zero knowledge that their witness actually indeed satisfies this as equals T relation um so once you've actually implemented uh this proof system uh the prover times turn out to be pretty reasonable the proof sizes are under two kilobytes unfortunately the verifier times are still several seconds long um so if you were to actually deploy the system as is you would run into some

challenges the reason for this is the short discrete log proof uses an inner product proof similar to uh bulletproofs and so as you show if you want to prove that say more ciphertexts are well formed or if you want to increase the lattice Dimension you're using or if you want to increase the ciphertext modulus all of these things will blow up the runtimes of this proof and so we're currently working on using gpus to accelerate scalar inversions scalar multiplications and multi-scalar multiplications surprise surprise that's a recurring thing so we're trying to speed all these things up so that we can get reasonable verifier times

so once we've shown that a ciphertext is well form we now need to show that the messages within these ciphertexts Obey whatever properties the system requires so for example when I want to send ravatol some money because I spent too much on a drink last night I have to show that the amount I'm sending her is not a negative value and I have to show that it's less than my account balance ah so to do this we use bulletproofs for many of the kinds of things we want to show we're doing Simple comparisons for example in zero knowledge these are fairly small they're under a thousand constraints under a thousand multiplies prover times are well under a second verifier times are 50 milliseconds

somewhere there were about and proof sizes are also under two kilobytes so bulletproofs are perfectly fine for this so now that we have an r1cs circuit that shows some kind of properties of some Cipher messages in ciphertext and we have the sort of discrete log proof showing the well-formness of some ciphertexts how do we show that the inputs to the r1cs circuit and then the message that's going into them is in fact the same message you used when proving your well-formness of the cyphertex and it turns out both proof systems use a Pederson commitment at their core to their inputs

and so what you can do is use the same generators for both proofs neither of them use this trusted setup you can break the Pederson commitments into two parts in both proof systems into a shared component and a non-shared component the prover can publish this shared um commitment and the I guess non-shared ones as well and then the verifier can pass the same shared commitment to both proof systems regenerate the total commitment and continue with the proof the approver also needs I think they need to reuse the blinding factor in both proofs so that um the stars align and the proofs can be verified

so we rather than just using bulletproof's r1cs directly we built a compiler so that maybe we're not married to any particular proof system if we ever need to change this in the future our our zero knowledge proof compiler is currently ongoing work but we already support gadgets types and you can use public or private inputs so some of the inputs may be known to both approver and verifier some of them only to the prover and the approach we're taking with this is very similar to our fhe compiler where you write a circuit you describe it as a function in Rust and you put this like nice little macro on it and then you Pat you can pass that function

to the fhe compiler and it will spit out a directed graph of all the things that need to happen and the nice thing about this is you get in Visual Studio code you get like little red squiggles when you make mistakes you get syntax highlighting you get uh you can publish these things on crates.io you get all of this for free we didn't have to build any of this infrastructure and the API for using r1cs circuits since sunscreen is very similar simple and exactly what you'd expect you compile an r1cs circuits you can then prove that you know a witness that satisfies it and the verifier can then just verify that proof

but as we mentioned we also have these short discrete log proof and these things are a bit nastier you have this a matrix and you have how do users Express this uh like here I want to show the well-formness of three ciphertexts so what does that API look like furthermore users are going to need able to specify which parts of the witness they want to share between the two proof systems so that that API is also kind of indeterminate and we're still thinking about that so if you want to build an fhe compiler for web3 you have to tackle a number about of issues uh it needs to support a scheme that is actually important to

web3 so bfv or tfhe you have to make circuits that run on the order of milliseconds not minutes you have to effectively use the hardware in your machine when running the circuit sunscreen does this today it will automatically paralyze execution down your depend dependency graph and the kind of primitive types used in uh TF in the fhe schemes so it'd be for example their polynomials over zp which are really annoying to work with so your your compilers ideally expose types so that users can play with things that are more friendly like integers

some operations like re-linearization which you should do after multiplications the compiler can automatically insert these for you so that users don't have to think about them and finally most compilers today they think of the world as you're going to compile and run this one circuit so you feed some inputs to it you run the circuit you get some outputs and then that's the end of the story you don't do anything else like maybe you decrypt the output but um in web3 this isn't really how things work you're going to have some data that's on chain and maybe I send Robert's all some money and so this this impacts and decrements my balance then she sends me some money this increments

my balance and so the same ciphertext is being transformed over time and so the data is actually going through multiple circuits potentially even different circuits and finally as we've kind of explained uh you need zero knowledge proofs to go along with fhe otherwise I can just send random values to The Ether and who know like you're just gonna random garbage if you do this so you have to prove that the input is well formed and valid so is uh fhe currently usable unusable well we need a bit of tooling before we can truly use it in web3 in particular we need the tight

integration between zero knowledge proofs and fhe so now that we've kind of discussed some of the challenges facing fhe and its adoption in web 3. we can start approaching talking about Solutions and how we solve some of these problems so um thanks for attending the talk you can follow us on Twitter at sunscreen Tech or you can visit our website sunscreen.tech from which we have links to our Discord server to our Twitter our blog and our GitHub repository and very excited that we have a zero knowledge podcast episode coming out tomorrow where ravatel talks about fhe and so with that I'll open the

floor to questions microphone [Applause] [Music] any any of these is open so so you can stop playing yes we actually have a playground so if you go to playground.sunscreen.tech you can try it out in your web browser alternatively on our GitHub like so all this is open sourced and additionally we have some crates published so you can just download as a dependency and use it any questions

foreign [Music] I don't think we currently have any plans to support those but that's something we can investigate in the future though

maybe you should answer that one so this project started out while I was a cryptographer at news Cipher I was working on secure private functional smart contracts you can guess that abbreviates to SPF the fact the founder there hated that name so thankfully it turned into sunscreen foreign [Music] yeah so I would say there's a few things

going on there I agree that a lot of applications just need homomorphic addition by itself particularly private transactions so that's not the best use case what we're really imagining is that using fhe combined with zero knowledge proofs can be a more lightweight solution for the user because there is less things for them to prove so we're imagining it as supporting General private smart contracts in terms of interesting applications of fhe outside of web3 of course A lot of people are interested in private machine learning so doing private inference where you definitely need homomorphic multiplication I hope that answers it you want something what thanks guys

[Applause]