Recursion Security

Transcript

Thanks Ron for the intro. Also, thanks Giacomo for the setup because I guess recursion and Fiat-Shamir very related. So, yeah, I I will just introduce the main problems that we plan to talk about. Um very very shortly, what is recursion? I think we all know. You want to prove that you know a witness and when I say recursion in this talk, what I mean by that is you instead prove that you know a witness or a proof. So, that should be equally meaningful just by intuition. Um and why do we care about it in let's say in the context of Ethereum? We care about it because of CKVMs where recursion is used and also in this distributed setting where you want to aggregate signatures and then aggregate

their aggregates, you are using recursion. So, you can think of this as being a SNARK that proves knowledge of a list of signatures and then this is a proof that you know two SNARKs that prove list of signatures. So, this is also where we use recursion. Okay. So, let's look at it a little bit more abstractly and I want to really have one working example of a recursive relation that is the most simple one that I could think of and that I will use. So, very roughly, what recursion does is Alice has some statement X, some instance and she knows either because she computed it herself or because she received it a proof uh for that instance X that convinces her that this is a

valid instance. And now, she proves knowledge of that proof and she gets another proof and this is what we mean by depth. It increases the recursive depth by one. Okay, so uh what does what do I mean when I say she proves knowledge of that proof? Well, she proves uh using a SNARK for this relation R prime. Okay, so let's read this. So, the relation that we ultimately care about is let's call it R. This is our base relation. We want to prove, for example, this is a list of public keys for which we know signatures.

Um And then the relation for which we actually use a SNARK will be something like this. So, either you know a witness, this is the first case, or you know a a proof which is accepting for depth I minus one. Okay, so this is the most simple recursive relation I could think of that somewhat makes sense. So, if we now see a proof under our prime, why should we intuitively be convinced that X is a valid instance and someone knew the witness? So, it's actually quite simple. So, let's say we see a proof pi D uh that verifies under a SNARK for our prime, then by knowledge soundness of that SNARK, someone must have known the witness and produced that proof. So, we can extract it via the extractor that we

get from knowledge soundness. And by the definition of the relation, this is a proof of depth D minus one. And now we have another process that generates a proof of depth D minus one, so we can apply the same argument again and extract a depth D minus two proof. And we do that all over again until we end up with depth zero, and then by definition of the relation, depth zero means we will extract a witness for R, the relation that we care about. Okay, so that's very roughly the intuition why recursion should work.

Uh in in this session, we want to really understand does it does it really work and where are the limits of our understanding of it? And we want to make explicit where the limits are by defining heuristics so that, for example, we can later write them down formally in Lean and then prove security of CKVMs end-to-end. Okay, so where do we stand with our understanding? So, the first thing, I guess we all know that, is if you have an IOP and it's round-by-round knowledge sound, then you can apply the BCS transform, like Merkle trees and Fiat-Shamir, and you get a knowledge sound SNARK.

Okay, that's great. Now, when we compose these Narks recursively, what we also know is that if we do it in the right way and we define our relations properly, then the recursive composition works just by this recursive extractor argument that we have seen on the on the previous slide. And what what does that that mean? It means for example, the signature scheme that we build is unforgeable or the CKVM that we build proves the computation that we care about from the first state to the very final state.

Okay, so looks good. We have this implies this, right? Not quite. So, actually these two results live in different worlds. So, on the left-hand side, we get straight-line extraction in the random oracle model, which is a strong notion of knowledge soundness, but in an idealized model in the random oracle model. On the right-hand side, what I will tell you is that we better do this in the plain model. Okay? And the goal is really to understand what is this gap? How can we make it formal? How can we bridge it?

Okay, and I guess an obvious question is why why do I say this should be in the plain model? Why can't we just do this whole thing also in the random oracle model? Let me spend one slide on it. Um So, question is why can we prove why can we not prove recursion just in the plain random oracle model? And for that, we look at our relation again. So, this is the very same relation as we had before, but now we are working in the random oracle model. So, as you see, the verifier needs to query the random oracle. Okay? And if you look at this, this is not an NP relation and our Narks work for NP relations. This is a relation in NP in this funny world in which every machine

has access to this random oracle. And if you don't have access to the random oracle, then if I give you a statement and a witness, you cannot even check whether it's in that relation. Okay? So, this is what we call a relativized relation. And if you want to make recursion work formally, then we need to prove this relation with a snark. So, we need a relativized snark, which is a snark that can support these languages. Uh or these relations. Okay. Unfortunately, there is a very nice paper, which is one of my favorite papers that says this is not possible.

Uh two of the authors are here, I think. Um And yeah, so what does this mean? Does it mean that recursion is broken? No, it does not. It just means that there is one particular relation that is relativized and for which you cannot have a snark. But, it at least tells us that via this route of relativized arguments, we will not be able to at least easily show that recursion works. Okay. And uh if this is impossible, then for sure we should not write it down in Lean as an axiom. Uh because then we would assume false and what This has all sorts of bad implications.

Okay. So, what I mention uh for completeness is that there are models that are variants of the random oracle model uh in which relativized snarks exist and so we could analyze recursion in these models. Uh the question is how realistic are they? Uh so, I will for the rest of this talk uh set them aside. But, uh it's just it's good to know that they exist. Okay. Coming back to this picture, we have these two worlds and we now know this lives in the random oracle model. This is somehow we should think about it as being in the plain model. Okay. And now, the first heuristic that we could make is that well, we already do that when we deploy these systems in practice, even if we don't do

recursion, that knowledge soundness in the random oracle model implies some form of knowledge soundness in the plain model. Okay? And this is the Making this heuristic explicit would bridge the gap. Okay. And uh this came up in a lot of discussions with Ron and and other people, but yeah, mainly with Ron and this is why I call it Ron's heuristic. Okay. Um Okay, so this is this is uh one part of the puzzle. The other part is uh let's look at this recursive extraction and let's assume we are in the standard model. Let's forget about heuristic A and let's look at this side. So, it's also not entirely clear that we know everything we could know about this

step. And for that, let's look at this picture again. So, I've argued before that from this proof, we can somehow via recursive extraction extract a witness. Okay, the picture becomes a little bit more complicated if we look at running times. So, let's say our adversary that produces this proof runs in time T. Then, what do I know about the adversary that produces this proof? Well, it's it runs the adversary and then the extractor. Uh and if you are in the standard model, often when you prove knowledge soundness, you will use rewinding. So, you will run the extractor the adversary multiple times. Let's say we're in the most simple case where you run it two times, then this will run in time 2T. So, I need time 2T to produce this.

