ZK14 - Making verifiable FHE practical - Daniele Cozzo (IMDEA Software Institute)

Transcript

Yeah, it's our pleasure to welcome Danielle. He's going to talk about verifiable FHE and uh yeah, let's get it started. Up to you Danielle. >> Thanks for introducing me. Um so yeah, today I'm going to talk about uh verifiable FHE and the work we are uh doing to make it practical. So first let me uh explain what is the problem that we are trying to solve and it's quite simple to explain. It's about outsourcing.

You want to outsource a computation because I don't know you don't uh have the resources to run it or you don't have access to the code. Um, and this pretty much uh abstracts uh lots of use cases like machine learning as a service. So you might want to request a an analysis u an a machine learning uh analysis on your medical data or generating an investment plan based on your financial status. a lot of things you can do. Um thing is uh as it is this is not um

this is not good because of course you don't want to upload your your your data in the clear. So we what can we do? We use fullyomorphic encryption. Um it's an amazing technology um that allows um enables uh privacy preserving computation. So you encrypt your uh your data uh you send them to the cloud and now the cloud can do the computation over cipher text. you get a um something in as output uh which is a cipher text you decrypt and you learn the result of the

computation. So privacy is is the issue of privacy is solved. Uh but uh FHE although it's an amazing technology uh it works in a uh in a trusted setting. So we are assuming that the cloud is really doing the computation as it was supposed to do uh which is not guaranteed and FH alone doesn't enforce uh correctness.

So in principle nothing prevents the cloud uh from uh biasing the result or even running a different computation or sending garbage. you have no control on what the cloud is doing unless of course we use snarks. Um so combining a snark with FHE gives what is called verifiable FHE or VFH in short.

So now the cloud is uh asked to provide a proof that indeed it did the right computation. So you appends a proof uh to the results and you check that the proof uh verifies and only later and only then you decrypt and uh learn the result. So VF is uh basically the gold uh standard for secure outsourcing because we get privacy integrity and thanks to the saxine property of snark it's also the proof is also very

easy to verify. So um this is really what we desire in the context of outsourcing. Um so the question is do we have VFC? Um a theoretician would say yes of course we do. Uh snarks are too incomplete. So we can just take a snark and prove the computation over cipher text. There is no nothing new about it. Uh but since we are actually I am interested in practical things.

Uh the real question is can we have it efficiently and well the answer is it is very hard and it's probably one of the hardest problem in cryptography getting uh an FHC that is practical enough. Why is so? Um well there are many reasons. First of all, um, snarks anomorphic encryptions are primitives that work, uh, in completely different settings.

Snarks, as you know, typically work with large frame fields and they process circuits that have a very arithmetic presentation. While FHE uses uh big rings, polomial rings where the modulus is uh is not a prime. most of the times and uses a lot of non-algebraic operations and on top of that there is also a problem of uh size. So if you want to prove something on cipher text you have to take into account the fact that cipher text are larger than plain texts.

Um so the the hover the the overhead could be like 2 to the 6 and yeah so if you imagine like you you can just run to multiply two integers it's very easy trivial uh takes two bytes of memory takes pix seconds on a normal laptop but if you do that in FH then again the size of the cipher Ex means that you have to store the wall process which takes uh kilobytes and it's also slower orders of magnitude slower

and also conceptually is not that easy because you have uh multiplication is tensor product key switching and uh rescaling. So just with that you can start understanding why VF in practice is hard. So I'm listing here three main approaches uh for uh verifiable FHE.

Uh the first one is the generic snark approach. you take a snark, a normal snark, and as I said, you prove the computation over the cipher text. Um, well, it turns out as you can imagine that it's uh it's not feasible uh prover wise because you would have to emulate uh ring arithmetic with uh field arithmetic. You have to uh translate um non-algebraic operations like is switching or scaling and so on.

