How to Prove False Statements: Practical Attacks on Fiat-Shamir

Transcript

So, I'm excited to introduce Ron Rothblum, who's an associate professor at Techneon and uh head of cryptography at Succinct, and he's going to tell us about some uh exciting and slightly concerning uh new attacks on deployed proof systems. Go ahead, Ryan. >> Thanks, Justin. Uh great to be back here. Um I'm usually in the business of uh proving security uh but this talk is going to be about breaking security for a change. So hopefully it be uh interesting. So this is a joint work with wonderful collaborators Dimmitri uh Kovtovich and Lavukunov. So let's uh get right into it and I'll try to explain what these things uh mean. So this talk is about the Fiat Shamir transform. Fat

Shamir transformed is named after this beautiful paper by Amos Fiat and Adi Shamir uh from all the way back in 1986 even though nowadays the way we view it is I think we've extended it quite a bit from what they originally envisioned and in a nutshell especially the way that it's interpreted nowadays is that the fameir transform is just this amazing technique to take uh or transform interactive protocols and make them non-interactive which is almost by magic and it's really a critical component in most not all but post uh snar construction. So it's really it has become uh extremely important in practice. The original goal was about was a little bit different. Let's sort of focus on the modern interpretation of of fameir. So to give context and kind of like uh see that we're all on the

same page. Our starting point is this notion of an interactive argument system. So we have a prover and a verifier. The prover is trying to convince the verifier that a statement x is true. What does that mean? So we have a fixed uh say circuit or computation that we care about C. And what we want to show is that there exists some witness w so that c of xw is equal to y. So there's some uh sort of nondeterministic computation and we want to verify that it's correct. The verifier knows x the provers x and the witness. Both of them know the circuit C. They interact back and forth and in the verifier should be convinced. What does that mean? So if the statement is true, the verifier should accept. if the statement is false, no matter what a cheating prover can do within a

reasonable amount of time um with high probability our verifier is going to reject. So that's sort of our setting in uh in the interactive world. Oh, and something that's going to come up uh in the talk is we're going to be focusing on public coin protocols, which means that the verifier messages are just random coin tosses. So they're not sort of like intelligent challenges, just random coins. And you know luckily enough almost all the protocols that we actually care about have this form and it's going to be important later on. So that's public coin. Cool. So that's an interactive protocol. And in practice we you know we kind of are okay nice to have an interactive protocol but would it be even nicer to have a non-interactive one? And it's not just about you know uh saving you know less

rounds and so on. um nonattractive protocols have the distinctive feature that you can post them somewhere and anyone can come along and verify for example on a blockchain. Okay, so it's uh really uh an extremely important feature. So what does fmeir again take an interactive protocol make it non-interactive and do it in a very generic way. So how does it work? Where's what's the magic? Well, we start off with our interactive protocol. We have P talking to V. I'll denote the prover messages by alpha and the verifier uh challenges which we recall are just random coins by beta and we transform it as follows. So we have a new proof system PFS VFS. To do it we're going to be using a hash function H. And I assume you are probably all familiar

with this. So so it won't be uh too slow. But the way it works is as follows. So you start emulating the proof system, right? So the prover can you know uh generate and send over alpha 1. But now it can no longer wait to get the response beta 1. So rather than doing that, we still want it to be sort of unpredictable. So we'll compute beta 1 by hashing kind of everything we know which would be like x and y and especially alpha 1 to derive beta 1. Now that we know beta 1, you know, the verifiers are going to do it later on on on her side as well. But as a prover, we can keep going, right? So we can now generate alpha 2, send that in the same message, compute beta 2, and so on and so forth. By sort of replacing the

verifier by a hash function, we can compute all the verifier challenges. So the transformation to those who haven't seen it before is a clear and also to those who have seen it before. Right? So this is the suggested transformation. One thing I want to really uh emphasize is that you know while it is very very simple as described it is sort of notorious for implementation bugs. So this is a list including one very recently I think on the Salana blockchain which I think was uh made made some news and the reason is sort of while it's very easy to describe this way in practice you have a very complex protocol and you need to make sure that you're really hashing everything possible that uh the verifier knows um or or sorry that that that that yeah

that you can um and it's very easy to miss. So there have been a lot of implementation bugs. This talk is going to be not about an implementation bug but really about using fietir sort of as you're supposed to. Okay. Uh we can talk more about this. >> So so the implementation bugs are usually leaving out some of either x or the alphas. >> Yeah. So the the classical implementation bug is uh forgetting to include x which means that a cheating prover could like based on now that it knows beta 1 it can choose a good x for which beta 1 is easy. So kind of anything that the prover can potentially control you have to include in the hash and people know this by by now but they still you know these mistakes come up all over. I should say that there is some uh nice work by mikuel or I think

on trying to standardize fetch and have like libraries so people make less mistakes. Cool. Cool. So we have this Famir transform. It's been extremely influential and incredibly important um in cryptography. And to highlight some reasons, first of all, it's incredibly powerful for just because um interactive protocols are amazingly powerful. Kind of like surprisingly how how much interaction buys us. So stuff like uh you know some GKR, the Fry protocol, a lot of the protocols that we really love and have designed are naturally interactive and they really get a lot get a lot from this interaction. and all of a sudden we have this you know best of both worlds that we can enjoy you know all this these benefits of interaction without actually interacting so it's really really powerful it is

highly practical and really like deployed everywhere um and a large reason for that is that it's very small overhead right all you need to do is like there's a hash function very lightweight no public key crypto and so on um so so it's very lightweight so people like it a lot and you can get you know this goes back to being powerful you can get a lot of mileage out of it. So starting off you know um in the beginning with efficient signatures which was designed for going on in theory land to things like uh CS proofs and nowadays snark starks all that stuff. So so we kind of really like the feature transform. The question that we want to sort of like focus on in this talk is is it sound? So first and foremost let's start with intuition. Why why would you expect it to be sound?