And then I have the the adversary that produces this whole thing, so that runs in time 2T and I again apply the extractor to it, so I get a two times overhead again. And I do that, so I get a two time two to the D times T to produce this final proof. And if I'm in an asymptotic security land, then I still need this to be polynomial in the security parameter. Yeah. >> Uh is this is this only happening if you use rewinding? >> I mean, this runs whenever you have sort of a black like a black box statement that your extractor runs in time 2T. But, this just an example to illustrate. It's not for a concrete proof system or anything. But, whenever you use rewinding and not

straight line extraction, you have this running time overhead for the extractor, and it means that your depth is bounded, right? Because this thing needs to be poly, and if your running time overhead is two, then you can afford a logarithmic depth. If it's poly in the security parameter, you can only afford a constant depth. Okay, so we don't live in asymptotic world, right? We deploy systems in practice, so it's not really clear what it means, but it indicates that there's maybe uh some challenge there or some limitation in our understanding. >> [snorts] >> Okay, but I also want to say that there's no matching attack, and it would be really cool if uh someone comes up with at least, let's say, a contrived SNARK where there is a matching attack or where we can prove that every extractor must run in time 2 to the D *

T or something like that. Yeah. Where it's proven? Okay, that's great. Yeah, okay, recursive AGM is even more crazy than uh than recursive wrong. I I I don't want to talk think about the AGM honestly. You can prove You can prove wrong knowledge assumptions in the AGM. Right.

Okay, so uh Yeah, I think uh closing our gaps in understanding here would be good by finding more contrived counterexamples, less contrived counterexamples, or I don't know, finding a scheme where we can actually skip some rounds of the extraction and take a shortcut, and yeah. Uh the other thing that we see here is that we have uh for every step there where we do the extraction, we actually have some some error. With some small probability, the adversary will be will be able to forge a proof, so the extractor will fail. And uh if we just do this naively, then these errors will add up over the rounds, right? We have to If you do it naively, we will have to take a union bound over all these errors. And if If you fail at one of

these steps, you will fail. Uh I think this is less of a problem intuitively because well, the SNARKs that we build, if we are build them via BCS, and if we then, let's say, domain separate and uh put into the hash where Where are we in the recursive topology, then at least the adversary has to split its query budget uh across that. And so, I think this is more like a This is more intuitive to me that this is really an artifact of of the proof. Uh whereas, the other thing could be an artifact of the proof. Uh Yeah.

Anyway, so, uh let's say heuristic B for now is that uh the depth doesn't cause any issues. And these two things are just proof artifacts, okay? Okay, then we are back at this picture. We have now two heuristics. And uh the question is is this Is this it? Is this all we need? Uh I think we I think it is all we need, but we need to think more about heuristic A. And in particular, what is this notion of knowledge soundness in the plain model? And uh I want to spend some slides on that. And I want to show you three notions of knowledge soundness in the plain model that all have their issues.

Um And the question for the workshop will then be what would be a good notion, for example? Okay, so, let's start with the first one. This is the most simple one. Um Intuitively, knowledge soundness says, "If you give me the proof and the statement, then I can extract from it a witness." But what does it mean from it? So, in this very simple notion, we say there is one extractor that works for every adversary. And we look at the following experiment. The adversary outputs a statement and the proof. The extractor outputs a witness. Okay? And then we want that the probability that the proof accepts and the uh statement-witness pair is not in the relation is small. Okay, so, this is maybe if you have an intuition of what knowledge

soundness means, this is what you would write down. But, you immediately see some issue and that is there's some compression going on, right? The adversary sends very small information and the extractor has to produce large information. And you can actually show that if at least if collision resistant hash functions exist, I think there's a stronger one based on one-way functions, uh but under that assumption, this is impossible. Let me quickly tell you why. So, let's consider the following adversary. It samples a witness and then it outputs the hash of that witness under some hash key.

Remember, we are on the standard model. Um and then it honestly proves knowledge of that witness. Okay, this is a valid adversary. It always produces an accepting proof, so we should be able to extract from it. So, we extract a witness W prime and now there are two cases. Either W is equal to W prime. This is very unlikely, right? Because essentially here, you have a you have a channel over which A sends short information and then the extractor extracts a witness. So, you you're literally compressing information if you recover the exact witness. If you recover another witness, then you break collision resistance, right? Because you have now this W prime, which is a

pre-image of this hash and W is a pre-image of this hash and they are different. Okay, so we need to change something. That definition was way too strong. We cannot achieve it. It should not be the definition that we use in our heuristic because that would again mean we assume false, right? And then Lean would do all sorts of crazy things. Uh Okay, so let's let's make it weaker. For that, we the first thing is we change the order of quantifiers. So, we say for every adversary, there is an extractor and that in particular means that the extractor can depend on the adversary and it can depend on its code.

Um and then we run the same experiment, but we also now give the extractor, let's say, A's random coins. The coins that A used to produce these. Okay, so now intuitively, there's no compression going on, right? Because the coins could be as large as W or even larger. So, this is good. It seems that this is It's possible that we can achieve this. The problem is that it's often quite a useless notion. So, if you want to use this in some application, let's say you want to build a signature scheme from it, or you want to build you know, signature aggregation from it, then the adversary is not just a box that gets random coins and outputs stuff. It's a box that gets as input some other information, for example, the

public key of honest parties. And then based on that, it would find a proof. So, for example, it could be that we give the adversary G to the X, and it produces a proof of knowledge that it knows the D log. This is not modeled by this definition, and in fact, you can you can sort of show protocols that should intuitively be secure, but based on this notion, you cannot prove them secure. So, this is a notion that is too weak. Okay, and maybe so more of more of a meta point is that if the coins are so large that they carry enough information to extract W, then what what is the extractor doing with the proof? So, it feels like a weird notion where the proof is just ignored. So, what's the point of the proof?

Anyway so we had one notion that was way too strong, then we went to something that is too weak. Let's make it a little bit stronger again. And for that, we give the adversary an auxiliary input. So, it's the same picture as before, but now both the adversary and the extractor get an auxiliary input, and think of this as being this public key of the honest party that I've mentioned before. Okay, and then you quantify for all adversaries, there is an extractor that works for all auxiliary inputs. So, if you are familiar with UC, that's pretty much the same. So, that's also why it's Z, so the environment and you see is also often called like this.

