Simulation extractibility of zk-SNARKs: from theory to practice / Ignacio Manzur

Transcript

foreign [Music] can everyone hear me good all right so I'm Ignacio I'm with the nethermine cryptography research team and today we're going to talk about an important property of certain proof systems in particular zero knowledge proof systems um just so we make sure that we all understand what we're talking about so what are CK snarks so ZK snarks are special proof systems for relations and we recall like very quickly that

very formally a relation is a subset of strings binary strings and when you have a relation you have an Associated language which is essentially the set of strings such that there exists another string such that the pair is in the relation you should really think about these as being instances and Witnesses for that instance and we are concerned with proof systems snarts that are for NP relations so these are the languages such that if I give you the instance and the witness you can actually decide whether the pair is in the relation in polynomial time very efficiently our finding uh such a witness for a given instance might be

extremely difficult and the point of the prover is to show to a verifier that it has the knowledge of that Witness this is very important so what does this acronym stand for so ZK is zero knowledge essentially what that says is that very informally when the prover gives its proof to the verifier that it knows this witness the verifier learns nothing except for the fact that the prover knows that Witness the S stands for succinct which very simply says that the proof is short formally the proof should be sub-linear in the size of the witness non-interactive this is the n

it means that the prover only sends one message to the verifier and the verifier then decides to accept or not um this only this unique message that the prover send usually is called the transcript and AR stands for arguments meaning that this proof system should be sound which means that whenever you have an instance that is not in the language the prover should absolutely not be able to convince the verifier that it is um and what we ask here is that this property only holds against again computationally bounded provers essentially so if you're very observant you notice that we're missing the K so what is the

k for and that stands for knowledge okay so what does that mean so here we have an adversary um it has some public parameters for this for this proof system it has some reference strings so we're in the trusted setup case and it has access to some hash function or an oracle outputs an instance and approve transcripts okay so let's just assume that this proves transcript causes verifier to accept with like some non-negligible probability then what we ask is that essentially there exists an efficient algorithm which is gonna output a witness for that particular instance in some sense the adversary had to know the witness because it could just run

this this efficient algorithm itself so this is a property that we usually call Knowledge soundness it's a very strong property it usually implies soundness and and and and and we we only we only require that this this efficient algorithm extracting Witnesses for when the adversary can convince the net to verify with non-negligible probability okay so what is not like what they do not tell you in this definition is what the adversary really knows so somehow this definition assumes that the adversary is isolated it has only access to the to the proof systems parameters um is that the case in the real world

absolutely not in the real world what the adversary has like if your proof system is running for example on a public blockchain the adversary not only has access to the proof systems public parameters it also has access to a lot of instances of people proving their own statements and the actual proofs of these statements so what if the adversary sees all of these proofs and then says well here is a way to kind of modify them or combine them to prove a statement for which I don't know the witness this is absolutely not covered by the knowledge soundness definition so we need essentially when we deploy proof systems publicly some stronger security guarantees so why does that matter for example so

let's just take this example right here wherein this dog account a wants to create a coin and send it to account B what it does it it sends it to a mixer and then the account B should claim that coin by essentially showing that it knows a secret and usually we do this with a proof system uh with a ZK snark but now here's this very sneaky cat and it sees the proof instance by account B if your CK snark doesn't satisfy this stronger security guarantee what can happen is that the the discount sees the proof it modifies it into a proof for

the statement that the the coins should go to its account itself and it doesn't have to know witness necessarily for it for this to happen so this is a quite a serious problem so how do we prevent this so we need to show that the adversary cannot turn the proof it sees into proofs for statements without knowing witness even if it sees proofs if even if it has access to some proofs it cannot turn them into proofs for its own statements without knowing a witness so there are many ways to do this you could design your your proof systems to be like application specific design where you add for example an encryption of the witness or a one-time signature

or and this comes at at some some loss of efficiency or you could use actually a snark that is already simulation extractable and what that means is that even if you give the act the adversary access to simulated proofs for any statement true and false statements um it cannot come up with a proof for for a false statement or for a statement without knowing a witness because we can still extract it so simulation extractability is this stronger extractability guarantee in which even if we give the the adversary um access to a simulator with for for false and true statements it still cannot come up with its own proof without knowing a witness

