Advanced security for SNARKs: A survey with Quang Dao

Transcript

all right so for the last talk of snark week I'm excited to introduce Quang who's a PhD student at Carnegie melon and our intern for the summer here at a16z so he's uh already produced many strong results in uh both theoretical and applied cryptography and today he's going to tell us about the security properties of snarks that you really want when you deploy them in actual applications and how to show that they have those security properties I'm very honored to be talking here today at the end of snar quiek which has been very exciting for me personally and I hope for you as well so my talk is going to be sort of a survey or overview of the recent Advanced security results for snarks basically uh what sort of

security Notions that snarks should satisfy when they're deployed in practice and when they might encounter attacks that may not have been analyzed very much in the theoretical literature we all know and love uh snarks they are succinct non-interactive arguments of knowledge and basically what they are is just they are a certificate or a proof that is both short and non-interactive so the prover does not need to do any sort of interaction with the verifier just sense of proof this proof is also very fast to verify and in terms of Standard Security Notions for snarks you want two two of them right the first one is that if the

verifier accepts a proof then it means that the approver must have known some Associated witness W to the statement X and the second property is zero knowledge which says that the proof itself it can be simulated without knowing the witness and these two security properties are proof basically with all every snar constructions if if and I think knowledge soundness is is a must and zero knowledge depending on the snark whether you want it or not okay um and you know snarks have found so many applications both in the blockchain space and Beyond in the blockchain space we have all these ZK rups and the prise

for these uh private smart contracts or private transactions I'm sure a6z has a lot of uh working a lot of with a lot of portfolio companies on all of these uh exciting applications but beyond blockchains there are also many other interesting applications such as image ad station so if you see an image on the New York Times right uh how do you make sure that it has come from a reputable source and this whole process may involve a lot of Transformations from the original image which is very very high quality and so what you can do is you can just uh do a snark of these

Transformations that these transformation have been applied correctly to get the final output uh similarly you can also do a SN proof of correct AI training or correct AI inference or you can show that um do a SN proof to show that your account is not on some given block list on some Federated website and many many other applications so with all of these uh deployments here I guess a very important question to ask is that are these security Notions that are usually proed for snarks are they enough to

guarantee security when snarks are deployed it turns out that in many applications in practice uh these security properties are not enough and roughly the reason why is that for example if you look at knowledge soundness is defin in this Standalone setting you have one malicious Prov that is outputting a proof but in actuality this malicious Pro may see many other proofs from different parties okay and in this context where snarks are deployed we also want to guarantee security when it is composed with other protocols as well with these extra proofs that a malicious Pro might

have then may be a very real uh extra attack Factor here which is called a malleability attack what this attack does is that a malicious Pro may see a proof and then modify that proof to be some other different proof without necessarily knowing the underlying witness at all Mal ability attacks have actually been sort of devastating in practice maybe not for snarks but for Signature skeps so I think allegedly what happened with the Mal go attack is that the Bitcoin uh signatures for Bitcoins at the time were malleable so what could happen is that somebody submit a valid

batch of transactions uh Bitcoin transactions with some signatures then because the signature is malleable someone else some adversary can take that signature M it to be different and then submit that first you front runs the actual valid uh transaction batch and if that can happen then it is a valid malleability attack and you may get all the Sor all the rewards for that transaction batch sort of a a very simplified um scenario for what could go wrong if your snar or your signature scheme is malleable we really want to rule out these malleability attacks in

practice and one such strong notion called simulation extractability will help rule out this attack this is basically adapting knowledge soundness to this more general setting where a malicious Prov may see arbitrary proofs of his choice so let's say here the snark is zero knowledge there's some simulator that can simulate any proof that you want and you give this um access Oracle access to the simulator for the for the malicious prover and you still want knowledge soundness to hold which means that whenever the malicious Prov outputs a new proof If this one is

not something trivial like it has been qu before then it must know an Associated witness to this new proof you can not uh generate new proofs out of nowhere this means that uh you can now forget about Mal ability attacks because every new proof that anyone produces will uh will come with an Associated witness even when you can see all the other proofs it's also very helpful for many uh applications um so for instance in a blockchain uh setting you want your transactions to be non mble right and one way to do that directly is if you