What? Why don't you do UC? Anyway. Okay. Um so, as I said, this auxiliary information, this it could be everything that the adversary obtained from the environment, which could be cryptographic keys and and all sorts like that. Um that it used to produce that that forged proof. Okay. Unfortunately, this is also impossible. Um and we can really do almost the same uh impossibility as on the in the first variant, but we need to sort of hide it under obfuscation. So, the intuition is that we put into that uh auxiliary

input, I mean, has to hold for all auxiliary inputs. So, let's put an obfuscated circuit that implements the impossibility from before. Little bit more precisely, I don't want to go too much into details. Uh if Z contains an obfuscated circuit that pseudo randomly picks an a witness and then outputs an honest honestly computed proof, then our extractor doesn't need to do our adversary doesn't need to do anything except like take Z and execute it, and then we have the same result. And because it's obfuscated, this additional information that you give to the extractor doesn't help the extractor, and you can sort of do some hybrids and then switch to the impossibility result from before.

Okay, so that's bad. We now have three notions. One is not applicable, two are impossible. What do we do? Uh one uh thing that has been suggested is to restrict the the distribution of the auxiliary input. And like this last impossibility was based on a very adversarially chosen auxiliary input. If you think about systems where this is the public key of an honest user, maybe be so realistic. The problem is what should this distribution be because we For example, you may say, "Oh, it should not contain obfuscated circuits." But then maybe in a few years, obfuscation is ready and we use it on Ethereum layer one for whatever reasons, and then there are all sorts of obfuscated circuit that

the adversary could use as input to help him forge proofs. Okay, so this is not so clear, and this brings me to my last slide where I want to set the open questions for discussion. So, the first is if we accept this heuristic A that in knowledge soundness in the random oracle model implies some form of knowledge soundness in the standard model, then what is a good notion of knowledge soundness? It should be achievable, of course. It should not be just plain false, and it should be usable, strong enough so that we can use it in applications.

And the second is this whole discussion around depth and how to interpret the security loss. What does that mean in terms of bits of security? Should we put on our website this thing is end-to-end 128-bit secure? I don't think so, but under certain heuristics, we could we could say that as long as we make these heuristics explicit. And uh yeah. So, that's I guess where we should start the discussion. >> [applause] >> Okay, so really um thanks for the fantastic presentation, Benedict. Um I think the the main point now in this like a workshop is a discussion about these points. I think these are sort of two related but

different points, and to organize the discussion somewhat, let's start off by kind of maybe discussing point number one. Um and then we'll switch to to the second point. Um and we have some experts also in the crowd. Um Uh I don't. Um so so yeah. I know it's two is much easier to discuss, I think, so So, why intentionally I want to give enough room for one. >> Can I ask an annoying question which I I keep mentioning when we have these discussions? Do we have to be in this world or can we find a model where ballot box snarks exist like the A ROM and should that be part of the discussion as well?

>> Absolutely. I think it should be and very happy to hear opinions. My opinion is that, you know, I am not a huge fan of idealized models. I think it's good for sanity checks, but as you know, you know, sanity check is better than no check, but then like putting all of our kind of like belief is in in this model and then once it once it's out there and then you kind of start abusing it more and more. I personally am not I'm not a huge fan, but I think it's really a discussion, so if you think differently or others do, I think it's it's worth discussing.

>> I guess the same could be said of heuristics A and B. >> Right, so >> We can rely on them and start getting used to that. >> Better than nothing, but I think it's >> So, so unfortunately we're in a situation where we don't have a good solution I think and we need to choose between bad ones. I think putting like, you know, very uh explicitly what are the heuristics that are are put in place gives a more clear message than an idealized model that's maybe not the most natural which helps us pass a sanity check, but beyond that we don't understand it so well. Uh Adam?

>> Yeah, first thanks Benedict. Where did you go? Okay. Hi. Very nice talk. It was putting a um a very clear and systematic way thoughts have been kind of flowing around for for years. Um I mean I I don't know of a good intermediate knowledge soundness notion. Um maybe there isn't one. I hope there is one. Um I wanted to >> [clears throat] >> mention at least um some uh uh I don't know, things you can try to do that I'm not sure that you can literally put them as like lean statements, but they kind of teach you something, right?

Or at least should teach you something. Um one thing could be to concretely analyze the security losses for a signed oracle, right? You could say, "Okay, there are no more oracle by itself, you cannot check it in a circuit, but you could imagine augmenting it with a signature scheme. With a concrete signature scheme with you know, concrete security, right? Like you quantify the uh the you know, forging error as a function of the size of adversary, the number of queries to the signing oracle, and all these things, right? And you try to work your way through some proof of security of uh well, you can try to prove me I don't know, Micalli or BCS uh secure with respect to that oracle. You see

concretely what happens. And you try to work your way through the kind of now possible concrete security reduction of either IBC or PCD. And you kind of unfold all of this, right? And you see kind of what comes out, right? There is going to be some sort of envelope of attacks that uh um are ruled out, right? Uh of course, there are some attacks possible in practice that are not covered by such an approach, but I'm not aware of like I say, some end-to-end concrete security analysis of this kind of signed oracle construction.

>> Can you can you say in a bit more detail what you mean by signed oracle you mean >> You just take uh the random oracle and you augment it with uh a signature scheme. So, that's your new oracle, right? It's >> What does that suffice for arithmetization? >> No, you you can you can verify the the the questions to the oracle in in the circuit. So, so you don't need to embed like basically, your your new let's say, SNARG in this signed oracle world has a verifier that lives in NP rather than NP to the Oracle, right? So, now now you you can actually articulate, uh, let's say a replacement construction, right? And analyze its concrete security. So, I I think this is doable. I think if you

take a powerful model and you kind of stash in it kind of sufficiently kind of clear existing literature and you ask it to go in this direction and churn churn churn churn, you will get some some reasonable bound. Then you have to stare at it and see if it does it look good or not, maybe managing the model a bit. But, this I think would be like an interesting thing to do, right? And you can also try to do kind of not only get a decent bound, but optimize the bound and see how far can you take it, right? >> So, so you're saying this in the in the context of the this is like Would you say that this is within the framework of working with like other idealized models because you >> Yeah.