Well, we have the interactive protocol, which we're assuming is sound. And in that what makes the interactive protocol sound is when the prover generates a message. He doesn't know what the verifier's next coin toss is going to be. And that is crucial to to the soundest argument in the interactive land. And it seems that when you do hashing, you have something similar, right? You from the prover from a cheating prover's perspective, until he decides what his message is, he doesn't know what the hash of this message is going to be. sort of makes sense, right? And and therefore it seems that it really uh mimics the uh the interactive setting. So that's sort of the intuition. Um but as cryptographer cryptographers, we don't love just

settling for intuition. And indeed, for a long time now, we've had this analysis that we very strongly rely on, which is what known as what's known as the random oracle analysis, which says, you know, our hash functions are amazing. They're really, really good. They're so good that they are, you know, they're so nonsensical have have have no structure that we may as well just treat them as totally random functions. So that is sort of like a leap of fa of faith that is made or or a modeling assumption. And if you analyze your hash function as a fully random function then it's been shown that the phmir works. You have to be a little bit careful but you can make it so that it works. And now with with this in mind the common interpretation has been you know our hash functions are so good we have security when the hash

function is really good. So if we have an attack on fietir it has to be because the hash function is not as good as a random oracle. It has some defect and we should replace it with a different hash function. So far so good. So that has been sort of the the common wisdom uh for a while and it's been the common wisdom despite the following amazing paper called the random oracle methodology revisited which is from a good 20 years ago. It's by Keneti Goldrich and Halevi who showed that there actually exist specific u cryptographic schemes that are secure when like using the random oracle model.

So they they're in the random oracle model. But in these schemes, if you instantiate the random oracle, no matter in what way, security is broken. So it's really it's not uh the fault of the hash function. So you could use, you know, no matter what hash function you use here, it's broken. Yes. >> So specifically, what cryptography primitive did this previous paper? >> Um I think they they they did a bunch of different things. I don't remember off the top of my head. I think they had encryption, maybe signatures. um they couldn't quite do uh fat which is what I'm coming >> are any of the attacks actually relevant in practice in this paper >> good so so this has been known for a while now I might ask how are people still relying on the random oracle uh

model and so on given this attack and the the point really is that the schemes that were constructed here were highly contrived so they were it's not maybe clear what I mean by contrived but it is clear that they were specifically designed in order to fail okay it's very clear when you look at they have a weird component that you would not expect to see that was intentionally put there. Um so it doesn't ruin security when you're in the random moral model but it ruins security when we instantiate it. Okay. And that is why I think um the common wisdom remained and people were not really worried about the random oracle model that answer the question. Yeah.

So a couple of years after that, this is like journal versions that's why the years are mixed up. But >> so so that was like a trapoor trick kind of thing in there. Okay. >> In a sense, so there was an intentional trap door if you like meant in order to violate security when you instantiate the random oracle. A couple years after that, the years are are just like journal versions. So Barack and really like Lvaser and Kalai struck the point. Uh so they showed an example of an interactive protocol in the random oracle model. So sorry, sorry, it's an interactive protocol. It's secure. If you apply fetch to it in the random oracle model by the previous result, everything is fine. But if you instantiate the random oracle, it's broken.

Okay, so this is showing that you know famir is insecure. You might start wondering okay are we in trouble? But again here the interactive protocol that you start off with was contrived. And throughout this talk when I say contrived I mean it is very clear that it was intentionally designed to fail. So these results they're they're like constructive like it's not >> Yeah. It's an explicit protocol and we're going to see something along this uh very soon. >> Yeah. >> So basically there's an explicit attack given. >> Yes. So it's an explicit protocol and a fully explicit attack. More recently uh in joint work with my student Leon Bonman and Bertusk uh Justin Homegrren and Fermyim Ma we showed that actually if you look specifically at the way that a lot of like uh basically how hashbased

snarks are constructed namely um take something like a PCP or IOP and compile with a vector commitment. We showed that even for that type of construction we have an attack which seems more concerning and I think it is. However, still we had a contract component. So we had sort of two results here. one had a contrived IOP. So the underlying I don't if people are familiar but uh a key underlying component of snarks is something called uh an IOP. We had a specific IOP for which you know the general methodology fails. That was one result and the other result had a specific uh hash function for a Merkel tree or vector commitment that would make it fail. But again we had a contrived component. So I don't think people were particularly worried about these attacks.

So the point here was just at least the high level structure matched the practical construction. >> Yes. Yes. So so like it was getting more and more closer to actual protocols and the contrived component was becoming smaller. >> Yeah. And really the the point of uh of this new work is that we show uh something that I would say is not contrived because it's a protocol that people have um you know written a bunch of papers doing it and there are companies that are running it um and for which you know they these papers show that it's secure interactively but we show an attack when you compile using feature mirror and by an attack I mean that we can actually convince it's fully explicit to to Ela's question we can convince the verifier to accept a statement that is blatantly

false and we're going to see it. The order of quantifiers here is a little bit nuanced. So, so we're going to uh I'll write a more or less formal theorem statement soon. So, before showing you our actual attack, I want to start off with a motivating example which is sort of in the flavor of the previous contrived protocols just to give a sense of like what might go wrong and I think it's skewed. So, let's do that. So, uh it's a protocol. We have a prover and a verifier. Um and you know, you're trying to prove something. I don't know. C of X is equal to Y. Not super important. And the protocol is going to look as follows. So the prover sends to the verifier a message M. Okay, so far so good. The verifier tosses a bunch of random coins. Think of lambda as a

security parameter. So maybe 128 bits. Okay, uh random vector. Send that over to the prover. So far, great protocols. All protocols look like this. Now comes the weird part. So here's what the verifier is going to do. It's weird. verifier takes the message m interprets it as code in I don't know rust do you like rust whatever you like C++ C++ to interpret it as a C++ program and starts running it and it runs it on a on a specific input so it feeds as an input to the program the input x the claimed output y and the code of m itself why does it do that because I wanted to

weird okay but does it does this sort of like thing remind anyone of anything from undergrad diagonalization right you're running the program on itself as input so it's weird let's see why we're doing that so not only so so so we do this thing m so think of like this m of m kind of thing and we check whether the result is equal to r now what's the probability of that very very very small right because m was determined before r was chosen so this on the right hand side is a fixed string And we're asking what is the probability that a fixed string is equal to a random string. So why are we doing this? We'll see. But we're doing this. So if it happens to be this very unlikely event