Bootstrapping again with field constraints and all of that uh would take uh in probably infinite memory and uh the age of the earth to run just a prover. So completely unfeasible. Um second approach is something called um HOP which is uh basically running a snark under FHE. Um, I'm not going into the details of what that is, but uh, normally it's super fast because the snark runs over the plain text as uh, usual, but it has

some uh, problems that are inherent. For example, it cannot be publicly verifiable. Um it's also weak to verification oracle attacks and uh also it doesn't uh work with um a specific FHE scheme which is CKS. It's a FHE scheme used for machine learning. And then the third line of work which is our work um and where we take a different step and instead we try to design snarks that are specific

for FHE operations and this is what I'm going to talk about today and it's based on two actually papers uh one appeared last year at crypto and one in currently in submission. And we realized a VF scheme that is able potentially a scalable with large uh computations and is um well works natively with rings and is able to prove most of FHE operations.

And of course we get uh we get CKS Um so the main contribution of our work is a blueprint for VFHE. In other words, a recipe for designing practical VF schemes. The recipe starts with an FH scheme that in our case will be CKKS and then we make it proof friendly. What proof friendly means? I will explain it later.

Uh then we arithmetize it. So what is the arithmetization? is a process that translates uh FHE operations into a language that the snark understand which in this case would be relations over rings. And the cool thing is that we we show that uh we can express any FH operation with just two relations over RQ. One is um checking arithmetic circuits

and the other one is checking uh ranges. So this is the language our snark speaks. And then we are able to define our snark. Um as as as probably you already know the modern way of combining a information theoretic polomial of P with a polomial commitments and both must be defined over rings. And in particular um the PIOP is made of two components. A GKR style uh protocol for proving

arithmetic checks and uh a range proof uh for proving range checks. This is our blueprint. And now in the rest of the talk I'm going to explain you all these building blocks and the challenges we face when we try to um use this framework to uh design FHE VFHE schemes for concrete uh applications. So first of all let's start with a proof friendly ring.

Um so FH schemes work over rings not over fields. So normally they use this kind of rings uh polomials with coefficients mod Q over the seat atomic polomial. And if you look at the parameters you you can easily realize how big this is. This is really huge. Right.

And this is a matter of fact. Um it's big and we have to work with these big rings. The good news is that we can choose Q&N. And how do we choose them? Well, um we have two goals in mind. uh first uh first efficiency we want to store compute efficiently with these objects and the second goal is what I call proof friendliness.

Um we need to find inside our Q a large exceptional set. Uh why so what is an an exceptional set? It's a subset of RQ where the difference of any two elements is invertible in the ring. Why why it matters? Well, you know that for snarks there is this pilema that says that sness is uh size of the computation over the size of the field roughly. If you translate that to snarks over rings, uh you have to replace field with uh largest exceptional set.

That's why we need to find a large exceptional set in RQ. With that in mind, we take our RQ and we do two rounds of Chinese reminder theorem. first time we apply it to the modulus. So we take Q as a product of primes that are that fits uh a register in an uh computer and this is called RNS form. Q is set to be in R NS form. It satisfies if it's like that. And then we do a second pass of uh the CRT this time with respect to the cytoomic polomial.

Um that way the uh RQ now splits into the product of uh extension fields. And we have two cases. Either uh the the cycllotoic polomial splits completely um which is the optimal case for efficiency because we can use entity uh but the fields now they are not extension fields they are just fields are not large enough for soundness. So we would need to do repetitions and in snarks repetitions it's something that you want to avoid.

So but um second case it's what we do uh we do something in between uh we let the cyclomic polinomial to split uh in um irreducible factors of the grid D. So we have extension fields of the grid D. Actually we choose four for because it's the optimal the optimal parameter. And this is cool because we now these are actually fields of moderate size that give soundness and we can also do efficient arithmetic thanks to something called incomplete entity.

So that was the proof friendly ring. Um now we can instantiate our proof friendly CKKS. I'm not going into the details but just to give you a rough a rough idea of what that is. So on one side we have normal CKKS which works uh over uh a fully splitting RQ. It also has some other problems. For example, when you do a multiplication of morphic operation uh the underlying grain changes which is very bad for snarks.