>> My my so, there's like the question of like the sanity check and the understanding concrete security via this um I guess that that those are the two things you're >> Yeah, this is this would be like, uh, some sort of kind of bait and switch, right? Like I we want to analyze what we have in practice, we don't know how to. We can try to replace it with something that looks as close to it as possible and try to see what we learn, right? >> Our paper our paper does cover that case right? >> Yeah, so this leads me into another kind of thing that I think is not I don't think it's as good, but it's it was trying to win the direction. So, with the ZK-SNARK we tried to do precisely this some time ago purely in the ROM. Now, when you're

purely in the ROM you don't have signatures, then what are you going to do with your queries and answers? So, what we proposed back then was to just forward them along, right? The like just don't prove them, just pass them on as like, uh, ever accumulating claims down the line, right? >> The like a community >> Now, of course, your construction now has deviated from what you have in practice because it is no longer succinct, right? But, it's kind of morally trying to track of what's happening in practice because what were you going to do with these queries and answers if not check them, right? In the real world, you kind of embed them in the circuit and they kind of disappear through succinctness.

In this alternate replacement construction, they're forwarded down for the last verifier to check. Who will check them, right? Now, and we did look at what would happen there and we were kind of try to be reasonably careful and you get something. You get some signal. Like certain things that could have blown up don't. Um I think another step in the direction would be So, I think this would be like that was the the the the step zero, right, of trying to approximate reality. The next step I would take is something like the signed oracle and see does anything else change or uh and you can argue about whether the second step is a further step or a different step. Maybe there's a discussion to be had.

But either way, whether, you know, these steps are kind of pointing the same direction or slightly different directions, they're clearly going towards reality. And then you can could ask, "Okay, are there any other steps you could take to go towards reality?" I'm not sure, right? But this is this is kind of uh um at least it's potentially a spectrum that you can travel and on each step you take, you would have some sort of end-to-end concrete security analysis with straight line extractors, right? I I actually don't have So, these are ideas that I think are somewhat tractable. I don't have any actionable suggestion for the other direction. Kind of within the the >> plain model.

>> Yeah, within the plain model. >> Yeah. Um So, again, so so like really as as I saying, I guess Benedict as well, like one direction here is to work with with idealized models and um I don't think that they're inherently bad, but I think um we should only put so much weight into into what they give. Um >> Sorry, I also jump in. I want to distinguish idealized models that are attempting to model what's in the real world and other idealized models that push you down other constructions like for example what kind of we did back back in the day in this like low degree random oracle and arithmetization random oracle.

Yeah, you have relativized SNARKs but then the line constructions are distinct from what we actually use in practice. So they're like uh a potential outcome would be okay, you can Yeah, exactly. Change the protocol, right? What I was suggesting was not that. It was just like stay with the protocols. But then try to kind of consider idealized model models that seem to model what's happening with the current protocol. So I would view these things are like different types of questions about idealized models.

Uh Benedict behind you. >> So I think I agree with what you said in a sense that you know the more analysis we have in different models, the more confident we are and the more attacks we rule out. But I I want to come back to this first question. So one approach that I that I didn't mention is that So right now the the last definition that I showed says for every adversary there's an extractor so that for every auxiliary input and then the question was can you maybe restrict the distribution of the auxiliary input? And the question is what is this restriction?

But maybe you don't have to pick a specific distribution. You just say the distribution is fixed before the before the adversary is quantified. And I'm not entirely sure if this if this already rules out this impossibility. So you would say for for every distribution >> useful though? Is it that does it really really capture reality? >> what is the distribution that we would care about? So consider the following setting. You uh you sample G to the X. You give it to the adversary and you ask the adversary to output a proof of knowledge of X, then the distribution that you care about in this particular application is the distribution of all G to the X.

Essentially, the distribution of random group elements and nothing else. And in that particular setting, um this would be covered by that notion, right? So, that the question would be, is this a useful thing? And uh or I think useful it's pretty clear to me, but uh is it impossible? Does this other result extend to that? Because then we didn't make progress. But if it's uh if it's not impossible, then we could use it as a heuristic and specify it in Lean and be sure that it's sort of there's a sanity check. There's like a Yeah. I mean, another thing that we have to say if if we talk about, you know, assuming impossible notions, then they are most of the time they are only

impossible because you also assume compression. So, if you if your Lean if your Lean code base does never assume explicitly that there's compression, but proves everything else, then I think there's not I mean, my intuition is that there's not the danger that we prove something from false. Because we we actually don't assume something that is impossible because we leave out the compression thing. That's just an efficiency thing. So, uh yeah. Just wanted to bring it back to these notions. >> Dmitry, you have a mic?

>> Yeah, um actually one So, if uh the first uh heuristic is um it's difficult to get having all the three properties, then maybe drop the the word usable to some extent. I mean, well, after all, this is all about uh proving uh RISC-V program. So, something little bigger. When we think about kind of generic SNARKs for NP, we always face this impossibility results and counter examples. Maybe we should kind of step on ourselves and restrict to something to much smaller world, be less usable, but kind of be more satisfied with >> So that if you're only proving

limited class of statements, then even though we we plan to prove general pretty general statement. >> Yeah, of course we want to prove general, but maybe we should start with limited. >> So like maybe within the world of signature aggregation or something. Something like that you mean? >> Yeah, well, but maybe at least try with like limited set of risk-five programs. And that will also give us hints how to restrict auxiliary input distributions and all this stuff and will rule rule out obfuscation things. >> So when you say a limited set of risk-five programs, what do you what do you mean?

Like what what sort of limitation are you imposing? >> Well, like I know small set of uh >> set of instructions that >> Small set of instructions of a small size of the entire program and like [clears throat] very like for example low limit on the number of steps. If it helps in any kind of no For example, if we can't prove meaningfully billions of steps, maybe we can say something about a thousand. >> Somehow I think the the the negative examples usually come out of like proving like cryptographic things and the things we actually want to prove are cryptographic things.

Uh I don't know. I guess I don't know and you know and Z you've worked on this. So what's what's your feeling? >> I actually wanted to bring up another active line of work on kind of this rat by zation recursion. Not not really recursion, but rat by snarks that might be like related to I don't fully understand what you mean by limitation, but in a different context, people have been looking at ways to get around our impossibility, the one that proves rat by zation cannot be done uh, recursion cannot be done in the random oracle. Um, so, just two sentences about the intuition of the impossibility. Impossibility is looking at like one specific class of languages