happens, we immediately accept. And if not, then you run your other proof system. You're on Jolt, which is secure. So that's the protocol. And first I want to say, yeah, this is Jolt. I want to claim that this is a secure interactive protocol. And the reason we already sort of sketched right the probability of this quality being true is is negligible. It's exponentially small. So we can more or less ignore it and we're just running some other protocol and jolt is secure. So everyone is happy. Right? So as an interactive protocol it's secure. Let's think what happens when you apply fetch. So what did fameir tell us to do? So we're using some hash function h and rather than choosing r at random we are computing r by hashing whatever we know which in our case is uh

x and y and m. Okay so r is computed as a hash of x y and m. And now for a prover to cheat in this protocol, what it needs to do is to find the message m so that you know r which is just this thing is equal to the right hand side thing which is this thing. Can anyone think of a message m that will make this equation pass? >> H >> h right. So if you send h it passes you can make the verifier accept any statement with probability one.

So it's fully explicit to question fully and you can convince um you know any statement that you want of probability one. Okay. So this protocol is really contrived right you stare at this and you don't expect to be running you know like a user specified message treating it as a program running it on itself as an input. No protocol would ever do something like this, right?

So it turns out that our protocols are now sufficiently general purpose that in some sense you can do this. Okay? And that's what I want to show you in that attack today. So so let's jump right into it and show that attack. So to describe the protocol that we're attacking, I need to give you a little bit of background. So basically two things. one is what is a PCS or polinomial commitment scheme and the second thing is uh the GQR protocol or just like a little bit of information that you need about this protocol. So first of all what is a PCS or polinomial commitment scheme. So first of all it's a really important uh component in most uh snark constructions. So it's a way to commit to a very large polinomial and you have different variants whether you know it's univariate multi multilinear and so on

but you want to commit to a very large polinomial in a su very succinct way so that later on you can prove statements like p of x is equal to y so I commit to a very large polinomial p using a very short hash but later on I can prove to you evaluations I want uh you know one of the luxuries of breaking security is you don't have to sort of define security of the internal things because you're breaking the overall thing so I I won't define formally what it means but intuitively it makes sense. Cool. And specifically for today we're going to be focusing on polinomial commitment schemes for multilinear polinomials um over a finite field where you know sufficiently large finite field. So that's one component we need.

The second component is the GKR protocol by uh Guy and Shafi should say Shafien Ya and Guy um from almost 20 years ago. So the GCAR protocol is a statistically sound interactive protocol for proving correctness of a bounded depth arithmetic computation. So think of you know I want to prove that C of X is equal to Y where C is some bounded depth arithmetic circuit over the field. Something worth uh emphasizing because we'll change it in a bit that this really deals with a deterministic computation. In contrast to what we were saying before we want to prove that there exists witness blah blah blah here it's fully deterministic. There's a fixed circuit C. there's an input X that prover and verifier know and we're proving correctness. You know, CFX is

equal to Y. So, I want to show you how how the protocol works. We won't need like too much details, but we'll need a little bit. So, remember we said we're dealing with an arithmetic circuit. I drew it here from input layer at the bottom going up. And the the circuit has, you know, addition and multiplication gates. And the way that you compute is you put in an input and you feed it into gates. You evaluate the gate and you uh move on and on and then draw all the edges. you go you should think of it as a layered circuit and you go layer by layer until eventually you evaluate the output. Okay, so this is just an evaluation of an arithmetic circuit. And now we want, you know, let's say I'm an honest guy, of course, you know, I am. Um, so despite breaking

some some some stuff today, um, we when we feed in an input X, that determines the output Y of the circuit. How does the GR protocol work? Well, I'm coming along and telling you, hey guys, the output, you know, this is X. If you evaluate the circuit, the output is Y. And the goal of the protocol is to avoid you having to re-evaluate the circuit. So we want a more efficient uh procedure. So the first thing you do as verifiers is to choose so we're going to look at uh a particular encoding of the evaluation of the circuit. Right? So when we when we evaluated the circuit for every layer we got the values that you know we got during the evaluation and for every layer separately I'm going to look at an encoding of these values using a specific error correcting code

which is the multi-linear extension. In other words I'm interpolating these values as a multi-linear polinomial. the specifics don't matter that much for for the talk. At one point they will, but it's not going to be huge. Okay, so that's what I mean with the yellow bars here. So these are there are the encodings of the individual layers. So I come along and tell you, you know, the output layer is supposed to be an encoding of this string Y. What you're going to do as a verifier, first thing is choose a random point in this encoding um and compute the the the value that is supposed to be there. So the entire encoding is very large but you as a verifier if you're only interested in one specific point you can do this very efficiently. Why do you do this? Because intuitively intuitively if I was lying

if the output of the circuit was not y it was some other y prime I take these two strings and I evaluated them at random point because of sort of this error correcting property with good probability the results should be uh different. Okay. So now I've managed to reduce the claim about the entire output layer to a claim about a single point in the in this topmost layer of this in the encoding of the topmost layer. So far make sense? Cool. So that is uh the main part that we'll care about. But you know just to not leave you hanging let's see how the protocol works from from here on. So the next thing that that happens is some little interactive protocol that manages to reduce a claim about the output layer, a single point in the output layer to a single point about one

layer below that. So there's a specific interactive reduction that manages to to do that. It relies on the subject protocol, but the specifics won't matter for us so much. So I managed to go from a claim about the red dot here to claim about the red dot there. But then I could do this again and get a claim over here and a claim over there and eventually a claim over there after I do this for these steps and the claim that I get about the input layer I as a verifier know the entire input so I can verify it myself. Okay. So that is a structure you know the the original GKR protocol. Um the way that GKR is used nowadays is a little bit different than how it was originally proposed. So I want to show you how how we extend GKR in a sense. So I was as I was saying

before GKR is you know was designed for deterministic computations but nowadays the way that it is used is also to handle nondeterministic computations. So I want to prove to you not only that C of X is equal to Y but rather that I know some secret maybe W so that C of XW is equal to Y. And the way I will do this is by combining GKR with a multilinear PCS. And I want to show you how to do it. So here's the idea. So we again we have our prover and verifier. First thing that's going to happen is for us to sort of agree on what circuit we're using. So maybe first of all the verifier will specify parameterization of the PCS. Okay. So in case our PCS usually will involve some sort of