so how do we show this so this is actually worked by Ganesh koshaklak corwise Nicolas coenzions in 2021 and very recent work by Dao and grubs which essentially reduces the simulation extractability property to proving three three main properties the first one is K unique response which is essentially a measure of how much Freedom you have in answering the verifiers challenges the second one is in the trusted setup K Prime rewind knowledge soundness which as you will see is some sort of um special soundness if you're if you're familiar with this term for non-interactive protocols in the the transparent setup you only need

knowledge soundness of the of the of the of the non-interactive protocol and the last property is something called programmable zero knowledge um which in The Trusted setup case should also be trapped doorless and some mild conditions on when these properties occurring especially in your proof system what these people show is that this implies simulation extractability and this stronger knowledge extractability guarantee and this is somewhat somehow easy you show essentially that if you you have an adversary that breaks simulation extractability then it can break essentially one of these three properties like it's especially knowledge soundness and unique response

so what I propose is that we go through what these properties mean exactly and then we look at two two simple examples to show how this is applied and how we can essentially improve simulation extractability of many many deployed snarks which is a good news so I might have some positive results which is a kind of rare both in computer science and in mathematics so let's just go with K unique response so we considered uh two mu plus one move protocol so there's the prover always sends the first and the last message and then the verifier sends challenges uh for for each of these messages except the last one so here is an interaction between approver and a verifier and here let's just say the verifier accepts

so usually this Pro the zero knowledge snarks they are constructed in a way that you take this interactive protocol and you make it non-interactive by using something which is called the Fiat Shamir transformation or the Fiat Shamir heuristic in which instead of the verifier sampling for example uniformly the challenges what you do is that you hash the prover messages and to get the the second challenge you hash the first three messages and so on so forth so when we use the Fiat Shamir transform usually what we say is that the transcript consisting of the proverb messages is accepting why don't we include the verifier messages it's because we can always recompute them by hashing

okay so here's another proverb P Prime could be the same and it produces another transcript the K first messages are exactly the same as the previous transcript but the last the last ones can potentially be different so what the k unique response tells you is that if the last messages are different then this new transcript cannot also be accepting it has to be rejected and what you can you can you can summarize this by saying that the probability of having two accepting transcripts which are different because some of the last methods which are different but the K first messages are are the same it's is negligible you cannot have that

and here you say okay but how can the proverb messages be different if the challenges are are obtained by hashing so the challenges should be the same but what I'm not telling you is that you can program the case challenge the adversary has the possibility of programming the case challenge even in that case the having two transcripts that are different but agree on the first game messages is impossible all right what about this rewind knowledge soundness that we need in transparent case so here's a running instance of the protocol where the dots represent proverb messages and the edges represent verifier messages particularly this one is accepting the verifier accepts this instance so what I can do is I can rewind to the

point where where shown in the screen and I can actually choose other challenges to see what the prover does essentially and here when I chose this other challenge C1 tilde um the transcript was actually accepted at the end but when I chose C2 tilde then the transcript was rejected and in in fact I ignore those branches where the verifier rejects the proof so in this way I can build this tree of transcripts where I rewind to the points which is of interest to me and I choose different challenges so what we ask is that when we've built this tree there also exists an efficient algorithm which looks at this tree and says here's a witness for that instance

and in fact here I've represented a tree where the rewind happens only at one point but you could the property gives you freedom of choosing different rewind points and many many different rewind instances it's just that in the protocols when you try to prove it many times you end up with trees that have this form okay and the programmable zero knowledge is actually just a flavor of zero knowledge if you remember like zero knowledge property is essentially saying you have a simulator that can simulate proof transcripts and they are absolute they are identically distributed to the ones Anonymous prover would generate when proving a statement and the programmable zero knowledge

property says exactly the same thing except that the the simulator is allowed to program the K prime prime challenge okay in the trusted case it also has to do so without a trapdoor but let's let's just let's just go over that so here is a here is an example in the trusted setup so this is the the Planck proving system so essentially what happens in Planck is you have an arithmetic circuit and you try to encode this circuit with polynomials where you interpolate the they have fun in two and fan out one so you interpolate the left and right wires

of of inputs with two polynomials and you interpolate the output wires with another polynomial and use the prover is supposed to send that to the verifier and then the verifier and approver should essentially interact with some challenges and in the end the prover should send this this quotient polynomial t at which point the verifier sends uh an evaluation challenge which is called Zed and the prover should respond with the evaluations of all the all the polynomials together with opening proofs so you should think about these commitments at kcg commitments and these openings are the the openings indicate in the kcg commitment scheme so why is that unique response