relation where, uh, kind of the, uh, deciding a language really, um, relies on the fact that you know the entire witness and the verifier has to like make a lot of queries. But, what if we restrict our attention to kind of a subclass of, uh, circuits where, um, the circuit has oracle gates, has recursive calls, but, uh, you can kind of corrupt epsilon portion of the oracle calls, and then the circuit remains intact. This is like robust robust kind of circuit. They're still NP-complete, um, in the random oracle model, uh, in the Rätviss sense, but, uh, with this you can easily get around the impossibility

result by just combining Micalli with some spot check of the oracle gates, uh, where you kind of, uh, again push all the oracle calls into, um, the witness and do normal arithmetization and then check the, um, uh, the oracle gates. And the, a lot of different constructions has been done in this line of work, um, and uh I personally don't know how to use this to do recursion. SNARKs can be constructed easily, but recursion I don't know. But, I feel like, um, the heuristic of, um, uh, not having Rätviss SNARKs for all of NP

in the random oracle model is not that bad potentially. >> Uh, Did I get it right? Um, okay. So, I wanted I want to describe the, um, Zcash context. So, um, uh, first of all, we're talking about, um, circuits and, um, a small number of circuits. So, uh, a one circuits that are fixed by the design in advance. Um and so for our existing system, um use Halo 2, um we have a proof of um soundness of Halo 2 uh with some heuristics for um uh in the

uh AGM plus random oracle model. All right? Um and that's a straight-line extraction um result, so the concrete security loss is pretty low. >> Mhm. >> Um and so my perspective on this is that that security loss is real. Um we it's intolerable for it to to be exponential. >> The security loss from depth, you mean, or from >> Uh uh security loss um uh of the extractor.

>> Okay. >> Um so that security loss is real, it's intolerable for it to be exponential, and therefore um at least for our current um pre-quantum stuff, we needs to work in the AGM because that's the only way to get straight-line extraction. >> Mhm. >> Um uh and therefore, given that we've accepted the AGM, um the problem in extending this to recursion, again for a fixed set of circuits, um is just this impossibility result, the the um is it BCS um 24?

Um so the the remaining question is how to get around that impossibility result in the AGM plus random oracle model. So >> Can you use the cursive AGM? You decide the top. >> Mhm. But but what is the recursive AGM? >> The The recursive So the AGM is like when I uh the adversary outputs a group, there's a in the beginning there's some set of group elements, a common reference string or structured reference string.

The AGM every time the adversary outputs a group element, uh they they explain how that group element is a linear combination of other group elements. So what is the recursive AGM? So the the adversary outputted this set of coefficients of the linear combination. Now, what if uh say some two adjacent elements of of the of that a vector of a coefficients is also a valid description of a group element.

So and and you have to define and some encoding so to say what is it So in that case in the recur a recursive algebraic adversary has to also output now an explanation of this group element. >> And >> And and so forth. And and by the way, uh you could you could define a similar model in in the in the Merkle tree hash-based world. You could be like, "Okay, there's some valid encoding of of Merkle roots. There's some valid encoding of Merkle roots and whenever the adversary outputs a valid Merkle root, it has to output the the witness that that gives that Merkle root.

>> I mean, I I guess like a a Merkle root could just be like pure junk. But so sort of you want to say that if it's not junk, somehow like if if there is a way to to I don't know. I think I think Elon maybe had some ideas about this. >> Right. Right. So you have to So in the group setting you have the sort of what makes it for me intuitively somewhat reasonable is that most pairs XY are not a valid group element. fraction or Yeah. >> So >> So we already have this acknowledged gap in our formalization where the adversary can

evaluate the group hash, right? So So we have a CRS but we haven't accounted for the fact that um uh Yeah, it's possible for an adversary to execute group hash. Um and there are variants of the AGM I think they with oblivious sampling um that we've thought about sort of moving the model to that variant and then we plug one of the gaps. We still have remaining gaps. Um but I mean a formalization with gaps is better than nothing because it it rules out a set of places where we could make mistakes.

Um and those in practice were the the places where we made mistakes. We did the soundness problem in the Orchard circuit was missing constraints. It wasn't anything theoretical to do with our use of Fiat-Shamir. Um so Yeah, I I want to encourage people to formalize things despite these theoretical problems. Um but what do you think about the AGM with oblivious sampling? >> I mean in the context of a hash-based system I'm not sure like or like within like the Zcash context or >> Within the Zcash context or >> not sufficient I don't have sufficient expertise to to answer that. I'm like you know, I I come from a very

theory-friendly background where I don't like AGM I don't like ROM. ROM I'm somehow willing to live with. Beyond that I'm yeah. I don't >> Yeah. Okay, [clears throat] I have two points but let's start with one. So I want to go back to like the question you have, okay, cuz from all these discussions, like if we have a good knowledge and notion that satisfies, I feel that's like a very clean elegant solution. So, I just first want to understand if I if if if I understand the gap correctly. If the extractor runs in the same time as the adversary and kind of we don't accumulate running time, that would be somehow perfect.

>> Yes. >> The problem is if we say for every adversary there exists an extractor, okay, then maybe this exists like breaks crypto and we so you'd say, "Okay, I want a universal extractor." But if I have a universal extractor that somehow gets the adversary, at least needs to run it and then it maybe does more stuff to kind of cannot >> has to run in more more time. Okay, this is the gap. Okay. >> So, one notion maybe that I can propose is kind of saying, "Okay, yeah, you have the adversary.

I'll have like a preprocessing phase where I'm going to preprocess the So, it's not the existential. So, for every adversary there's an efficient transformation that translates the code of the adversary, okay, to a efficient algorithm that runs in the same time and now this extractor >> online phase >> that I did in polynomial time, now online he gets the input and and the proof and now he can provide >> Wait, again, so so for an adversary there exists like a a setup phase that's polynomial?

>> Yeah. >> Um but so kind of what what do you expect like um What is distinguishing this the preprocessing versus the online? Like what what extra information do you know online that you didn't know offline? >> the the proof. >> I see so I see so um got it. So, the instance comes after? >> Yeah. So, you just have like the Turing machine the code. >> Is this [clears throat] somehow maybe it's irrelevant because it's a definition we're kind of like going to assume heuristically and not prove. But I would still that it would be maybe my my criticism which is not sufficient is that do we expect to be able to prove like this notion do we expect that like the the power of preprocessing the adversary