parameterization. So the verifier specifies it. And now the verifier uh sorry the prover tells the verifier what circuit are we going to be dealing with today. Now you might think in in practice the verifier is the one choosing the circuit for which we're proving stuff. But really we want you know especially with with soundness in mind we want things to be secure even against um maybe an adversarily chosen circuit. So I think of it as the prover choosing the circuit. Cool. So the the verifier the prover has chosen the circuit. If I like I I want my verifier eventually to be sublinear in the circuit. So what will happen now and this I think of it as a pre-processing step is that I'll only save just a little bit of information about the

circuit C which will be enough for my my proof system. So rather than saving the entire circuit C which is very large the verifier at this point just saves a small digest of C which I will denote by bracket C. So think of it as some sort of hash of the circuit of the circuit description. Okay. And it's very short much shorter than the circuit. So this notice that this doesn't depend on the actual input X or the witness w. So we've done that and now we want to start the actual proving. So now the prover gets the input statement X and the witness W and the verifier gets X. What do we do? Well, first of all the you know I as an honest prover will evaluate the circuit. I get the result Y and that's my claim. My claim is that the output of the circuit is Y. And I'll

also compute a PCS hash of W. Right? So I take W I view it as sort of the the guts of a multi-linear polinomial and I commit to it so that later I can prove make evaluation proofs about W. What do I send to the verifier? I send the input claim X. I send the claimed output which is Y and I send this alpha which is the PCS hash of W. It's very short just a hash of the witness. So I send this over to uh to the verifier. And at this point I want to think of you know given X and W there was a circuit that I want to evaluate and I want to start running GKR with respect to that circuit. So let's recall how the protocol worked. We had the circuit we evaluated it and now we sort of first thing that we did you

remember what that was to look at the output layer and compute the multilinear extension at a random point. Right? So that's what we're going to do. So verifier chooses a random point in the multilinear extension which I'm denoting here by yhat of y. Right? So whenever I put a hat, it sort of like interpolate this data as a multi-linear polinomial and evaluate it at R. I send R back to the prover and now the prover and verifier start engaging in the GKR protocol. So reducing it layer by layer until eventually we get a claim about the input, right? But notice that uh the input here is not just X which we have, it's both X and W. So what we're getting in GR eventually is a claim about the multi-linear extension about the concatenation if you will if you like of

X and W. Turns out that it's easy to uh break that down into separate claims about the multi-linear extension of X and the multilar extension of W. So the multilinear extension of X, we have X as a verifier. We can compute it by ourselves. But we don't have W, right? So how do we compute the multi-linear evaluation of W which we got at the bottom? Well, conveniently enough, the prover has already committed to a PCS of W in the beginning that was alpha, right? So, what we need now is just an evaluation claim about this PCS.

Does this make sense so far? >> So, this is where the diagonalization comes in like >> no diagonalization so far. This is you know an honest you know this is a protocol that people have proposed um you know I don't know when five more than six years ago and people are using um there's a startup company that or at least one that that uses it this is a nice protocol that people like >> I I meant the component where you run a >> what is the component that we're going to attack you're asking >> no eventually you want to convince us that GKR has some component that runs a program on itself no or >> um you can force it to do something like that. Um, it's not entirely clear where yet in this picture, but I'll show you

soon. So, just notation wise, I'll denote this protocol by like pi for protocol. And notice that it depends on the PCS that I use, which could be something like Fry or whatever you like, and on the depth of the circuit because GKR you have these dep. So, it depends on the depth of the circuit. Cool. So, that's our our nice protocol that we're going to attack. And notice what happens when we apply fatir to this protocol. So first of all in the beginning I will need to tell you what future mirror hash function I'm planning to use that is this uh red h and then you know we proceed in the protocol as before. So I as an honest prover evaluate the circuit. I compute the pcs hash of the witness alpha send them over to the verifier.

The next thing in the protocol that happens on the verifier side. You remember what it is? It was choosing a random point in the multilinear extension of the output layer of the circuit. >> But now we're doing fmeir. We're not choosing stuff at random anymore, right? What do we do instead? So instead of choosing R at random, we hash. What do we hash? Everything we know. We today we're hysterical. We're not going to have any implementation bugs. Everything we know, we hash. So the description of the circuit C, X, and Y, and the alpha that we got, we hash everything and we derive R in this way. Okay. Then we start uh and the prover also does this similarly. Then we start running the GKR protocol. Notice that GKR was itself an interactive protocol. So it's actually

familiar of GKR in this step. Um so all the arrows are just pointing towards the verifier. And then at the end uh of this Femir GKR, we're still going to get a claim about the multi linear extension of W. So we'll run the PCS evaluation proof which again is going to be familiar and we're doing a proper famil with all you know everything we know being hashed out. Right? So that's a protocol that we get and I'll denote this by just fs subh of the previous protocol right so what happened is just we replaced all randomness whenever we had with evaluations of of h and what we would like for this protocol to be and we'll show that it isn't is adaptively sound so what do I mean by

that what does adaptive soundness mean here right so the first thing that happened is that the verifier chose the pcs parameterization and the hash function h and then the prover spec specified a circuit C. In order to violate soundness, I would need as a cheating prover to find a circuit C, an input X, an output Y, and the proof pi. So that two things happen. First of all, this is a false statement in the sense that this circuit on input X will never ever ever output Y. So if I'm claiming that, you know, my circuit C there exists some witness W so that I'm given input X will output Y, this statement is false. First of all, second of all, despite it being false, I can make my

verifier accept. So if I give, you know, CX uh Y and this proof PI which consists of the entire GKR thing and the PCS evaluation, you know, the verifier will accept. If I can do that, I've broken adaptive soundness. Soundness here is adaptive because I'm I'm allowing my choices to depend on the PCS and hash function H. Okay, so that that's how we denoted the protocol. As mentioned this protocol has been you know um widely I would say explored in in in practice um in a sequence of works a bunch of academic papers were were uh we're studying it and and improving it and also deployed in practice by uh a protocol called uh expander by a company

