ZK9: Non-malleability of zkSNARKs - Michal Zajac (Nethermind)

14 Apr 2023 · 14:34

A ZK9 Summit talk from April 2023 in Lisbon, in which Michał Zając of Nethermind examines non-malleability in zkSNARKs. He contrasts the baseline security notion of knowledge-soundness with the stronger property of simulation extractability, which guarantees that proofs cannot be reworked into valid proofs for a different statement, and explains why most zkSNARKs in the literature are proven only knowledge-sound. The talk works through real-world use cases where non-malleable proofs matter in practice.

Speakers

Topics

Transcript

foreign [Music] so he's going to be sharing a little bit about the simulation extractability of ZK snarks everyone please welcome Mikhail to the stage [Applause] great to be here in program you you will see like a bit different uh title for this talk namely normal ability of zika snarks but these two things are mostly equivalent so um yeah so so let me introduce you to to the problem of uh well malleability of of ZK snarks

but let me first figure out how to work with this thing do I need to oh okay so um so so the question is how do we prove uh security of of zero knowledge uh zero knowledge proofs security meaning how we make sure that that the malicious prover

cannot prove a false statement or make a valid proof or a statement he doesn't know the witness for so so usually what we have is we we have some algorithm a like adversary okay uh we we input some some public parameters we we give it like uh SRS structure reference string if if we use one if we use a trusted setup and because uh well most of Novel SDK snarks use random Oracle model we also give the adversary Oracle access to well random Oracle and

with that input we ask the we asked the adversary to produce some some X and Pi okay and if we have uh if we want to show that that our snark is sound then we require that it's impossible for for adversary to come up with with a proof or false statement so for a statement that does not belong to some predefined language and if we want to show that uh that the snarky's knowledge sound which is like a stronger notion much more popular because of various reasons we we require that a cannot produce a valid proof for for a statement it

doesn't know the the corresponding Witness Okay so what does the adversary know so so the adversary know exactly these things we we let him know so so he can make some queries and gets this this input um so so so in principle the adversary is not allowed to learn anything from from external world and this is a bit problematic right uh because in in real life uh we we may see uh like a lot of uh proofs flying around proofs for for valid statements uh

proofs for uh generated by by honest uh by Honest provers um so so in principle it may happen that even though our snark is sound or knowledge sound so it's secure in this isolated idealized model where where where the the knowledge of the adversary is very very limited it may be the case that this adversary given access to to this proves that that are somewhere in there like in his environment is able to to build like uh like a new proof for a new statement so it can can build uh

approved for a false statement or proof for Satan doesn't know witness for uh so so uh why non-malliability matters uh let me give an example of of tornado cash okay it's it's a very simplified uh simplified variant of tornado cache but I think it illustrates that the problem so uh so so so so we have a party a with some account a that wants to deposit 100 ether into uh into tornadoes okay so to to that end this this party creates a coin with some secret SK and some nullifier NF

okay then it adds uh the coin to to to the to to the Merkel tree in the tornado customer contract and updates the route of of the miracle tree uh and that's uh how it can deposit like say 100 100 ether to to This Tornado Cash Smart contract okay uh then when this user wants to withdraw the funds uh he can create like a new account like account B okay we'll we may think that this is the very same guy who who deposited but like coming from different account you know

to to to break the link between like identities um and then this account B claims uh some particular coin c by uh by showing proof of knowledge uh for for this secret SK the the same secret as in this coin uh during the the deposit uh and some particular nullifier enough so more precisely it makes uh proof of uh of knowledge for for X being the the current root of the miracle tree the nullifier and f that this nullifari is is revealed and used for uh to to prevent the double spending attacks and

and some value B which tells where the funds from the from the mixer should go to okay so so this is very important that this B is is here and the weakness is is basically all the secrets um this uh this account created while uh while depositing depositing the funds okay um so yeah so so this this user sends some uh some sense statement X and and the proof for for for that for that statement uh so assume that the snack we

are using is malleable um so in that scenario we may have an adversary like some adversarial account C that observes that this this particular instance and proof pair and based on that creates a new new instance along with with new new proof okay we assume that this adversary learned something from x pi to create X by pi Prime in particular this uh this x x Pi P Prime uh maybe

um this x Pi maybe a statement with well root the same nullifier as in X but with B substituted by C right so so this attack would would result in account C stealing funds from from account B and the important thing is that standard say standard definition of of security for snark doesn't prevent such attacks okay so actually like a stronger security notion is is required it's it's uh and this notion is called simulation extractability it's not a new notion

it's it's been around for like I don't know 20 30 years probably um but I think like with with this rise of uh of applicable zero knowledge we should pay much more attention to to this um to this notion so um how we can show that that the snark is simulation extractable on or non malleable so use basically like two roots one is we can use a transformation so we have a number of available transformation that basically take a snark and add some elements to it and make it non-mallowable this way like for

example this transformation may add like one time signature thing May encrypt the witness and also like show that the encryption is correct there are some Frameworks that that discuss discuss this this transformation like lamasu tiramisu there's also like a number of classical result and these results are great however the problem is that they come with a cost right because now we our the statement we are showing is is bigger and the verification is also bigger so um so yeah so so we pay uh by by introducing efficiency loss

on the other hand we can prove directly so we can take a snark and like show that this particular snark is simulation extractable so so that's uh say uh longer longer way because we need to analyze say snark by snark however it introduces no efficiency or or security loss um so the good news is that the the requirement on snarks to to be simulation extractable are very mild okay so wow for a snark to be simulation extractable we require it to be

knowledge sound so I okay that that's really mild because if snark is not the knowledge sound then well uh it's not a very interesting proof system uh it needs to have something that's called K unique response property which I will introduce in a moment and its proof needs to be simulatable um without using a trapdoor so if you have you are aware how we show zero knowledge we show zero knowledge by introducing a algorithm called simulator that is tasked to produce um a proof that is indistinguishable from the proof uh provided by an honest prover but without knowing the witness

so so we need to add this simulator some special powers and if we are in a trusted setup snark usually we provide the simulator with uh with a trapdoor uh or and if if we don't have any any trapdoor then we allow the the simulator to program random Oracle so so to uh to to say that random random Oracle on input X returns y okay and but don't worry this simulator party is like only artificial party that is used for uh proof purposes okay so um let me dive in into uh these these two

two properties so we have unique response property so uh basically what we are saying here is that at some point the the protocol the snark we have becomes deterministic like the prover's actions become deterministic so so the the proofer uh takes challenges that they approver uh can like digest like previous messages from the protocol but does not add any Randomness to uh to the transcript how much time do we do I have one more minute okay so let me skip to uh let me uh skip that so uh okay so so the bottom

line is uh that virtually any snark we are using and they're all simulation extractable um and even like graph 16 is simulation extractable but with a bit weaker definition of simulation extractability but but this situation is definitely like not granted right like we had to to show like uh we we had to show a protocol by protocol that they are assimilation extractable so so I I believe it's uh it's a bit like a call for Action uh because uh we have this free well-defined properties that are I would say quite easy to show especially if uh if we are use polynomial

commitment like kcg uh so when you design a new snark think about simulation extractability there are results that will help you showing that the snark is in fact simulation extractable or non-malleable so please use them and and please make sure that your new novel beautiful snarks are also secure against the attacks I described thank you very much