ZK12: Towards Verifiable FHE in Practice - Michael Walter

Transcript

[Music] hey okay thank you guys uh we're going to continue this FHA segment with Michael from Zama for next talk before the break right um hello okay yeah um thanks uh thanks also to um private and Rick for a great introduction to my talk thank you um so this is based on joint work with Lou who's also with Zama and I want to talk about verifiable F which is something that we're very excited about

and I hope I can convince you uh or explain to you why um all right since time is money let's Jump Right In what's well you just heard it right like FH is this amazing primitive that allows you to um encrypt your data send it off to a server the server can compute on it and send you back the result and it never needs to decrypt it doesn't need to know the secret key it can just do it and in this sense it enables um uh privacy preserving Outsourcing of computation so you can you know Outsource your competition without having to compromise on privacy and then you have a um you know this thing that you guys all know of in the snar community or in the Z knowledge Community is this technology called snarks which is sort of complimentary in the sense that it allows you to enable U

or it enables verifiable Outsourcing of computation but doesn't have really privacy guarantees now I'm you know I'm ignoring the Zer knowledge part of snar for this talk which is uh you know um weird for the cas suit but uh bear with me um this the kind of privacy you get from the knowledge and this in this setting is a different kind that like a different kind of privacy that what we want out for the input of the data of the Computing party or of the client uh that's not doing the computation so it allows you to do the U enables verifiable Outsourcing of computation but doesn't give you really the Privacy guarantees that we're looking for and so the natural question is can we slap them together to get something what's called ver fial F which would allow you to Outsource your uh your computation uh

both in a privacy preserving Manner and make it verifiable and that's kind of like the dream of out and computation if you think about it right like it's verifiable and private which is essentially like running it on your own machine is just you didn't have to run it on your own machine it doesn't really get better than that it only gets more efficient hopefully let's see um but yeah so that's what we're going to try to do uh we're going to try to um combine FHA and snarks uh I should probably say that um there might be other ways to get um this kind of primitive that allows you to do privacy preserving and verifiable aism computation um potentially uh we're going to go to the FHA and snar Route and even if you look at the FHA and snack route you take a step back um

there seem to be several ways of how you can maybe achieve this uh there's two obvious ways ways you can do it you know you can uh take your FH scheme where um you get a circuit that you want to evaluate on your plain text Data the fhe scheme tells tells you how to turn that into a circuit on uh Cipher text and then you can take this circuit on Cipher text uh and prove it using your snark so you can prove the cyhex operations using the snark um so in some sense you're running inside the snark you could also do it the other way around you could potentially run the snark inside of AG which means you know like um you have the circuit that you want want to compute on your plain text and the Prov that uh you know proves that you did it

correctly uh is also just a circuit so you could also homomorphically run this inside F right and so you would homomorphically compute the proof inside the cyer text so these are two different uh fundamentally different approaches of how to do it and from a performance uh standpoint it's not quite clear which one would give you the best performance uh probably depends on you know which kind of schemes you try to combine here um interesting though if you uh look at it from a security standpoint there's a surprisingly clearcut answer which is you do want to run your F in and snark you want to use the snark to actually um verify the or prove that you did the cipher text operations correctly um and why is this um that is because it allows

the client to verify the proof first before it decrypts and that is actually quite important so from crypto we kind of know um that the decryption operation is a pretty sensitive operation because it involves the secret key and the secret message pops out so as soon as soon as there's like any kind of signal that the adversary might get back from this decryption operation it can try to tamper with Cipher text and try to learn something about the secret key or the message and it really helps the security if you can verify first that nothing fishy has been going on with the cipher text before you actually apply the decryption operation right so I'm going to talk a little bit more about security later hopefully time permitting but I just wanted to motivate um what we're

doing and why we're doing it the way we're trying to do it okay I hope this is uh somewhat clear um you want to First verify and then decrypt so what we're going to do is we're going to slap a snark on the FH instead of the other way around okay so we have these two complimentary um Technologies we have FHS we have snarks uh are we done well in theory you could potentially say yeah but in practice uh you run into quite a few problems when you try to do this um and the over arching problem problem here is that uh both Technologies sort of incur overhead and the combination like you know gives you overhead squared essentially so um with this in mind so you know we just talked about FH or Rick and Ravid aled um and an F you have something that's

called Cipher Tex expansion which means if you encrypt your data your Cipher Tex are going to be larger than your data that you encrypted so but that also means that the the cyhex circuit is going to be larger than the pl teex circuit you originally trying to compute so the circuit gets significantly larger uh by encryption just by because you're running it in FH which you know with snarks we know that they're pretty sensitive to the size of the circuit the larger your circuit the slower theover and also the more memory intense um second you just heard you have this this uh bootstrapping operation which in any FH scheme like all FH schemes that we know of today um need to need to do this because they all work with noise so at some point you will have to do it um and it is