called polyhedra. So this is their know from their thing and this is from their GitHub uh a fix to the attack that that we that we showed and we'll describe later on what is the fix. Let's first understand that attack and then we can describe the fix. Okay. So but this is a very much a real world attack. >> I mean you you do still allow yourself that the circuit see your input X might be contrived in some way even if the protocol is not. >> So we're going to discuss that. I mean I um I allow it but we'll see whether or not that is actually true. But for the moment, let's say we're we're happy with that.

Okay. So I uh I want to state what the the result a little bit more precisely is. So the main result is the following. So tell me what PCS you're using, whatever it is, and tell me, you know, what depth D GR you're doing. As long as the depth is sufficiently large, then we show that the protocol is not adaptively sound. What does this mean? You know, just a contraositive of what we said before. Given the PCS parameterization and the feature hash function, we can generate a fully explicit circuit C star. We're going to see it today and output YSAR. So that C star never outputs YSAR and yet we are able to convince the verifier that it does. Okay. So the verifier in the protocol will say oh yeah sure C star

does output Y star sometimes. >> So sorry you're saying the circuit depth is going to be a function of the >> complexity of the hash function of PCS. So that's where the adaptive >> Yes. Okay. And in particular going to Tim's question something that you know naturally comes up when you see this uh statement is this our circuit C star contrived and I would actually say that it isn't and we we'll see in a little bit. At first glance it might look but I would argue that it isn't. So we'll try to make that argument. So that's the first attack. Second attack that we do is an extension of the first attack. I call it the backdoor attack. So in the previous attack we're saying you know there's a specific circuit that we're trying to target. But let's say you know there's a circuit that you guys are

interested in proving. In the second attack I'm saying the following. You know actually designing a circuit is hard. So instead of designing a circuit you're going to go to some like you were going to outsource it and go to some company and they're going to give you a circuit implementation. What we're saying in this uh second statement is that you can take any circuit and change it into a different circuit which computes the exact same function. So for each and every input in the world, my circuit is going to output the exact same output as your uh circuit. But for my version of the circuit, I can entirely break security.

Okay. So the uh security here does not depend only on the function being proved but the actual implementation of the circuit which is I think quite concerning. Yeah, especially you know to audit a complex circuit. Um you know I described it to someone who does that. He was he was very happy because it would mean a lot of work for him. Third result uh we have a version of a non-adaptive attack. I think I'm not doing great on time so maybe I'll I'll skip that and I want to just like directly show you the main result which is an explicit circuit for which we can break security. Okay. So not not even high level idea just a plan. Our plan is to construct an explicit circuit C star.

We're going to be targeting a very specific output string which is just you know the vector of two elements 0 0. It's a very specific vector which is convenient and um we're going to build it. So, you know, we're going to claim that our circuit C star sometimes output Y star even though this uh never ever happens and it's an adaptive attack as sort of Tim was pointing out um my circuit C star can depend on the choice of PCS and hash and the key idea really and this is like the key idea we want our circuit internally to try to predict what is the fetcher value that's going to be produced okay so let's try to do something like that so again I'm describing a circuit C star it actually

won't need any input X. So we're just asking does this C star is does there is any witness W that will make it output the 00 string. Okay so let's try to build it. So I have a circuit C star just as gets an input a witness W and it's going to do some stuff but eventually I want to predict the fmy randomness and specifically remember this point R in the multi-layer extension of the output that was being computed I want to try to predict that R. How was that R computed? it was hashing the circuit description and Ystar which is the claimed output and alpha which is was the PCS uh commitment of the witness. Okay, so I want to do something like that.

And when I try to do something like that, I run into a sort of a big problem which is circularity, right? In order to describe my circuit C star in its description, I need to know its own digest. So how do I do this, right? I need like only after I finalize my circuit do I know its digest and only then can I feed it here. So it seemed like a problem. So the way we get around this problem is that rather than you know hard- coding the circuit digest C star inside the circuit, we're going to sort of be expecting to get it as part of our witness.

Okay, so let's see what I mean. So this is the actual circuit we're going to use for our attack C star. So as before, it gets the witness W. The key point is that we're going to interpret W as a circuit digest and we're sort of going to plan things but expecting it to be our own digest. But you know we're innocent. We don't know what it is. But so we're just treating it as any old circuit digest even though the attack is geared toward it being our own digest. But for the moment you know we want to define the circuit and just saying look at W and interpret it as some circuit digest. Now compute the PCS hash based on on W. So compute alpha as you're supposed to. And now we can sort

of try to predict the randomist R. I'll denote it here by gamma to distinguish. So what are we hashing? We were supposed to hash our own circuit digest. We're we're expecting the subsai to be that. We fit in y star which again was just a zero. And we feed in alpha which we've just computed. And now we get gamma. We're thinking of gamma as being our sort of guess as to the randomness that's going to be selected. And now I do something a bit mysterious which we'll understand in a second. I output two field elements gamma and gamma minus one. Why that that part is a little bit of a mystery for the moment. We'll see in a second.

But this is the circuit for which we're going to be proving a false statement. Is it clear that it's like well defined no circularity right? It gets W does this. So first claim that I want to make is that this circuit is never ever ever ever ever no matter what W you feed into it never is it going to output 0 0. You see why? So it's always outputting consecutive integers. So it's not going to output 0 0. This is the circuit. never does that. But I'm going to produce a proof that convinces my verifier to believe that it does output 00 even though it doesn't. So we've established claim one. Let's try to prove claim two. So I wanted to tell you

what the prover does, right? So let's rethink uh in our mind what the protocol looks like. So first thing that the that happens in the protocol is that um the verifier spec specifies the PCS and the fetch hash function H. And now the prover needs to select what circuit it's using. Well, it's going to be using the C star that I just constructed. That's the circuit that we're going to attack. And then the actual protocol starts, right? So what do we do in the in the protocol? We need to send So if there were an input X, we would need to send it. We don't, so we don't need to. We need to send our claimed output, which is Y star. So it just be this 0. And we need to send uh PCS hash of the witness.