is what will really help you in reality? >> Okay, so that's back to point number two, but okay, that is an assumption that you can put and then you can improve and and have you know everything and then it goes back to your heuristic right and saying okay, this heuristic when I instantiate the random oracle yeah satisfies this notion. >> So so we're never actually proving that this definition holds. It's just like a sufficient definition for everything else to work, which is why I think it's it's maybe reasonable.

Um my like got my my initial reaction is that like how would they ever like if I were to ever like manage to prove stuff is that how I would I would expect to be able to to prove to somehow squeeze stuff out of the adversary in preprocessing. >> Yeah, okay, so that leads me to point number two. That okay, you're trying to capture like sound notion of all snugs. Okay, that we call it composition of all snugs, but in practice we kind of always use snugs that have the format where we commit to encoding of the witness.

>> Right. >> And the extractor kind of only cares about this part. >> Right. >> So the extractor actually would even run faster than the adversary. The extractor doesn't need to run the adversary. It doesn't need to convince the verifier. >> After after trying to >> It to kind of run the entire IOP and stuff. It kind of only cares about this one step the adversary does. >> Mhm. >> And so I think you can do like a lot of contrived examples of snugs where it's actually hard to extract because you don't have the step where you commit to the witness. And so now the extraction notion only that needs to be about the commitment phase, right? So I have a extract adversary. He needs to somehow commit to the witness.

So yeah, either he sends a bogus root and but then he cannot open. But if he wants to send some root that he can open even some percent of the leaves, then I can extract the same percent in runtime that is actually smaller than the runtime of the adversary. >> That I think is quite interesting. >> Um Are you now assuming that the commitment is extractable like by itself cuz there are also some analysis where you do rewinding to go and like extract the commitment. Like the commitment itself cannot be extracted, but I see enough transcripts that I can eventually get what I wanted out of it. In that case, we're still having this

uh like lower problem, right? >> So I don't want to rewind at all. Like rewinding just doesn't work, okay? So let's But I don't need to rewind, right? Like in the random oracle model, we don't rewind cuz we see the transcript. Fine, but like I just needed to exist an extractor and like Okay, so notion of extractor just comes to say that the adversary has to know the witness, right? That's what we mean want to quantify. We don't know how to quantify it like exactly. So we say, "Oh, there's a some other algorithm that extracts." But that's just our notion. We just want to say that you cannot convince without knowing. And yeah, if you have this commitment scheme, so you take your favorite hash function, I don't know,

Blake 3, and you're like, "Yeah, I cannot commit to a witness, you know, without knowing the witness and be able into open." That is like a very mild assumption about the concrete hash function in the standard model. >> So I mean I think we want to We don't need to pass that. >> Yeah, so I think I like this idea a lot. I mean you you explained it to me yesterday already. So I had some time to think about it. Um I think there's still one remaining issue. So even if you can show that So let's say you you let's say you make this assumption this sort of knowledge assumption about that is now about the hash function and that gives you sort of standard model knowledge soundness for the snark.

I'm not sure if it really does because there's still This is the hash for the Merkle tree, but there's still the hash for the Fiat-Shamir. So you would essentially if the the way you decompose conceptually the snark is you say there's a extractable commitment phase followed by a sound proof. But the soundness of the of the proof that follows still depends on the random oracle model. So you would have if you really want to show that the full thing is now knowledge sound, I think this knowledge assumption on the Merkle tree stuff is not sufficient. You still need to have some assumption on the Fiat-Shamir hash that gives you the soundness part of it.

Um but other than that, I think this is a a great direction like Yeah, but you need some other assumption on top of it. It's not like this Yeah, yeah, yeah. I'm I'm just saying this this alone doesn't give you the the the knowledge soundness of the full thing. >> I can't hear properly. Can Can you use the microphone? >> Oh, sorry. I was saying you Okay, you have this knowledge assumption for the commitment, but then like you said you need soundness of the rest of the snark.

>> [snorts] >> For that, maybe we can have like plain model hash functions and that'll be enough. Exactly. Like some property that we assume of the hash function and then cryptanalysts can go and try to prove or disprove that. >> So So okay. You first. >> Um I like the direction. I'll think about it. It's It's very nice. I particularly like the idea of not targeting to understand recursion in general cuz I guess we don't need to. Like I guess it's enough to prove security for whatever, like you know, things that come from IOPs, and uh and they are maybe your original assumption is a sum strong assumption just about the compressing part of the compiler.

Um I wanted to kind of throw in an kind of an another idea. Um I think it's kind of supported a bit by by theory. So, if you look at the constructions of relative I SNARKs, like if you kind of strip away kind of all the um non-oracle part, the the reason why they exist is because somewhere inside of it there is a subroutine that accumulates queries. That's it. There's like it's not a generic NP-style proof system. It's like a subroutine that says, "Thank you for, I don't know, a billion queries. You can You can reduce them to checking, you know, a hundred, right? No matter what you started with, a billion or a trillion and whatever."

So, once you know to do this for some oracle, it basically generically gives you a relative I SNARK. So, here's an idea. You could say, "You know what? Actually, I am going to change the construction in practice. I'm going to use the current tools to split the SNARK into two pieces. One piece will be on the NP part, which will be like an oracle-less circuit where you strip out all the invocations to the hash function. And then you do another SNARK um just in the accumulation part. It will says, "I have checked the following kind of list of queries and answers."

And of course, you need to kind of maybe put something You like you have to make sure you're talking about the same queries and answers and need maybe you need a commitment proof SNARK or like something like that. But then, like if you actually do change the construction that you're using in practice with having these two sub two SNARKs, now kind of your your theoretical issue has been kind of DN Pified, right? Like you you don't have to it seems like you don't have to no longer contend with the full generality of NP, but you purely have to understand the theory of the accumulation part, which is exactly what ends up working out in the other models. And so, maybe like this kind of uh gives you a bit more theoretical

maneuvering room without running into as many as many troubles. But this one of course does mean that you have to change your target construction. But it seems like a a mostly harmless change if that is going to buy us maybe some additional theoretical tractability. And maybe I don't know, this can be compounded with the other suggestion of analyzing a classical constructions that now look like this uh with with some I don't know, commitment. We're sorry.