so the point is that once you've chosen the the the reference string once you've chosen a polynomial and an evaluation point the kzg opening scheme is completely deterministic you you you cannot do anything else so once you've chosen all the messages up until the point where the evaluation point is chosen um you cannot have two different accepting transcripts they will be the same after that so this is essentially given for free by the property of evaluation binding of the kcg commitment scheme so why is it rewind knowledge soundness here's it's a it's a simple little trick where essentially we're going to rewind

to the evaluation point and we're going to choose a different evaluation point and the prover is going to respond with the evaluations of the polynomials at different points and so because these polynomials have essentially finite degree when we get enough points we are going to be able to interpolate and re and recover them so interpolation is a is a is an essentially an algorithm that allows you given enough evaluation points of a polynomial essentially one more than its degree it allows you to reconstruct the entire polynomial okay and finally why is it programmable as your knowledge so the point is here the simulator is

going to do something kind of counterproductive it's going to choose the the polynomials it should commit at first completely at random so this is rubbish it should it should it should it should give something that is it should encode nothing about the arithmetic circuit so it should in particular it shouldn't verify any any constraint of the Planck arithmetization so what happens is as the prover and the verifier interact the the quotient polynomial which should be a low degree polynomial is going to be some very high degree polynomial it's going to it's not going to satisfy anything so how do we how do we kind of trick the the verifier into still thinking that

it's a low degree polynomial well we choose the evaluation point in advance because the simulator can program that point and what we do when we know what the point is going to be is instead of committing to the quotient polynomial which is not a polynomial law or not a low degree polynomial we commit to another low degree polynomial which agrees on the evaluation of the particular Point we've chosen and when we do that essentially the verifier is going to accept this proof just because the opening of the kcg opening is going to be valid and we can do that precisely because we can choose the evaluation point before choosing what the commitment to T is going to be

so here very high level we've shown that Planck satisfies the three properties that it needs to be simulation extractable which means that if you want to use Planck as as a as a public proof system you at least have the guarantee that people cannot take proofs it's they see on on your public blockchain for example and turn them into proofs for their own statements without knowing a witness all right so let's look at the transparent example so let's look at the if start protocol for example and here it's very similar so the proofer is supposed to send commitments to some polynomials some witness polynomials and the verifier at some point sends

this Q point which is also supposed to be an evaluation point and the decision process is such that supposedly um the the evaluations of the witness polynomials that the the verifier sent are supposed to satisfy some constraint equation which is given by this equation star it's not important why what it encodes it's just it's supposed to to satisfy this equation and how do we check that the evaluations of these polynomials are are correct uh with the commitments here the commitments are not kcg they're actually Merkel commitments so you put the evaluations of the polynomials on the leaves of a Merkel tree and you hash that and you get a root and that's your commitment to your polynomial so the way

that Stark enforces the that the evaluations are correct is actually applying the Fri low degree testing to this function G which essentially is a low degree polynomial if and only if the witness polynomials are low degree and furthermore they evaluate to the alphas and the betas at the points at the denominator so why is this protocol K unique response and here the point is that we're going to late and we're going to wait until very very late in the protocol when we open the the points in in Fry this is done by essentially showing a path to the to the Merkel route

of the Merkle tree you've committed your polynomial with and this is if your hash function is it satisfy some some some obvious properties like let's say Collision resistance or premise resistance this is going to be deterministic in in some sense like the it's going to be extremely hard for approver to kind of cheat you into into thinking that it's open correctly because it has to find essentially collisions in the hash or like pre-images in the hush and why is it programmable zero knowledge so here the the technique is essentially similar to what we had with for for Blanc is that the simulator is going to choose the polynomials completely a random so again this is this is this is bad usually it won't it

won't satisfy the the equation star at all so what you do is forget about the polynomials let's just choose alphas and beta such that the such that the equation holds the constraint equation so why can we do that for example we can choose everything at random except one beta and then the equation becomes linear in the in the in this last variable and so we just solve for the the last variable so once we've done that we claim that the polynomials we've committed to evaluate to the alphas and the betas that's absolutely not true so in general this function G that we apply the low degree testing to is not it's neither polynomial it's not a low