So we're just going to do PCS of the digest of C star. At this point when I describe the prover I fix the circuit C star I know what the digest is kind of like pulled the digest outside of C star itself. Okay. Um so and you know the prover still needs to generate a bunch of stuff for the GR and so on. But let's pause here for a second because this is where something interesting is going to happen. Cool. So the actual output of the circuit is gamma gamma minus one where we saw how gamma was computed. It was specified a couple of slides ago, right? And now I want to ask you uh a question. It doesn't depend so much about what gamma itself is for the moment. But what is the multi-linear

extension of the string gamma comma gamma minus one at the point r? And because this might be not so clear, I want to spell it out a bit a bit more. So we're looking at um sort of a function that at zero outputs gamma at one outputs gamma minus one and you know it's multilinear but it's only a single variable function. So it's again a single variable function. It's a linear function because multilinear with one variable is just linear. At zero it outputs gamma. At one it outputs gamma minus one. Any guesses what it will output at two?

Gammaus 2. And at three gammaus 3. And at r gamma - r. Right? But notice just by construction we when we built our our uh circuit C star gamma was computed this way but R by FIA how do you compute R you hash the stuff you saw before guess what it was designed to be exactly the same so what this means so we have our like the actual output of the circuit is not 0 0 but if you evaluate its multi-linear extension at the point R you're going to see a zero now let's think about the fake output right I'm claiming to you that the circuit output is 0 0 even though that's false and now I want to ask ask you an easier question. What is the multi-linear extension of the function that is zero at zero and zero at one? I'm asking you

what is its value at two? It's a linear function >> at zero and at three at zero and at r at zero. Right? So the multi-linear extension of both the fake output and the real output is zero is sorry equal to one another at the point R it's at zero. Okay. Okay, so going back, we were saying before that if you take the multilinear extension of two different outputs because of the distance of the multilinear extension at a random point, they should disagree. Well, guess what? Our point is no longer random and they happen to agree or we build it up to agree, right? So what happened really is we started off with a false claim that the circuit is outputting 0 0. But when you

know using feature to choose the random point R we set it up so even though the claim about the output of the circuit being 0 0 was false the claim about the output of this the the extension of the output of the circuit at the point R being zero that claim is true and so we managed to move from a false claim to a true claim and once the claim is true we can just run the honest prover strategy and everyone is happy. So we're actually for almost the entire protocol we're just running the honest prover strategy. Okay. So maybe to summarize what the attack looks like. So we have P star which is the attacking circuit. It gets the PCS description and H. It specifies the circuit C star or nasty circuit C star verifier saves the digest. Then

online our claim is that the circuit outputs 0 and we send a PCS encoding. This should be of C star sorry the digest of C star. Now in frame mirror we fix R to be this sequence but now the claim has become true. So the claim that the circuit output there extend at the point R is equal to zero. This claim is true. So from here on just run GKR honestly and run the PCS evaluation honestly and the verifier accepts probability one. So now it goes back to Tim's question that uh occurs quite frequently. Is the circuit C star that we built contrived? And at first glance, you might say it definitely looks weird.

It's doing something like evaluating the fatir hash function inside. It's doing a PCS evaluation. No, that's weird. So, I want to argue that this is actually not weird in the sense that circuits that we actually care about a lot tend to do these things. And I'll try to give two examples. First of all, something that comes up uh very frequently in these applications is that I give you a particular hash. And I'm claiming that this is a hash of a huge database, say a blockchain or something that satisfies some properties. So proving stuff for your circuit to depend internally about the hash is very frequent. I would say that that is the typical application even. So that's on one side. The other side which is I think even to to in a sense even more

concerning something that uh people myself included I guess uh tend to do is to do recursive composition in which you use um the proof system to prove the verification process of the proof system itself. And this uh can be very uh help a lot in different aspects of efficiency. When you do this you know by definition your prover is proving stuff about the future mirror hash function. So I would say um for the circuit to include the future mirror hash function happens uh all the time. The PCS is maybe not as frequent but then again PCS's are often implemented using hash functions. So I would say that I would make the argument that the C star is not not at all contrived and if you do think

it's contrived you know can have different opinions but we do have extensions of the result that do handle sort of like more general setting. in particular I can take any circuit and know insert a back door into it so that I can attack it. So far it's been bad news and I think you know to an extent uh that's going to be the message of today. Uh but there is a question about like you know can we make stuff sound. So one thing I want to point out is that there's been uh really a rich line of work that I've also been uh quite involved in of trying to establish fetch security based on standard cryptographic assumptions in you know uh the plane model or at least with a common random string based on standard assumptions like lwe ddh and so on and I think it's

been we've made a lot of progress there so two challenges here first uh even before practicality all the results that we have so far are only able to deal with a very limited amount of nondeterminism. So we don't know how to prove like general NP statements using uh you know forget about uh practicality even theoretically we don't know how to do it like so in theory land doing snarks for NP under standard assumptions is an open problem uh you know probably number one open problem in in in theory land. >> So so partial is parameterized by the witness length or what does that mean?

uh no so so for till like a few years ago it would would have been like no nondeterminism nowadays we're able to prove um sort of conjunctions of NP statements so we proving that um multiple NP statements are all correct and the length of the proof will be proportional to one of them or a bit more so you're proving kp statements and the proof size is only like uh say one or so of them yeah >> so so there are some works that show like with some special soundness property He like you you can remove the fashion and those don't those papers don't work for >> I'm not sure what line of work you're uh referring to.

>> There's like some papers based on lettucees and stuff. Are you saying they don't >> so so like uh Brandon David's uh papers on like u I've been to a bunch of talks that show >> Yeah. So they do bar so they can do this partial nondeterminism. No. Yeah, but not not not just just spark, but also like other papers that get rid of the the >> So for snarks for NP, you can do it based on uh maybe stuff like IO. Um you can do it based on knowledge assumptions. That's sort of the extent of what we have.

>> And what about if you don't need the success? >> I mean, if I don't have I'm not talking about zero knowledge here. So if I don't have success, I don't have anything. I'm only insisting on uh short proofs. This entire talk is not, you know, you could have zero knowledge on top, but this was all about succinctness, but of course, if you don't insist on success and want zero knowledge, then we have non-interactive zero knowledge. Um, NISK. Yeah. >> So, yeah. So, Nzik is like, no, if you don't need success, we do, but uh in principle, we don't uh have to.