>> And what do you envision for session accumulation scheme? >> No, in practice you just use another SNARK for that, right? Uh in practice, the oracle gets replaced by a hash function. So, you just run again some SNARK that says I've checked, you know, like a a billion queries and answers. Now, it produces a SNARK proof, right? >> Yes. >> You know, the queries and answers of course need to be coming from somewhere cuz if you just keep them in the instance, there's no compression. Okay, whatever. So, you need to use some commitment proof SNARK. Um but ba- basically what I'm saying is that I don't think it's implausible to change our target to put all the generic stuff without oracles in one piece and keep all the oracle stuff with no kind of generic anything other than a list in a

second piece, right? And then start theoretically analyzing that. >> Do you think it may be even possible to use the output of this snark that verifies all the calls to kind of to run the recursion again, for example? And now use this kind of knowledge or even as a sort of randomness and now do all the checks, for example, the second time. >> Yeah, but it will let you do that. Like I said, if I mean, that's how relativized snarks work. Like if you have such a piece in the Oracle world, then you are able to construct a relativized snark.

Like there there's a generic implication that says if you give me a correlation scheme for your Oracle model, then you can always pair it with like some generic NP thing that has no Oracles and you will get a relativized snark. I hope that that answers your question. >> Try try to be brief to end this point. >> Um >> So so there's another constraint that I'd like to impose, which is that um uh lean proofs uh are only kind of efficient computable reductions. Um we we impose that discipline um uh in doing the the um formalization for Ironwood and it was very helpful. Um first of all, to to constrain the AI not to go off in strange directions.

Um uh and yeah, I I'd like to encourage people to um to impose that restriction because um otherwise it's very hard to reason about um kind of what the proof actually tells you. Uh efficient computable. So So the the lean the lean notion of computable. Yeah. Um it's hard in lean to express efficiency, but it's not hard to express computability. We actually check it in CI.

>> [snorts] >> Okay, so let's maybe shift gears a little bit to talk about the security loss that we sort of observe in improving recursion. How do people think about it? Do you think it's it's it's real? It's not cuz right now we're not really, you know, we we kind of advertise 128 bits of security even though we potentially run pretty like substantial depth. Thoughts about that? Um Benedict, you start. >> Uh so I think one question, if we talk about concrete security and security losses, what does even bit security mean for a proof of knowledge? I mean, for a sound proof, I can totally see like you

look at the adversary runtime, the adversary success probability, you take a quotient minus log of that, whatever. But now you have a you have another dimension if you look at proofs of knowledge because you have the running time of the extractor. So what does it even mean if we say 128 bits of security? Is that while our extractor is running in time 2 to the 60 or while our extractor is running in time two or in or I don't know, it solves the halting problem, whatever. So that I think bit security is not a sufficient notion for the security of of a proof of knowledge. There's one more dimension to it.

>> I I think that So that's not specific to proofs of knowledge right? In general, a bit security um as a single figure, it doesn't make sense. It's actually a function based on the number of queries. >> I mean, there's one I think the implicit definition or some papers make it explicit is you take the maximum over all adversaries of the fraction of uh running time divided by success probability and you require that to be at most 2 to the minus kappa. So you would map Yes, you have two two values, but you map them to one. But now I'm saying you have three values and it's much less clear that how to map them to

one. >> Um So that the the stuff of mapping it to a single um bit security level is not helpful. Um so you have several audiences. You have an expert audience that um understands what an advantage function is and you just give the advantage function. Right? Um regardless of how many parameters it has, how many inputs it has. You can just give the function. Um then you have to explain that to um a more general audience and I still don't think that um giving a single bit security figure is helpful there.

Um you basically cuz >> I mean, you are forgetting information. That's that's obvious. You map two two values to a single value, right? >> Right. >> But uh I what all that I wanted to say is that for this, if we can all agree on what bit security is, then I think we still don't agree on what bit security is for knowledge sound is because there's just one more dimension. >> Or or even like uh forget about the number of the single number. What is our definition of like being concretely secure? >> Yeah, exactly.

>> Yeah. I I encourage people to look at the Iron Wood book because um we had to um that's uh zcash.github.io/ironwood. Um so, we had to kind of explain what we'd proven. Um um we only managed to explain it to an expert audience, I think. Um but it's Yeah. We we had to go through that exercise. Um it was hard to um the the AI just got it completely wrong um and did a very poor job of explaining it. So, it took a lot of effort.

>> So, Benedict, this is I I I think interesting in theory. In practice, though, uh I think the extractors I've seen recently have been straight line and extremely efficient. So, it it Oh, okay. So, fair. I I Well, I was going to ask you, can you point me to an interesting but extremely inefficient extractor? But, um maybe it in cases of recursion is where you would find that. With the the extractors you know are what? Are >> But, these are kind of like >> Oh, in the Oh, okay. In the recur- in the case of recursion.

>> like the not explicit extractors. We're kind of like uh we build explicit extractors in the ROM. Then we are assuming they transfer like into the real world without like it's an assumption, so we don't I can't tell you what the extractor does. But, it inherently has to run uh not be straight line. So, it's an assumption that I haven't actually constructed. I'm assuming that it exists and it inherently cannot be straight line. Yeah. Because we we are moving from the ROM to a plain model in order to do recursion. So, in the ROM we had the straight line extractor. Now, in order to do recursion we have to sort of move either to an idealized model or uh lose that. So, it's it's very annoying. It don't please.

>> [cough] >> So, I want to give [clears throat] like a uh a small warning, okay? And relates to what Benedict said about this domain separation. So, suppose I have a scheme and I have and the runtime of the extractor is is the same, okay? Somehow we solve that. >> Mhm. >> We still have like a knowledge error. Okay? So, I have a scheme has knowledge error, let's call it epsilon one. And then I do, let's say, one recursion, okay? So, my new recursion has also a knowledge error of epsilon two. And then you can ask, okay, what is the error of this entire step? Is it the max of epsilon one and epsilon two, or is it the sum? Okay. And what Benedict uh suggested is kind of doing domain separation and making sure that somehow

when we analyze this, we get the max and not the sum. And I just want to say that even if this epsilon eyes are like exponentially small, if it is the sum, there is some risk. What is the risk? So, even if the error is very, very small, the adversary can come up with a proof that he did recursion two to the 100 times. Okay? Even though he didn't really do it. But he can kind of jump straight as if he is proving your statement that is on depth two to the 100 or 200. And that's because the error now accumulated is so big that he can actually break it. And he just give you a proof of a false statement that is of