prove the whole transactions with a single snark and that snark is non malleable or is simulation extractable then then you're good if it if it is not then there are ways to make it so that you know compose it with other Primitives such as just ordinary signatures so that the the um the the final scheme is not malleable but that sort of adds extra overhead so it's very helpful if your underlying snark is already proven to be simulation extractable because then it can just be used directly for these applications so these are the the benefits of proving that snarks are simulation extractable

and the question now is are existing snarks uh satisfy this strong property question yeah so that was that definition uh in the context of snarks in the upper left or they were thinking of something else or uh yeah it's a in the context of just proof systems in general yeah it predates the introduction of snarks just when they have proof systems or non- interactive proof systems so let me give you sort of a very quick overview of uh where we are in the context of simulation extractability at the moment there are many popular ZK snarks that have been proven to be

simulation extractable this list includes say cross 16 bulletproof plun Marin Starks uh and Spen and so on with the exception here that cross 16 it satisfied this somewhat weaker notion of simulation extractable where given a proof you can randomize that proof but up to that you cannot do anything else some of these snarks satisfy a stronger notion known as UC security UC here stands for Universal comp composability so I'll talk more in this later it's sort of a stronger properties that also guarantees security when composed with arbitrary other protocols and there now

established templates for proving simulation extractability for Starks it basically boils down to The Standard Security properties so knowledge soundness and zero knowledge plus a very mild property called weak response and I'll get to that later it basically says that uh given a not proof you cannot continue it in a different way at any point during the snark proof on the downside it turns out that many snarks that are deployed uh in practice they lack a proof of simulation extractability it's either because well the the full specification of that snar has not been really written down and

analyzed anywhere it may contains optimizations compared to some original protocols like this is what happens with many plot variants H and so on and also despite having a template sort of instantiating this template uh still require some case-by case analysis there is no uh simpler properties that you can show that immediately implies a weak unic response which then immediately implies simulation extractability so I also get to this when we go to the details so let me go into the details for simulation extractability and then also talk about us security and end with some open questions the central

point in proving simulation extractability is that well it's mostly just knowledge soundness right except that the adversary has a bit more power it has the power to access some additional proofs of his choice it would be most natural to reduce it to just knowledge soundness well that is basically what is happening is that it will be very nice if somehow we can just ignore all the extra proofs that uh it it sees and says that these extra proofs they do not help the adversary in any way towards crafting a new proof and that's basically exactly how these simulation extractable results are proven it just shows that either this

final proof that the appos produces has no overlap with prior proofs or if it has any overlap at all then it must be identical to a prior proof in which case the the output is Trivial and so we're going to instantiate this templates for uh different kind of starks and in fact question yeah what what does overlap mean in this context right so usually a proof you have like uh it consists of some components right and overlap here means that some components are the same but other components are different it's sort of makes more sense when I get to exactly what those components are okay

and I the other question would be so what exactly is the model so like as aover you're I give you like uh you try to generate pi and you get to query whatever you get to generate as many X Prime Prim primes you want for X Prime not equal to X is that how I you think about it yeah yeah you you know you have this simulation article you ask it whatever statement you want even possibly false statement and you still get back simulated proofs for all of them and so you can just get all these proofs but then whenever you produce a new proof it must be the case that you produce that proof in an honest way somehow like you actually use a witness

for that proof or should we be thinking of the simulated proofs as coming from the simulator whose existence is guaranteed by the ZK property or just from elsewhere in the protocol or all of the above yeah um so this really only makes sense for zero knowledge snarks so this is actually the zero knowledge simulator okay yeah I'll I'll get to in a mo like at the end like what happens if there is no zero knowledge and I think it's still sort of an open question to just show non-ability for SNS are not zero knowledge M because the mount GX attack was a malleability

thing where there was no simulator or anything it was just adversaries were seeing proofs and and Molly well signatures and moling the signatures right so yeah yeah but the signature is just like built from a zero knowledge identification protocol yeah yeah so in your application you motivated with that the adversary these other proofs and should not be able to come up with the new proof but here you are giving a simulation Oracle why not giving an actual proof Oracle which takes a statement probably the orle is on mounted computes the witness and computes an actual proof why not why not give an actual orle and instead give a simulation orle yeah um I mean one way is to sort of strengthen the definition