>> Yeah. I think I asked you this in the past, but I thought that CRT25 is for all NP. >> No, no, no. It's for like NC, so much much more restricted. >> Yeah. Oh, so so we have a result like a NISK. So if you want zero knowledge but no succinctness, we do have a result for >> Oh, okay. And it's also CR225. >> Yeah. So we have to that's why I'm okay. >> Yeah. Yeah. Yeah. Um so first of all it's a limited scope and second as Elena is saying it is uh very far from practicality and in different levels in but you know for one thing in contrast to frame which only uses lightweight hashing here it's using very heavy use of public key crypto in particular things like FHE so I think it is you know um

rather than saying it's impractical I would say that it is a grand challenge for us to make it more practical because a lot of things that nowadays people are implementing five or 10 years ago were considered wildly practical. So I think this is very interesting. >> If they rely on fiat, are they using correlation interactable hash functions? Yes. Yes. So, um, yeah, most most if not all of these works are Yeah. Um, okay. So, that's sort of like one side. On the flip side, I want to talk about mitigations. Are there ways in which, you know, should we like uh just pack up all this amazing work that's been done on ZKVMs and, you know, on with with Jolt with SP1 that we're doing at Sync and others or, you know, how worried should we be about the attack is one way

of putting it. I think we should be worried but I want to point out that actually uh preventing the attack is quite easy. So in the following sense so the key source for our attack is the fact that the circuit for which we are proving things could evaluate the hash function. What you could try to do is make sure that the circuit that you're proving for sure is not strong enough to evaluate the hash function and then I would no longer know how to apply the attack. So for example what we were suggesting in the paper is to increase the depth of the fmeir hash function for example by uh iterating it a couple of times so that the depth you know it's hard to argue that by iterating it the the actual depth formally increases but you know

practically probably does you can certainly conjecture that it does make the depth of the hash deep enough so that there's no way that the circuit would be able to compute it and if you do this I don't know how to run the attack but I also don't know how to prove security and and sort of like previously we could have said you know we we have the analysis in the random oracle and we're uristically instantiating it and now we can still say that but we also know that the random oracle does not capture real world attacks that could break actual security so it really uh to me it really like shakes our confidence um in what's going on here I also want to point out a work um that was published just a few weeks uh so a followup to to our work by galonv

um very shortly after our work which so they were proposing a different mitigation. So instead of increasing the depth of the fetchir hash they were proposing to make it sort of like harder to compute the fetch hash drastically. If you make it harder to compute that makes the verifier slow. So they actually do it via clever use of a proof of work. So that's a nice idea. So it's a different form of mitigation. Um they also show that their transformation is secure in an in in an an idealized model which is in a sense better than the random oracle model but on the other hand it doesn't really capture our attack. So I think the the model is is natural and and and it's interesting but

I wouldn't say that you know it doesn't like greatly increase my confidence that things are okay. I would say it way. So ju just to sort of uh summarize um what we what we show in this work is that this random oracle uh model or idealization is it was known for a long time that it's an idealization and it doesn't capture all facts that you could in principle do. Here we show that it can actually be problematic in practice for a deployed protocol which I think is concerning. So let me kind of conclude with some uh open questions that I'm I'm excited about. So as I pointed out, it's not difficult to avoid the attack. You just like increase the depth of your hash function for example and the attack will not go through. Um but beyond the fact

that the specific attack doesn't go through, we have very li limited evidence for security. So I think studying this is uh in my mind extremely important. Um so really especially for for for students in the crowd I think this is a fantastic thing to work on and extremely important to you know this entire like industry of like many billions of of dollars. Um so I think this is extremely important and as a specific challenge think of this mitigation you know if I make the hash function a little bit deeper than the circuit can you still can you mount an attack? I would say that this is not a warm-up. I would say if you can do this then we're in a lot of trouble. if you can do this kind of thing, I would guess that there's

nothing like anymore that's specific to GKR um that's problematic and like really the the common setting of uh of of Famir say for things like Starks and and Fry and so on would would also be in in a lot of trouble. Then I think uh something interesting to do something we sort of didn't get around to but I think is really interesting. Um it seems that the recursion circuit is a candidate for which we could maybe mount our attack. Um so it would be then I wouldn't even need to like make any sort of discussion of whether it's like the attacking circuit is natural or not. This would get like a full end to-end attack on a system. Um so that I think is really interesting you know so think of the

system before mitigations were in place. Could you attack it end to end? That would be really interesting. I think another super interesting directions is to try to attack uh specific protocols that are very that are built on GKR like say lasso or or or log of GKR or other things um in which you don't have a lot of flexibility with the circuit the circuit is fixed so it seems you cannot mount this sort of attack but then again the evidence for security relies on the more random uh analysis and you know so I don't know an attack and I would love to get either confidence or or see show an attack. Um, so so better confidence in just a random oracle analysis.

Lastly, I I want to point out that you know let's say we live in uh this kind of nightmare scenario in which fameir is broken and we can't use fameir and you might ask you know are all snarks doomed and I would say that answer is probably yes but we do have snark constructions based on other idealized models like the gen generic group model or something called the the the AGM the group model and we might say you know I tend to think of these as like much uh worse models than the random oracle model, but the fact that you know if we had a break on the random oracle model doesn't necessarily mean that those models are kind of broken as well. So I think a really interesting um direction would be to try to mount similar style of attack

against these other idealized model uh idealized models. And I should point out a work by Dant uh from 20 years ago. It's a follow-up to the this uh uh CGH paper that I mentioned which does give an example of a contrived protocol in the GGM which is secure as a protocol in the GGM but if you instantiate the GGM in some way then you have an attack okay so I think if you're able to extend this further that would be also extremely interesting um uh yeah >> what about other proof systems that use random oracle besides GKR >> um the for fiair or in what sense >> for fia shamir. Yeah.