typically the costliest operation in your uh in your scheme basically always um and to the degree that it's basically in feasible for large circuits for for snarks to prove as we'll see later um and then in FH you typically um have your operations your cyer Tex operations are usually native operations um over Rings very common is this ring is this ring zqx mod x to the N plus one it's just one example but that's a very just to give you an idea of what kind of rings we're talking about and even this zq in front um the Q is typically not a prime uh you know in TF it's it's usually chosen to be two to the 64 or something to make operations very efficient and other schemes need this to be like a product of many primes and

like so there's different requirements for different schemes um and typically this is not a prime so you can't really usually rely on Prime Fields while you know most snarks um do have their operations natively uh over finite fields and that's important for security so there's a mismatch here to some degree and also in FH um especially this boost dropping operation usually requires some non-arithmetic operations as Ral Rick pointed out like many schemes are good at doing multiplications and additions uh but the bootstrapping uh really often requires like non-arithmetic operations um and then um yeah this is not of not always very well supported in different snarks

um again with all of these the the the issue is usually more Nuance than what I'm saying here I'm trying to stay a on a reasonably high level um but this is sort of the general picture the general problems that you run into when you try to combine these things okay so what do we do well we try the best we can we try it anyway and the um the first thing that we're going to do is we're going to pick a very very lightweight F scheme and with that I mean TF not just because uh you know I'm with Zama and at Zama we do like TFG um there's good reasons to pick TFG for for this kind of combination uh because it has a you know it's it's relatively lightweight it's a third generation scheme that uses a very very light bootstrapping

uh right like as um you know it was explained before you have this gen two and gen 3 uh kind of um f schemes and the gen two schemes you can think of maybe like as um as or I like to think of them as like these huge trucks where you can you can put a bunch of stuff in and then get it from A to B it's going to take you a while but you can transport a lot of stuff at the same time so your latency is going to be not great but your throughput is pretty it's going to be pretty reasonable on the other hand these third generation schemes are more like little sports cars right like all it's going to fit is like your shopping bag but you're going to be get from A to B really really fast and so you know latency is going to be good

throughput you know depends on how many sports cars you can drive I guess so um yeah so so and when you're going to try to apply a snug to something where you know it's going to be challenging at anyway maybe not try with a truck maybe try with a sports Cary so that's what we're going to do um and this has also like TF has this nice feat that it can be par parameterized um with a with different cyhex modulus like the cyhex modul is a structure it doesn't really matter too much as I said usually it's selected to be a power of two for efficiency reasons but it doesn't have to be actually the scheme works just like picking any any uh any modulus uh and so you know looking ahead as you can see what we can do is we can make it a

prime and we can pretty much make it any Prime we want as long as sort of like reasonable within like sort of uh this roughly the same size as what we usually use for TF um okay so we're going to match TF up with plunky 2 so plun 2 um I'm assuming it's uh you're famili most of you are familiar with it um it's it's a great snark it's like a um yeah it's a combination of uh plun with fry and it's concretely very efficient there's like very efficient implementations out there um it's a snark that is transparent and publicly verifiable which are nice properties that's going to carry over to our scheme when we do this uh combination and it you know very nice features also that works with small

Fields it works with this uh this this Prime which is called the goldilock prime which is around two to the 64 uh right like like a 64bit prime which a you know makes for very nice efficiency but also it sort of matches sort of the parameters that we typically choose for tfh um to make this efficient so it seems these two things just seem to to match up quite nicely um all right so are we done and when we do this like uh do we get a nice scheme out well as um you know I supposed maybe explained before in TF there's two operations need to support which is one is addition and the other one is a programmable bootstrapping now addition is pretty easy like addition is literally just

like adding the cipher text the cipher text vectors so your Cipher text expansion is going to take your data turn it into a vector and U you know the addition of the two values is like literally just adding these two vectors so this is pretty straightforward also to do in snark uh but what about the bootstrapping is that efficient and unfortunately uh the answer is no we tried this uh we tried to throw plony 2 just at like we designed a circuit for the bootstrapping tried to throw plony 2 at it um and we like even like very large Amazon instances with like huge amount of memory with like 52 GB of memory or something they ran out of memory just trying trying to do this even for moderate parameters like like not even like real parameters just like