so now you can also see uh valid proof for false statements uh another is just simplicity so if you uh need to like say um you know you you need to model like the adversary can see proof for statements of its choice right so what does it mean for adversary to specify a statement without any possible witness then like how is the proof generated I'm slightly confused maybe like according to Justin questions in in your answer the proof Sim simulation workall is the same simulator as for the ZK from the ZK property but that simulator can be run

by by the verifier even even without knowing the W the witness right like the so in particular the prover could run this Sim simulator even before I even gave him access to this model does that qu question make sense yeah yeah that that question makes sense so uh what I'm sweeping under the rock here is that the simulator has some extra power over the honest parties or even over the adversary right so like if you have a proof in the random Oracle model then the simulator can reprogram the random Oracle queries also don't the simulator sometimes run in uh it's it's like expected Pol time right so sometimes you can yeah in this

model you can just ask it and you don't like think about that but like if you're sitting there running your simulator you can run to situation where you're like oh I'm running forever like yeah yeah simulator has some extra power like reprogram random oracles running expected poly time or have some trapo that allows for simulation so this is basically the the template and inst staning this template is a little different for sort of two separate kind of snarks so this is a very broad uh attempt to classify all snars at least with respect to how simulation extractability is proved so on the one hand you have snarks like Ross 16 which are based on this linear pcps and

basically you have some very long CRS the prover knowing the witness will take some elements from the CRS and then craft a proof consists of some group elements whereas um in the fim miror based narcs what happens is now the two parties actually use a random oracles and then try to um you have originally there is some interactive protocols with uh the verified challenges being random and then you collapse this into a non-interactive proof by letting the challenges these CIS they're derived bya some hash function which we model as a

random Oracle okay so very roughly these two camps of of snark design and I'm only going to focus on the second Camp which uh actually is is sort of how most snarks nowaday are uh produced um for the first cam I'm just going to say that simulation extractability you reason within this algebraic group model or generic group models and within that reasoning you also are going to show that you know if you have a new proof then it cannot have overlap with any of the prior proofs and so on but the reasoning is somewhat different so I'm going to skip it before I show you how to prove it let's Show an example where

it is not the case let's say you take some Fiat Shir non-interactive arguments let's say this this guy just has like two message and one Challenge and then you're going to somehow double this protocol you double it by just um proving for this product relations where you have two different uh statements and two different Witnesses you layer the two execution sequentially okay so I claim that this protocol right here is not simulation extractable in fact this it's very malleable and here's the malleability attack the idea is that because you have these two protocols that are layered

sequentially what you can do is you can have a mix and match attack right you get let's say this malicious Prov is going to need uh to declare two statements right one of the statements is not going to know the witness the other one it will know the witness so then it can ask for just some arbitrary proof of those two statements and it's going to keep the first part like keep the first execution but it's going to change the second execution so when you change the second execution it can do so because it knows this the witness to the second statement this W Prime to X Prime

and because of that it can generate the second part of the of the proof here in an honest manner and keeping the first Parts okay so because of this mix and match attack you basically have a new proof that is this a a star Z Star where this a is part of a prior simulated proof so if like if the statement X here is some of a false statement then the adversary has has won this Mal ability game right so what we want in this in these fiir uh non-interactive proofs is that the protocols should not be able to be broken down like this or in other

words you do not want parts of the proof to be reused later on so there is uh a property that somehow captures this uh this intuition that you should not be able to modify part of the proof and and continue from there okay so this property is called weak unique response so let's dive into what this property is okay so it's defined by this game first your malicious prover it's going to choose any statement at once and then it gets back a a simulated proof now it's going to try to produce a different proof Pi Prime such that these two proofs they differ but they agree on at

least some of the components right the components here just means the individual messages A1 A2 and so on so they agree to up to some point but then they diverge the prover is going to win if it can man if it manages to do this okay so takes in some proof and then produce another proof where there's a branching uh up to some some components or some routs and the claim is that if it is impossible for a malicious Prov to do this kind of attack then it is also impossible for the prover to carry out a Mal ability attack the idea is basically now simulation

extractability is going to be proven as these two Standard Security properties knowledge soundness and zero knowledge plus this weak unique response property let me recall you what the simulation extractability game is again so we have this malicious Prov right it's going to have access to arbitrary proofs of his choice and you're going to want knowledge soundness to hold and what it means is that there is some extractor that's is going to extract out a witness for whatever proof that the malicious Prov outputs and now the malicious PR is going to win if this proof is accepting