depth two to the 100 without actually going and doing it. >> Yes, you could cap it you would like whatever you cap at where you would >> So, now you have to cap things. >> You cap it and then you do something. >> Okay, so you maybe you lose 30 bits of security. That's also not good. So, uh >> Right. >> Right. And you you don't want adversary jumping directly to the last uh >> And um I don't know like what's the status if we do the domain separation then we're happy with the thinking of the max or I don't know. >> Yeah, the analysis should prove that it's the max really. But uh >> Benedict?

>> I just wanted to answer that question. I mean for for recursion, I think the status is we don't know because we don't have a good proof for recursion, right? This this domain separation thing, this works intuitively in the random oracle model, right? Because you split the query budget. But recursion in the random oracle model is weird. So, the reason why where the the point where we have a proof that it's the max is when we go over multiple rounds in a multi round protocol where we do domain separation. And there it's the max.

>> Right. >> And that's why my intuition is that if you do domain separation, which I'm not sure if practical systems are doing, then you should also have a max there. >> this sort of from my perspective all goes into like um heuristic B saying that the the the fact that there is no loss uh is really counting for that. Adam. >> I I still think of that as a start starting point, not saying end point. Starting point to answer some of these questions and see how they behave. I would look at assigned oracle. >> Mhm. >> It just seems to be representative of some of the questions they were asking.

And if the analysis shows that, you know, with domain separation cuz you you know, there's different levels of how detailed and how greedy you want to be in uh the the the the the the bound you expect to get out of it. Like the max question, you know, will be like should be like a tighter bound and you will have to make sure that your candidate construction you're looking at has all the important domain separations. At least you know what those are, right? Uh cuz you can get lost in domain separation land like a what exactly are you putting into the tag right? A- and if you do that, then at least you have some starting point from which you can then understand, okay, like uh this idealized model like what does it not capture? Uh but it captures some things, right? And give you some

actionable points for implementation, right? That you know, then go back to implementation and say, "Are we at least doing the things that are informed by this idealized analysis?" >> one of the things that I view as a sanity check and I'm all for uh starting point. >> Just a quick question on the sign ROM. Should Should or could we call it just a verifiable ROM? >> Yeah, it's just Yeah. >> Okay, okay. There was also this recent paper where they used like a VRF to instantiate Fiat-Shamir. >> Yeah, I haven't thought about what's the right way what is the most like informative or useful way for our purposes to to make a ROM verifiable. You do have to keep track of, you know, concrete security, the size of the

these type of things. >> Yeah. >> But generally, anything that allows you to have a verifier circuits without oracle calls. >> Mhm. >> [clears throat] >> Yeah. Yeah. So, so there's a paper security bounds for proof of carrying data from straight-line extractors. Um I I Alessandro, I think you're one of the authors. So, >> I think so. >> Yeah. >> [laughter] >> Um so, I'm unclear on how much of the problem that paper solves. Um can you summarize that? >> It It It's a again, starting point, right?

>> [laughter] >> 15%. >> Okay. >> No, I mean, look, it's uh that's that's the these questions of like, you know, what is the concrete security of recursion? If we could analyze it, that's exactly what motivated that paper. So, the In that paper, there is a model that allowed us to analyze it so to have some initial answers, right? Because if even when you forward all the oracle calls, unexpected things happen, then or you cannot control the bounds like you wanted them to be controlled, then of course, in the plain model, you will have that and more, right? So, there it was just to at least to say, can we make sure that we can have highly

controlled, very good bounds in this particularly kind of um uh I is particularly ideal idealized model, right? And you can start from this particularly idealized one and make it slightly less ideal, right? And see, you know, how far down you can go while maintaining these good bounds. >> Okay. So, what was the idealization? Can you recap? >> Yeah, so here we changed the construction. So, to make sure that you can recurse, the circuit that you're proving no longer has oracle gates.

Which means that where are you going to put them? You just stash them in the proof. So, you intuitively it's like as if you have the SNARK that we use in practice and separately there's like a second part of the proof that is just all the claims and answers that are forwarded. And as you go into the recursion, you pick up more and more query answer pairs that were that cannot be checked along the way. So, you just kind of accumulate not accumulate, sorry. You you kind of uh a- accrete them through this the recursion right? >> That seems fine to me.

I would deploy a system based on that. >> Okay. I don't I don't want to sell that paper short. I think we learned something from it. Okay? Uh but there is maybe more to be done in in that direction. Okay? >> Maybe a last comment if Juan did you want to or Okay. >> Maybe it should have been for the first comment as a like as a practitioner in the ZK VM, I I I want soundness, but I don't necessarily need the knowledge soundness because I get the input for the deterministic computations. I can run it like >> [laughter] >> Uh you really need to quit here it. I mean, maybe the proof of soundness depends on

the knowledge soundness and maybe So, you understand. So, okay. >> I think even for >> We totally need it. >> I think even for the way we want to use ZK VMs in Ethereum because you you want to use them to compress certain things. Let's say I don't know, the the state proofs. You don't want everyone to download them. So, you essentially make the compu- computation even though if you look at it, it's a deterministic thing, but you want to compress certain things. So, you move them into the witness and then becomes non-deterministic computation.

>> I see. Yeah, I'm I'm I'm I'm I'm I'm not touching anything compressed yet. Maybe that's why, but in other parts of Ethereum, yes. Okay. >> Yeah, I I would have loved that to just care about soundness, which is what I usually work with. >> Actually, on that note, so if you only care about soundness, then you can use recursion and have an totally inefficient extractor. It still implies soundness. So, all of like you still have the knowledge error accumulating in your bound for soundness, but the running time of the extractor at that point is not relevant.

So, you can do poorly depth. >> [clears throat] >> I don't think I care about that. >> Okay, on that Sorry, small silly point. The on on that paper that I just mentioned we My memory fails me like but at the time we we did consider Oh, what if we put domain separation, right? Like how does the bound get better? Um in the end, I don't know. We ran out of uh you know, steam on that one. Other things to do. But Yeah, so we didn't So, there is a to-do there, which is to see is there a suitable setup of domain separation even in that idealized model that that

yields improvements. Okay, that that that Yeah. And uh some silly attempts did not work. >> So, the counting currently in the paper is kind of like a that it adds up. >> Yes. >> Okay. Okay, I think on that note uh maybe uh let's end here and continue to lunch. Thank you, everyone. >> [applause]