>> Yeah. So our attack really leverages something that is somewhat unique to GR which is that you don't uh commit to the entire computation trace and that is really the claim to fame in a sense of GR. It allows you to commit to very little information just to witness. So in traditional proof systems usually do the entire computation commit to everything and GKR gives you a way to commit to only a small amount and our attack really leverages it and for anything more or less except GKR you are committing to everything which makes sort of a typically yeah and and that is so the thing that gives you efficiency with GKR is also the thing that we attack and it's something that other protocols don't seem to have Um but it's

a great open problem. >> Two questions. Um one is maybe more of a comment that maybe it'd be interesting to find out if you agree with or not. Um so I guess the recursion circuits they tend to sort of check that a hash is right instead of compute the hash um from scratch if you will. >> I don't know if you think of like a Merkel tree then you probably got like one side um and the other you do compute right. You got the like one you have the two children. >> Yeah. And one of them you get just a save. You could have given everything >> but to save on proof size maybe you give one and the other side you compute >> and but okay the way to say is when you do compute the hash you tend to get like a bunch of non-deterministic advice to

keep >> so that kind of automatically keeps the circuit low depth perhaps lower depth than your standard. But you know if you didn't have this attack in mind and you were saying ah let's be super aggressive and try to minimize stuff we commit to maybe you know our circuit is low depth let's use GR for recursion right and I could very well see people wanting to do that >> right so to avoid exactly for sake of efficiency avoid committing to the intermediate steps of the hash um right so if you didn't have this in mind I do think there's something you might end up doing >> yeah potentially okay um other questions So I guess um trying to give evidence for security of like GKR just for grand

products and in lookup arguments say >> um we sort of know waving my hands a little that that's >> sort of enough to build a whole ZKVM which is enough for all of NP right >> and then so uh we have barriers against so I I guess two questions here >> the barriers are you mean like junky wick kind of barriers nowadays I don't know if people would still consider it a barrier. So, >> okay. So one question is you you think people might just manage to show um security in the like snarks in the plane model for all of NP um in the >> um >> you think that could happen in the >> I think I don't know it could happen especially like uh people do crazy things with IO so so maybe for me I'm you know uh

hoping not to be a hater but I would love to think of attacks um you know so it seems like very innocent the the circs you're doing are say a grand product just multiplying a bunch of But you're still you're controlling the the things you're so maybe grand product seems more safe. But lookups are feel like more general purpose in a sense. >> But you can build a lookup argument just out of the grand product. >> Uh >> like once you have a grand product, you I can directly reduce lookups to that. >> Yeah. Yeah. But >> you're saying that redu like that reduction >> the reduction doesn't do much. So I think for both it's more of a question.

So so the circuit is fixed. So not not too much you can control. Things you can control are sort of the inputs. >> Yeah. Can you bake in the hash function into the input that you're doing and do it? Seems very difficult. I have no idea how to do it, but it seems very important as well. It's kind of like um what are uh do I think it's risky? I think the odds of an attack are very small. If there were an attack, the damage would be uh crazy. So, I think it's very important to invest at least time thinking about this. >> Yeah. >> Can you say some more words on why don't you view Gentry Wick as a barrier? So for one, it's been avoided using IO. Um, so it has a lot of caveats, right? It's only about uh >> what does it state?

>> So there's the what what they're stating is sort of is a barrier for proving snarks for NP in the plane model. So when you don't have say a random oracle and so on. And what they're saying is that you won't be able to uh so suppose you you built a snag and you've tried to so you have a proof of security. If your proof of security is what's known as a blackbox reduction, meaning that it would map any uh adversary into an attack on some like underlying cryptography. So if and the way these reductions usually work is give me an attack, I can map it can use it as a black box to break the crypto that so almost always that's how it works. So that's called the blackbox reduction. So if you're trying to um show that your snar has

adaptive soundness using such a blackbox reduction um you won't be able to. Okay. So caveats here are a it's it's targeting adaptive soundness which is I think in applied word you do want it but for the basic notion nonadaptive might be interesting and there are tricks that once you have nonadaptive you can sort of lift it up uh to adaptive. >> How does IO evade this essentially? So IO evades it because the IO argument uses uh subexponential number of hybrids. Um so sort of in some sense subexponential assumptions are a way to get around it.

>> Um >> you're saying it's an unfalsifiable assumption. >> No no no it's uh it's it's quantitative. So you need to understand the fine print of gentry wicks and uh yeah and the other thing is you know we have it's true that like usually we like proofs that are in which you use the adversaries as a black box but we do know proof techniques that don't do this and somehow to me the lesson has been with these like uh barrier results they're more of like often like indicating in what direction you should try to to push >> this um >> so it certainly seems very difficult to do But um I would say that I would not be shocked if someone managed to do it now.

>> And then what uh how would you be shocked if someone manages to prove plain model security of like a snark we're used today? Because all this IO stuff is obviously not something we use today. >> Um I would be pretty shocked. >> That would be shocking. But the IO something like that. Good shock. >> Okay. >> Um yeah. So ba based on you know nothing so just prove period no like assuming collision resistance because so we don't actually an interesting open problem is like do does the existence of snarks even imply one way functions I think maybe for sufficiently strong snarks it does so you wouldn't hope for an unconditional thing but you're probably assuming you know you're you're

happy to assume collision resistant hash or stuff like that >> yeah I mean look my worry is that you know I don't know maybe we get snarks in the play model from IO say yeah but we still have like no idea if you know Jolt or SP1 when running on interactively is secure you know 15 years from now. That's my that's my worry. >> Yeah. So I mean this also true for uh encryption right we don't know that it's secure but we have candidates and they've stood the test of time for for a long time. I would like it for it to be that you know there's this so I believe that 15 years from now both encryption and argument and so on will rely on unproven cryptographic assumptions. The question is what are the assumptions? I would like them to be sort of as clean as

possible in particular to have the kind of thing that we like in cryptography which is a win-win. So either you know the proof system is uh secure or we know how to compute discrete algorithms very efficiently. So I would like to have that kind of flavor. Am I super optimistic about doing that? It seems very very hard. I would love to do that. I seem I think we are still quite a bit quite far from there but you know 15 years is a long time. So and we have uh talented students here. So let's do it. All right. Thanks so much.