but somehow the witness is not a corresponding Witness and also that the proof is not a trivial proof that has been quired before so this is the original game now we're going to do sort of a hybrid into a different game where you want to rule out the chance of approver using a weak unique response attack so now you're going to additionally reject if this pie star has any overlap with a prior P with a prior proof that has been queried basically this is the same condition as in the weak unique response game and so the claim here

which is somewhat easy to prove is that if somehow in game two you abort then it means that the weak unique response condition is is achieved by this adversary and therefore you can break weak unique response right which shouldn't be possible and then in game two now that this new proof has no overlap with P prior proofs what you can do now is you can directly reduce this simx adversary to a knowledge soundness adversary and so you you also win because knowledge soundness is supposed to hold with respect to this proof system so

basically with these two claims you can now see that uh simulation extractability it's just normal Security Plus weak unique response so how is Wick uni response actually proved for various different protocols sorry could you talk more about the proof of claim too cuz like in the know Hess game there will be no oracles so like how do you do the reduction yeah so the reduction is you basically have this adversary it's going to just run a simulator on its own and interact with this P star and the reason why this you know simulation on its own still works is that this output proofs

here have no overlap with prior proofs and therefore um the simulation goes through I see so you're saying like the like there exists some simulator algorithm that this reduction can run yeah yeah yeah it can run okay okay like it can run some sort of local simulator algorithm it's not um it's not supposed to be like in general it's not supposed to be exactly equal to the I guess like Global simulator but with this particular property that this new proof has no overlap then the two simulations are the same let's go into a simple protocol right let's go into this

uh schnor protocol which uh is used to prove the knowledge of the discrete lock of some group elements so here you have some group elements big X in some prime Order Group groups and you want to prove the knowledge of its discrete logorithm with respect to this base G let me also just recall the protocol very quickly uh basically it consists of the first message being just a random group elements right the verifier is going to send a challenge which in the non-interactive case is derived with the uh random Oracle and then it's the prover is going to send a response which sort of like incorporates both the discrete lock and the first message and

then it's going to have some verification property that the verifier is going to check so with this protocol in mind here uh we want to show that the response is unique right the response here is just this second message G and if you look at the verification equation it follows that if everything else Remains the Same so if a is the same if x is the same and G is the same then there is only one value of Z that is possible right so in this case the unique response just holds with probability one and then we derive this prior results back in

2012 that snow is simulation extractable but now let's try to go into more complicated protocols and in fact this uh polom iops or interactive Oracle proofs this is sort of the backbone of modern snar constructions and let's see how weak unque response can be prove for such General protocols again let me recall just very quickly how these protocols work it comes from some information theoretic interactive protocols where in each round the prover will send oracles to some polinomial and the verifier is going to respond with some challenges

after all this interaction is done the verifier can Now sample some query points there's some sort of indexing here that is maybe a little bit hard to see I just wanted to convey the general ideas that you know it may happen in multiple rounds and in each round there may be multiple polinomial the verifier going to sample some query points it's going to query these oracles to get the evaluations at these points and then it's going to decide based on these evaluations this is an interactive protocols you're going to collapse this into a non-interactive proof by essentially instantiating these polom oracles with polinomial commitment

schemes so now you're going to send commitments to each of these polinomial and you're also going to send in in turn with the evaluations also an evaluation proof these Pi e valves Okay so that's what a polinomial commitment scheme does and then you're also going to apply fmir to this protocol to make it non interactive so with these uh snarks that are derived from polinomial iops in this way how are we going to show that weak unique response hold for the final Stark a prior work has shown that this weak unique response property

it would follow from basically two conditions the first is that the polinomial IOP queries they are unpredictable so for instance if the queries are just like some of these challenges then they are going to be unpredictable because the challenges are aroundand them and secondly you want the polinomial commitment schemes to have weak unique proofs of uh evaluations so I'm not going to Too Much details on these weak unique proofs it basically just says that for a fix commitments uh evaluation point and evaluation there is at most one proof that it can produce to show that this