degree but what we can do is that we can again program the points where the fry protocol is gonna is gonna kind of ask for to see evaluations of that function G and we're going to interpolate G with a low degree polynomial over these points and engage in the log degree testing with that function instead so that's a complicated way of saying that we know which points are going to be queried because we can program them so with this additional knowledge which we don't usually have we can trick the verifier again into thinking that we have a correct function that we satisfy all the necessary constraints but but we don't uh

essentially so that's how the simulator is going to be able to produce transcripts for the for the proof um and so this shows that the the the the start protocol is also uh simulation extractable and satisfy all the all the nice extractability properties that we talked about and now if you're very observant you notice that for example in the Planck case the protocol the way the protocol was set up mattered for for for how these properties were found so uh Casey kcg gave us like unique response then we had like uh to interpolate by choosing different

evaluation points and so on so the the plant protocol kind of it mattered how it was set up for us to be able to prove these properties but here in the East Stark example sorry you you kind of see that these properties only were only dependent on the fact that we use the fry protocol to test the load the greenness of this function like it didn't really matter what happened before that point or after that point like the only thing that matters is that the low degree test or the evaluation test was the fry protocol so essentially what you can show or try to figure out is that you can generalize this for all fry based snarks and when you have a fry based

narc which in which the decision process of the verifier is such that it accepts if and only if you have polynomials verifying a certain constraint equation and the evaluations are checked using fry again you can use the same exact tricks and and show that essentially um this will also satisfy simulation extractability and and and this stronger simulation extractability grantees so what's been really positive I think is that essentially all your favorite snarts are simulation extractable like Blanc Marlin Sonic bulletproof Spartan eth Stark plonky2 they've all been shown to be simulation extractable so even

gross16 in in some weaker sense it was also shown to be simulation extractable so yeah there it is thank you very much for your attention and I hope you enjoyed this talk fantastic that's been very detailed very in-depth I'm sure we have some questions from the audience the gentleman right here in the center is going to wait for a microphone before he asks his question because there are thousands and millions of people watching online and they want to hear your question go ahead that's a lot of pressure no pressure yeah thank you for the presentation loved the way you explained it it's quite a complex topic

I as a developer myself face this problem quite recently and like seeing this breakdown like that is awesome my question is do you see that actually as a developer building on top of uh ZK snark Starks like should I actually care about that or should the protocols itself always integrates motion and Drug stability or non-millebility inside of the like when they designed the protocol so that I can just relax because right now we're building our own solution we have to work around to potentially prevent uh solution and extra stability like no ability Problems by hashing and doing some extra work so what do you feel like about that well I mean it depends I guess which which proof system you're using I mean if if if you were

lucky and it was in the list I said of the ones that were simulation extractable hopefully you don't need to care that much about it if it hasn't been shown I think it is a potential risk that someone figures out a way to as you said modify this proof like if if you don't satisfy normal liability in which case I think it should be important to add for example a one-time signature or an encryption of the witness as you said to make sure that your protocol is non-maluable which proof system are you using in particular I mean that's the problem for us so we are generally quite flexible so we plan to use Noir and their underline system but it's it's the problem is we need to figure out if they actually are

simulation extractable or not and that's a problem so I was wondering if it should be an industry standard where all the proof systems that are used should be by default simulation instructable so that we can just have peace of mind I think um I I think that's true especially if you're if especially if your proof system is a condition for you claiming for example uh your coins or some if if the non-malliability can uh it yeah the the security of of the funds in your protocol is dependent on the normal liability of the proof system you're using then I think absolutely yes and one more question a quick one um are

all interactive Oracle proofs non-allible or not there was a result for that or you don't know I think the simulation extractability definition applies to protocols that are non-interactive uh in some sense thank you thank you super in-depth you got more than one question into the block there someone else have a question yes no maybe one question from my side how long have you been working on the topic on this particular project from this particular topic uh it's been maybe three three four months

yeah and and where is it going from here so essentially like when we started we wanted to so the simulation extractability of the fry based protocols wasn't very well understood and hadn't been kind of so what we're planning on doing now is essentially publishing the write-up we have on on on on this topic and yeah hopefully uh also work on on some other deployed uh snarks which maybe haven't been analyzed yet and are you cooperating with some other projects teams I should mention that this work was supported in part by

a grant from the Xerox Park Foundation but at the moment it's been only the Netherland cryptography research team on this project okay super cool if there's no other questions from the audience go in once going twice Zara also no no questions no okay very good thank you inazio super thank you [Music]