even smallish like toy parameters um it didn't work so we have to do something more clever here um and so this is where we are going to take a look at the the structure of tf's bootstrapping uh and I you know I don't want you to like try to fully understand how the bootstrapping works just from the slide and this is a schematic view of tf's bootstrapping what I want you to to notice is that it's essentially a long Loop the core of the tfg's bootstrapping is uh What's called the blind rotation and the blind rotation is essentially a loop um that goes from zero to n and this n you can think of like roughly like somewhere between 500 and th000 depending on the parameters um that is the the core of

the um of the programmer bootstrapping of TF um right and now you might wonder well you know we do have techniques for this to solve this right like or to prove this more efficiently than just like unrolling the loop in a circuit and you right yes um we can employ IVC to actually um do this proof here and um there's a couple of ways to um to construct IBC uh you know this term has been flying around here for a while um all day and the more modern approach would be probably folding um but plet 2 is not really set up to support folding so we're going to do the Classic route of doing recursion based IVC so the basic idea of recursion based IVC if you

if you don't know um so the idea is that in every Loop iteration you're going to prove that your Loop iteration is is correct but you're also going to prove that um you know all the previous Loop durations were correct by verifying the proof of the previous Loop duration takes a moment to wrap your head around if you don't know um if you haven't seen it before um so what we're going to do is like every Loop o duration is going to be complemented with the verifier circuit and the nice thing about plunky 2 is that it's optimized for recursion so it's very efficient at proving its own verifier circuit um and so this makes this this kind of uh implementation actually quite efficient um and with this kind of Technique we were actually able to improve the boot stripping actually fairly easily even on

like consumer laptops as so you'll see next so what's um so yeah there's a lot of technical details uh that I'm spping on the TRU here um there's a paper that I'm going to link to at the end of uh at the talk go look at it if you're interested but um so I want to just present the the results really quick um these are the parameters that we that we um the um yeah that we that we experimented with and these are pretty typical parameters that are secure so you can use this for correctness and security and it's going to work um Q as I said is a goldilux prime which matches the pl 2 you know F finite field that it's working over um the the N the small N is a parameter that determines how

long the blind rotation is the the loops the number of steps in your Loop um the capital N is sort of like roughly corresponds to your C text expansion um KB and L are parameters the base better before in the talk before is U is this capital B here sort of and El these are decomposition parameters that impact the size of your circuit but I don't want to go into detail here for for now but uh yeah so these are typical parameters I would say for tfh and these are the results that we got and we really focused on trying um to get the Prova time um down and using manageable uh memory and uh you know what we got was you know Pro a time that's you know in the in the range of like 20 minutes for

large L uh AWS instances so 20 minutes for a single bootstrapping operation is fairly slow I I realize that but the main takeaway is here it's not ridiculous it's not absurd like you can run it it's great so for most applications this is going to be too slow um but you know things usually always get better like so or more performant at least so the hope is that with better techniques maybe snarks that are better tailored to FH or even FH schemes that are better tailored to to snarks we can get this down um a fair bit all right so now I've talked um sort of about like you know uh doing this in practice what can this give us and then we looked at this and was like took a

step back and we're like okay what does this actually give us like in terms of security like can we prove that this gives us nice security properties and this is where the academic and me sort of like took over and really wanted to get to the bottom of this um and so oh I forgot to mention sorry um you can play with a code uh it's online it's it's also in the paper so uh but please do not use this for anything that's worth anything like this is really just like academic style code um that is not meant for production at all um all right so let's say um okay so I wanted to talk a little bit about uh security um and what we can prove actually about this combination of of

using an and a snark um can we actually prove that this gives us anything like in terms of privacy and verifiable by the like is this combination actually sound like doesn't give us anything and the answer is yes we can actually prove something in a fairly strong model uh but we do have some key requirements for the protocol on how this is deployed right like one is as I mentioned before it's important that you verify first and decrypt second like whoever is uh in your protocol whoever is decrypting should also always be verifying first um the second is that the client who's decrypting or actually not decrypting the one the client that is verifying actually needs to know the circuit um and the input sa text like they need this for the verification like you could

imagine like doing a snark where you um where these are sort of like U Witnesses of the of the server um and then you know the client could potentially use an extractor to gain them but in that sense our proof breaks down so for for our proof to work you really need the client to know the circuit and the cipher text that uh the the the snar was actually using um or the the server was using to compute the output Cipher text um and you need to be sure that the input Cipher text are well formed otherwise the server could play with the input Cipher text or somebody else could play with input cyer text um and uh which would also be allowed to play with output cyer text just by extension and