evaluation is correct and also with some other standard properties of these PLP or pcom right and the proof idea here is basically you look at this proof here which consists of the commitments the evaluations and the evaluation proof and you look at um you consider when the two proof first diverge right if we're doing the weak unique response you need to have two proofs that diverge at some point so if it's going to diverge at one of these evaluation proofs then it means that the protocol has does not have unique proof If it diverge at one of the evaluations then it means that it breaks

evaluation binding and so on like if it diverge at one of the polinomial commitments then you basically can't do it because the queries are now unpredictable so you don't know uh how to derive the evaluations that's uh the end of it for simulation extractability this is a template that basically you can use this template to show that the existing snarks that come from polinomial iops are simulation extractable is there a relationship between weak unique response and like round by round soundness or or Notions that just come up when analyzing security of Fiat Shamir and sort of the standard

knowledge soundness setting yeah I don't know but if there is that would be very nice I mean it's interesting that like your canonical example of something that is not simulation extractable when using fat Shamir yeah involves repetition which is the canonical example of when fimir was just not secure period yeah and they feel a little bit related okay yeah yeah yeah and also the weak unique response seems Sim right cuz you have like up to a certain point the String's the same then you kind of diverge to get accepting proof and that's like exactly what R around sound tries to say you can't do right so it would be interesting to see if there's a relation there yeah yeah definitely so

let's talk about UC security um so what is UC security anyway and it basically tries to solve the following potential problems okay so when snarks are deployed in the real world they're usually deployed alongside many other protocols right and in this case it's not enough to just show security with regards to knowing many other proofs you also have to show security when you you you can see sort of the transcript of many other Protocols are executing alongside it so you need a very nice like theoretical

model that can capture composability with respect to arbitary protocols and this is exactly the goal that the UC framework uh is designed to do so it's introduced by rank conetti back in the 2000s and now it has become sort of a goal standard for cryptographic uh security because if a scheme is proven using secure then it can be composed arbitrarily with other protocols uh in this framework and still remain secure you see Security in a nutshell it says that a protocol is secure if it behaves like some ideal functionality and in the

particular case of non-interactive proofs it is this ideal functionality I call it fnic nisic just means non-interactive zero knowledge this function ality has can take in two kind of queries right one is the proof query and one is the verify query when you send in a a approv query you're going to send in the statement and the witness and you're going to get back a proof and then later on you can uh get that proof and send in a verify query and it's going to give you either accept or reject and moreover this ideal functionality it should be behave like the simplest version of a proof system

that you can imagine so it's going to look something like this you want the proof and the verify algorithm to be as simple as possible so what is the simplest thing that you can do well when you prove something you just sort of assign this statement and witness pair to some string right the string is the proof and you give it back this the string you're going to store this there's some sort of database where it remembers all of the proof that it has been given to uh that that has given and then when uh someone tries to verify a proof it's just going to look at this table for every proof is

going to extract out some witness it's going to check if this witness is is valid or not and if it's valid it returns accept if not it rejects yes this may not really matter cu conceptually but why does it have to store a table rather than like signing or encrypting the witness or something so that when it gets it back like you could imagine a version of this ideal functionality without a bunch of storage what do you mean by encrypting well like you said it like stores the witness in a table and looks it up later yeah it could just like encrypt the witness and give that out as a proof ah um so you want the proof to yeah yeah it's the sness right you want the proof to be

actually comparable to to the proof of an actual protocol and if it's a snark then you want the proof to be suct so the ideal functionality is sort of doing all the work here it's some trusted third party that uh yeah has this stateful implementation somehow it's conceptually weird though that the ideal functionality is stateful where like a proof system is not stateful right yeah yeah but I guess that's the that's the nice thing that if you can prove UC security then somehow this stateless thing is as powerful as a stateful thing and also let me just show you what UC security actually means with respect to this ideal functionality so in an actual protocol Pi there in the real world is

going to be UC secure uh like it's going to UC realize the functionality fnic in the ideal world if for every adversary it can interact arbitrarily with the peral pi and also with some ambient environments right the environment here you can think of it as a distinguisher it's trying to determine whether it lives in the real world or the ideal world so interacts with everything interacts with the protocol interacts with the adversary and it tries to figure out whether it's in the real world or Ideal World and if it cannot figure that out then it means that this protocol is emulating the ideal