What we do is we modify it so it works over our proof friendly ring. Uh we can do efficient arithmetic. We don't need repetitions. We also change uh the way we do multiplication so that the ring doesn't change and we do other other uh other things to make our life easier. So that's what uh our prefriendly CKS looks like. Uh efficiency wise, one might wonder, okay, how does it is it slower than normal CKKS? Not really. Um it's just uh 10% 20% slower.

Um so it's it's really nice. Um cool. So next step is arithmetization. So again, arithmetization is a way to translate omorphic operations into relations over RQ. I'll give you an example of how we arithmetize these operations. And one is key switching. Key switching is an FH operation that takes a cipher text and outputs a new cipher text that encrypts the same message but with under

a different secret key. You don't have to understand how it works. Just uh one thing to notice is that if we want to prove these gates there is there are some problems. Uh so this CRT minus one um is a map that takes an RQ element and then composes over the RNS components. And as you can imagine this is not algebra at all. So instead of proving it directly which would generate a huge overhead we do something different. and we let the prover to give us a vector W um that uh

recomposes under the CRT map to C1 and whose components are less than the RNS primes. This tells us that he's giving exactly the result of the gate we don't want to prove and then we can use it to do to compute the the result of the gates. So um as you can see we are there are two uh kind of operations the green ones that are algebraic uh and we know how to prove them.

uh we can use GKR sparn whatever and the orange one which is a rain check and we also know how to prove range checks we have a lot of works on lookup arguments. So we from something we didn't know how to prove efficiently now we ended up with uh two things that we hopefully know how to deal with. You can repeat this with any FHE operation.

Um and it turns out that uh we just need two relations uh arithmetic checks and range checks. How do we prove uh arithmetic circuits? Um we use a GKR style protocol based on some checks. We translate it over RQ. uh we introduce custom gates and wirings to to have it uh for our setting for proving specifically CKKS operations.

And the real cool thing is that uh we are able to flatten this GKR circuit so that it becomes a circuit of constant that four. So in particular it is independent of uh the original FHE circuit and this makes it very very efficient. So you don't have to look at this but this is just to give you an idea of what it looks like. These are the gates and wires that describe uh the GKR circuit. So it's not quite GKR.

Um second we need to prove ranges. Uh omorphic operations as I showed you before produces this w that we need to prove their bounds. The idea is that we collect all of them together and we do a lookup. So this is our vector of the W's. Each rectangle uh is an RQ element and we need to prove that all these squares the coefficients are bounded. How do we do that? We construct a lookup table uh which is the all the possible polomials uh RQ elements with coefficients bounded

by uh B and we do a lookup. we show that every element in our vector is also it also appears here. That's nice but it doesn't work in practice and simply because the table is big. Um so what we do table de composition uh we take a a base beta uh logarithmic b and we reduce one big lookup table into tb into smaller lookup tables into smaller uh t betas.

So we get this smaller looks uh still doesn't work. Uh still they are too big and again that's because of n the ring dimension. So now we need a specific solution for polomial rings. We need to decompose with respect to the ring dimension n. If we do so then we end up with even smaller lookups. Actually they are integer lookups. Now into this integer table lookup table uh namely all the integers from zero to beta minus one and if we choose beta properly then this becomes a

uh a problem that we can attack so that's what we do decomposition but still so we started with RQ vector of dimension n and we ended up with a vector of inte integers uh with a uh n overheads. So question is how do we commit because we need to commit to them at some point. How do we commit to them because we only have RQ polomial commitments. The rest of the protocol works over RQ.

Um the first thing we can try to do is to rembed them into RQ. So we place them into RQ elements. So these are the now again RQ elements. But well okay this works. It gives an RQ oracle. But as you can see there is a lot of wasted space. So this gives an n overheads that if you add to the previous ODN overhead from the de composition we would get something uh really really bad.