so it could you know play with the cyer text and still prove that it did things correctly so you know these three things are sort of key requirements we need for proof to go through uh but if you do have the and we do uh design like a very simple protocol like a super simple protocol for outsourcing of computation which is kind of the simplest you can think of but it has some you know what does this laptop do or like what does a client do when the server behaves in this way Etc um you need to uh you know some some things that you need to be need to take care of but um essentially it's a simplest protocol that you can think of um and we can actually prove security of this protocol in the UC model which is UC stands for Universal

uh Universal composability it's a very strong security model um and what's what's nice about this is that you can even reveal decryptions to the adversary uh so um even if you know you're an application where the where the client you know sense of data retrieves the data uh like retrieves the output Cipher text decrypts it and says oh this is cool I want to publish this and publishes this um then for this protocol in this in this um uh yeah in this protocol you can guarantee that the server actually doesn't learn anything beyond the cipher text well obviously it's going to learn the cipher text um but it doesn't learn anything about the key or anything else

and that's a big no no for FH if it's deployed sort of like a you know in a in a um without a snark for example then you have to be careful about these kind of uh kind of things um and so this is like crypto terms what I'm saying here is that in this setting um you're even secure against the fully malicious adversary like against adversity that is actively secure while usually FH is only passively secure um okay so this sort of strengthens the security of your FH scheme but again very important this first condition for this to hold okay and now uh a little bit of applications what we think what you know we have in mind what we can use this for

well I said uh you know TF supports two operations which is additions and bootstrapping right now we can only do one bootstrapping like prove one bootstrapping but we can now adding additions uh before it is is relatively easy like we can do this now with our prototype uh implementation um and then we can already support functions of this form again it takes 20 minutes is slow but we can do it um and if you look at this this kind of function well if you think of f as sort of like a um it's like an activation function well you got a neuron you got a neuron in like a a neuronet so you know uh it doesn't take too much in imagination to see that maybe uh at some point we'll be able to

actually prove neuron Nets uh and which would enable like verifiable and private AI which you know would be very cool I think um and then there are applications in uh blockchains with private transactions where you know you run your um you run F in the in the blockchain and here there's potential to to like reduce the number of validat to one which might not be actually uh you know saving on this computation on these computational resources might not be the killer here what would be really cool is that you can reduce the trust in the like usually if you run this in this kind of U blockchain you need to trust the majority of uh validas or you need to trust that the majority of validators is honest and doesn't collude um you could

remove this assumption essentially um and then also you could uh Envision like uh rolling this out in this uh um sort of like like a hybrid rollups that in this uh in these private transactions where the proving time might not actually be that much of a problem right like in if in hybrid rollups you only like actually need to provide a proof uh in case there's a dispute and in that case you know that hopefully happens very rarely and if then the proof takes maybe a few hours you might be okay here so there might be applications uh that are sort of like Within Reach I said like 20 minutes for one bootstrap you would want multiple bootstrap many bootstraps but we we might not be that far out from actually applications um as

this might seem at first and this is sort of like U what I want to take away um if you have any more questions I'm here obviously uh talk to me after this or ask questions now and also uh this will take you to this paper um you know this this and this are the same thing um um yes and I'm open for questions thank you thank you very much Michael so we have a question here I don't know who was first um hi uh thank you for the talk uh so you're mentioning that tfh is kind of a third generation schema in FH but I

see here that you kind of combine it with blany 2 which is superseded by blany 3 and there's like other new proof systems so did you consider combining it with kind of the newer systems for zkp yeah yeah so since you mentioned concretely I think plunky 3 is not actually a snark itself it's a tool could to build snarks and we haven't like you could potentially use it to build a snark that is you know more tailored towards FH for example that is a a research direction that we haven't looked into yet but is definitely something that is promising um and we have looked into to other schemes uh a lot of them though so a lot of flurry has been happening in in the realm of folding and that would be very

interesting to look into but a lot of like so far a lot of folding schemes rely on um like discrete lock based systems which you know have some algebraic properties which are nice but they also need like very large fields and in TFG we like to work with small Fields like 64 bit one bit is good enough sorry how about one bit or eight um what do you mean one bit field it's an 8 bit field does that who that said B okay okay yeah we'll talk later talk to me afterwards and you can take this offline yeah sure nice shill nice shill to say okay we have another question here so I have two questions but I don't know if I have

time so go for it go for it uh so the first one is you mentioned that you needed IBC uh which I understand but I wonder you didn't go with PCD for any kind of reason because with IBC you need to fult sequentially if you were to to do it but with PCD you can fold in parallel like as if you had a tree and therefore you get logarithmic uh increase of speed up so is there any reason why you decided to go IBC only or Brute Force recursion with plun to aside from the fact that gold Delux is of course a field that matches well the FH Primitives U so the question was why we're not using PCD why we using IVC instead of PCD so I mean we were focused on um this one bootstrapping and