functionality in the ideal world uh you need to replace the real adversary with some simulated um algorithm that you're going to Define that somehow sort of manages to um make it hard to distinguish whether you're in the real or Ideal World okay and then maybe you know UC has had a lot of extensions to handle like Global functionalities or adaptive Corruptions and so on that I'm just going to sweep under the rock for this talk uh sorry this might be a basic question but like in your diagram below uh like Zer knowledge interally like I can see that like oh the verifier only learns the bit so like it's zero knowledge in some sense uh but like

what's the intuition for knowledge sness in this diagram yeah so it's in the implementation of the ideal functionality so given every proof you have some extract algorithm that going to spit out a witness oh and rewinding is not a thing here no it's not yeah so that's actually the next slide so yeah I want to convince you why achieving UC security is difficult and in particular you've seen this other simulation extract property right does it immediately imply UC security and the answer is not always uh the reason is that you know you have this extraction

and simulation in the ucu framework it has to be straight line whereas extraction in many of current snarks they rely on rewinding the adversary and hence they're not straight lined and the same for simulation there may be something the simulator does that is just not allowed in the E framework because of this there have been prior attempts at trying to make uh to overcome these limitations and hence uh to achieve UC Security One such attempt is to encrypt the witness and send it together with the proof right so now extraction becomes simple because the extractor can just hold the secret key

and then decrypt the encrypted witness but then this loses Su synness and we want sub synness in a lot of applications secondly what you can do is use this so-called fish Ling transform which is a straight line version of fmir fmir usually you you can only establish security through rewinding but with Fishin you can actually get a straight line proof uh sorry straight line instruction but the cost to that is that you have an overhead in the proof size and in the proving time yeah um there there are a lot of straight line extractors for snarks you know that use Fiat Shamir if you can

watch the random Oracle queries yes um so what what's the issue with those is it that you there's no issue with those it's going to be on the next slide oh okay yeah but um like some some other protocols let's say like bullet proofs uh with with groups then I think the only known way is either you use the object Pro Group model or you need to use rewinding um right okay so if you establish that a snark is simulation extractable and it has a straight line extractor in the r Oracle model is it automatically UC secure um I mean you do need programming

the random Oracle for ZK is that an issue yeah that can be fixed with like adding a random salt to each of the rounds uh but yeah I think it should work but no one has written down you know a proof of this so maybe it's still a good good idea to to write it down some okay yeah like it just it seems like it it should work but it's a pain to write down so so what is really interesting to us is can we actually get UC secure snarks without any overheads and two recent Works show that indeed for certain classes of snarks you can have UC security without any overhead like the literally the original

construction is already UC secure so the first one are these so-called hash based snarks where you can observe the all the random Oracle queries and extract from that so now extraction is straight line and uh recent work by GSR and uh Jomo feny they showed that um this transformation for any hash based stars that satisfy you know uh these two soundness and zero knowledge Notions will be UC secure a second work showed that in the global generic group model so basically everyone gets access to some generic group

and can only like do group operations through queries to this generic groups then the gross 16 uh snark is also UC secure um here you also need to uh like modify the ideal functionality a bit to make sure that you allow re randomization of proofs but other than that it's it's easy secure okay and the the main idea that I I just uh discussed is that now you can make make extraction and simulation to be straight lines and hence uh the proof sort of goes through so so like in in in Breakdown if you use an error correcting code without efficient decoding the

extractor is no longer known to be straight line and would would your guess be like it's still UC secure it's just like we don't know how to show it like um yeah I yeah I don't have a good intuition on that okay yeah um are there I mean does it generally feel like like like all snarks people use like have all these strong security properties we want them to and it's just a pain to to prove it is like that's generally your sense or yeah I I don't think so like the maybe um like with this Global generic groups maybe you can show that a

lot of like group based Nars or pairing based narcs are actually straight line extractable and therefore maybe you see secure but yeah I guess it's just a lot of uh overhead in all the definitions and nobody has has done that yet like these two results are very recent like they're in the last month but we don't know like any like non-trivial interesting attacks on the UC security like of of snarks people are using today yeah yeah we don't okay so there are like other definitions of sess like I don't remember the names but like sometimes you give the advice thinging to the adversary so I was wondering like if like if there's any results on like how the UC security like as in terms of a