So this is not acceptable again uh ring dimension strikes back. Um what is the solution? um we pack the ZQ elements into RQ. So for example, this packed uh vector could be the initial vector. And instead of creating a normal oracle, we create a virtual oracle for ZQ. So it's uh it's not an actual oracle, but it's just an handle. So the rest of the protocol doesn't change. Um what does that mean? It means that the range proof will interact with the ZQ

oracle by making queries but what we are actually committing to and using is the original RQ oracle and we can switch uh to and back using a technique that we developed called packing and unpacking. So we don't have to commit to that ZQ better. And the nice thing is that the rest of the protocol will continue working with the original RQL. As a result, we don't get the O N square overhead. We save N.

We we get an N overhead, but that's inherent from and comes from the fact that we are working with polomial rings. And we can use this whenever we need to do uh something with that Q elements. The last building block is the polomial commitments. So we have uh Oracle access to polomial uh polomials actually to many polomials and we need to evaluate them. What we do is we batch them.

So for the polinomial commitment we chose base fold uh could be something different but we chose base fold because it's field agnostic uh multivariates and so on. It could it was just an arbitrary choice. Uh but then we designed it to also support batching. So if we have to do uh m evaluations instead of having m * log square n uh we are able to separate the log square factor from the batching factor and this is nice because there is a hidden constant factor over here.

Can we go further? Yes. Uh so the polinomial commitment uh the way we design it it's initially over RQ but splits over uh the components. So now notice that for each prime these components are isomeorphic to each other. So this gives evaluation different evaluations over the components. So we can batch them. So now if we introduce uh we can even improve a single evaluation of rings. So if n is the ring

dimension l the number of rns components uh we are able to separate the log square part from the ring dimension which is big if you remember and the um batching factor. So these graphs show the improvement we get for a single evaluation. On the left you have evaluations uh evaluation time uh normal base fold is orange batch fold green and on the right we have the proof size bold is in blue and batch fold is in in in orange.

uh there is also something called circuit preparing but I don't think I have time to to talk about it and it's basically uh a very practical problem when you design as an arc you also need to uh take into account that the verifier needs to to premputee the circuits and uh either evaluate the poloms that encode the circuit or delegate their valuations to the prover and uh because Again we are working with FH the circuit is big it's really big uh although the polomials are very sparse and take uh uh values in Z Q. So there is a problem how do we evaluate

this polomials and well we came up with a do solution which takes advantage of the packing we also combine it with batch fold and we get something called sparse part that improves on uh previous techniques for sparse polinomial evaluations. I'll quickly mention the results we got so far. Uh so this is the first we got uh uh smaller neural networks um two hidden layers, three inputs to outputs.

Uh we approximate the activation layer with cryptonet approach with uh squares and we consider different configurations of the neural network. Um as you can see the circuit size is big extremely big compared to its dense representation. So that's why it really matters to have a an efficient protocol for uh circuit prep-processing. And this table shows you the improvement we get uh from uh previous uh techniques to evaluate sparse polomials.

And these are the times for the uh range proofs. This is actually the most expensive part of of our construction. Uh these are single threaded and we would get say 100% uh 100 times better times if we uh go through uh more threads. uh to conclude my talk. Um so VF is uh hard to get in practice.

Um mainly due to the fact that uh FH and SNOX work with different parameters. Uh cipher texts are big. All these things together uh make it very hard. So we designed a blueprint for designing uh VF schemes that are potentially practical for small circuits. We tested them and we get orders of magnitude improvements over generic approaches and we are constantly we are currently working on scaling up the solution to larger and larger

circuits. Uh one last thing that I I think it's uh worth noticing is that we are really using the latest uh advancements in Snark's literature. Um actually I would say this line of work is actually sort of of playground where you can see all this new stuff um that get put in practice and I think it's really exciting before uh few years ago this wouldn't have been possible.

Thank you.