bootstrapping things we just a loop so you know for that IVC is like as far as I understand PCD is sort of the generation to like larger computation graphs right uh which is not uh something we need necessarily for um for the bootstrapping so um it so you have you have performed your bootstrapping already right so you have all of the intermediate results of the computation so that means you can fold in parallel absolutely everything that you have like you don't need to go sequentially one by one you can just start building a mer 3 and go to the top so you go logarithmically faster so okay so it's a question um so this is the difference between the PCD compiler and an IBC compiler within within these kind of

schemes so I was just wondering why going IBC if you can go PCD which is which can like deliver much better as right right why why not in why instead of doing the loop why not do it in the tree and um um yeah like why why do we do it sequentially and not like in a tree is it I understand why it's done like this because Boot trapping like this it's like ffts at the end or entities or whatever but like why when you are building a cirquit or verifying this computation you don't go towards this route of PCD which would be like likely I think the like PCD would be very natural for the next step which is um you know uh proving multiple bootstrapping like in a circuit and then sort of like combining this into like this is where I see the natural uh

application of PCD U you could also potentially apply it to the bootstrapping and and see if you can um you can get a fast appr out sure I you know this is sort of like a you know our first chart uh try how to do it and I think there's like much to improve here and I would you know invite everyone in this room to try to you know um get your hands sturdy and try to to make this better that would be great the other thing is there's uh one paper I don't recall the name which basically tries to amortise all of the bootstrapping that you need to perform within a single one but the constants are terribly bad do you think that some kind of scheme like this which you don't really care that much about the constants because what you want to do is prove MH the

computation rather than actually executing it uh by itself do you think that these kind of schemes could like you know make some sense within what you're trying to do it could I yeah I I know I think I know the papers that you're talking about um and I haven't really uh thought about it too much yet but it could work yeah it could thank you y thanks uh do you have opinion about ltis based proof systems uh like ltis fault would they solve any of the non-native arithmetic or uh non-arithmetic operations uh constraints uh yeah potentially yes uh we haven't so for lettuce based snarks there's not that

many like very efficient implementations out there like one thing about plun 2 is that like it's very efficient and it's just out there and you can just use it um with lettuce based snarks uh I think they could be useful um let us fold uh we'll see um is also something that's sort of on our agenda to to explore um but one thing is that so folding schemes seem to be or or the promise to to more efficiency is that you don't have to um prove the verifier at every step right like you can you fold these things together and so and so folding is usually simpler than uh doing the verifier circuit in our case actually one step of the loop duration of the

blank rotation is already a pretty big circuit we're talking like two to the 20 something right and um like Gates and um the verifier circuit though is much much smaller for planky 2 so I'm not sure if folding really gives you that like we'll see but uh or we hope to see we hope to get some better results but uh it's unclear how much we will get from this yeah I guess the more interest about is the lest part of that specifically to to avoid some of the those complicated part with slatus based f yeah yeah so so the hope would be for example that you could prove efficiently um TF with the power of two modulus for example that that could be very cool yeah yeah I think PC team privacy and scaner exploration are working on the uh

laus work it's like a framework for building laus based systems so might be interesting to explore that okay thank you okay we'll take the last one hey Michael thanks for the talk uh I had a question on uh alternative approaches so on one hand you could basically code the bootstrapping and rust running through risk zero on the other hand you could just run the bootstrapping through te right have you compared either approaches and where does your 20 minutes proving time fall in between those two so um I can so we we have a comparison essentially with uh the like

a z KVM approach unfortunately Z kvm's introduced a lot of overhead and uh for the kind of circuit that we were trying to prove um they're much slower uh and also like to the to the extent that we weren't actually able to run the entire thing for for like practical parameters like we didn't look too much into it like with some tweaking maybe it would have worked but uh from micro benchmarks it seems like we at least like two to three orders of magnitude faster with a PL 2 great um with um with T's T's are probably going to be much faster but you know from a from a um uh trust standpoint like or from security standpoint uh you're essentially just

shifting the TRU to somebody else right like uh T's are cool but you know like you're just uh instead of having to trust the person who's running it you have to trust the person who like gave them the hardware so uh I mean yeah um in certain applications useful but not not the same as running it on your own machine right it's not as cool it's not a fair comparison yeah it's not a fair yeah thanks yeah thank you very much so we're going to have a break now half an hour and we'll be back for lightning talks at 3:30 thank you very much and thank you Michael