security definition compares to like those definitions of soundness M does that make sense yeah yeah so like soundness with auxiliary inputs yes okay uh yeah I this I I can't remember off the top of my head but there might be yeah we we can talk about this softline so that's both simulation extractability and UC security let let me end with say two open questions that I think uh is still is very valuable to answer um the first is that we've mostly talked about snarks but recently there's also been a lot of work on more than just snarks and

in particular these incrementally verifiable proofs so in this IVC setting you have a a continuous chain of computations and you want to generate proofs for each of the steps of computations what's uh what's happening now is that many of these I IVC schemes are actually deployed in applications so for example I think the the Mina blockchains what they do is they uh is uh exactly instantiate this um IVC framework so that each of the step is a States um uh of the blockchain and then you do continue updates with proofs well they're deploy nowadays but there is no sort of R proof written down anywhere

that these um IVC proofs they are resistant to Mal ability attacks um I'm also not saying here that this is a bad thing uh I I did not look into the the whole protocol in in enough detail to to see if Mal liability attacks against these proofs will be a problem for the entire protocol or not it's interesting in this setting is that now there are some sort of unavoidable attacks you may call it attacks that may happen right so what you can do is you may get some proof somewhere that um that is valid and then you can just

continue the chain of computations right so already there is some um modification of the definition that is necessary in order to preserve what is the intuitive security notion and also uh another thing that needs new technical ingredients is that these IVC schemes they're uh usually built from a combination of two different Primitives right you have both the non-interactive arguments so this is back to this knar case as before but they also uh combine it with an accumulation or a folding scheme so those of you who saw Abram talk I've heard all about folding schemes and how

awesome they are and they are these two Primitives are combined together in an IVC scheme and when they're combined together what sort of extra things that you need to show in order to to to prove that the entire IVC construction is non modable the second question is what I mentioned before is that for non ZK Nars you just want nonm ability right but somehow in all of this talk I just assume that the stock is already ZK and then I prove a stronger property called simulation extractability but we really just want non-ability in some

applications like some applications such as these so-called ZK rups they're not ZK um they just want some synness so can we just directly prove nonability for such NS like for for jol for instance can we show that jolt is non modable here I think maybe I haven't uh Del too much in this question but at least on a surface level uh it seems that you do need some new technical ideas because the this these uh techniques for proving simulation extractability it relies a lot on having a simulator and so without simulator how do you set up the definitions how do you make sure that

you know the technical properties they all go through and so on so forth so you're saying the proofs you showed so far would not go through if the if the simulator was not a Sim simulator but but an or but an oracle that I can just send X to and get back a proof yeah yeah where would that fail intuitively like where would the proofs not go through ah so it's in so if there's no simulator right so one def potential definition is the adversary send some proof there's some like unbounded simulator that tries to figure out if there's a witness if there is then gener a proof right what goes wrong in that definition is that now when you try to

reduce to knowledge soundness the knowledge soundness adversary cannnot emulate this unbounded simulator right just just one particular way that you that that does not go through there may be other ways so in this talk I hope I have convinced you that similar extractability and U6 security are very important notion for starts it rules out these meability attacks which can be very devastating in practice and it also for UC specifically it also guarantees security when you compose uh the snark with arbitrary protocols so you really get like peace of mind when you deploy these snarks and in terms of future directions I've

showed you sort of two uh open questions there so if you're interested uh please talk to me I also like to work on these questions and a somewhat further Target might be you know how we formally verify these simmax or UC security proofs and how much overhead does that add to say the existing formal verification efforts that are on ongoing wasn't there a result that showed the Nova the IVC scheme is actually is malleable until you apply like a final snark at the very end of the IVC yeah yeah so can you hope to show then that these IVC schemes are uh simulation extractable or UC secure

uh right I mean it's probably going to come down to like IVC with these properties will satisfy simx and maybe Nova or whatever Nova version that was uh do not satisfy that notion do you have a sense of like if it's hope or not to have UC security if you only have rewinding extraction or like are there examples of like let's say you have a snark that was rewindable like you extraction through rewinding but someone else later showed it was UC secure like kind of separately I I don't know of any UC results where extraction is rewinding so it seems like still an open question to

me yeah what you can do is like maybe you have some components that is that must use rewinding but then you like add add in some extra small components that is straight line extractable or something yeah but still you need straight line extraction somewhere and I haven't seen that that barrier being broken yet yeah