Fiat-Shamir

Transcript

Today I want to tell you about some, you know, work that they we've done. So, as an example, I will be using the royal we for like this talk because otherwise I'm unfortunately I'm wired that way. And so, I will continue with that. And today I'm going to do something a bit different from the other talks. I'll talk about some limitation of Fiat-Shamir, some cases where like some heuristic that we use fails in practice. And one relatively simple attack that that we found recently. So, this is we're going to go afterwards into like a talk a workshop on recursion. So, I think that having this in the back of the mind is kind of like the possible things where our theoretical modeling has gaps should be like a good segue into that.

Good. So, let me tell you a bit about what Fiat-Shamir is. Uh I assume that we don't really, you know, need to explain too much, but overall is a way that we can take an interactive protocol, which tend to be very easy to design and easy to analyze under an information theoretical like framework, and then turn it into a non-interactive protocol. The reason we want to do it because typically interaction is expensive. If you want to interact, the prover has to interact with each verifier that wants to verify the thing. While once you're able to remove interactivity, things are nice.

And Fiat-Shamir heuristic has been exceedingly successful. It's behind like, you know, proof system that we kind of love, signatures and almost uh yeah, it's been it's found like an extremely wide amount of applications. And when you do Fiat-Shamir, you're able to get something which is probably secure in the in idealized models such as the random oracle model. So, for this talk, what I'm going to be talking about is one variant of Fiat-Shamir, which is the strong Fiat-Shamir.

What do I mean here is that in this Fiat-Shamir, like the the transcript uses this following thing. So when I'm taking an interactive protocol of this form to turn into a non-interactive protocol to derive the first verify message, I'm going to hash the instance and the first message to the prover. And then to to get the second verify message, I'm going to hash the instance and the two messages. This is not how Fiat-Shamir is done in practice. In fact, it is more conservative that what is done in practice.

I'm just assuming that I'm going to do the most the most conservative thing because it's an attack. So this gives me a stronger result. This is very important because if you don't put the instance, we know that Fiat-Shamir is this is the weak Fiat-Shamir transform. This doesn't give you like adaptive security and it has created, you know, many many soundness issues and uh bugs in practice. So I'm but for me, I'm actually going to work about the real Fiat-Shamir, the strong Fiat-Shamir. So as long as your IP has got like some strong properties such as state restoration soundness, which are satisfied by most uh protocols that we care about, you can

actually prove that when you compile this thing, you get something secure in the random oracle model. Of course, you know, we do not have a random oracle. We don't have like a magic block in the sky which gives you random answers. So typically what the heuristic is is that you you can replace it with a un-sufficiently secure hash function. So I wouldn't be giving this talk if this were a false it weren't like a heuristic which is somewhat dangerous. And this is something that we known for a long time. So in particular, the first works on showing that the random oracle heuristic were you know, a heuristic which can fail in practice was by this

beautiful work by Goldwasser and Kalai. Here I give you like a simple sketch of it. So, this is a way in which we can design a protocol which interactively has extremely good soundness, 2 to the minus lambda in fact, which is great, but then when you instantiate it in practice, you actually get something which is completely insecure. And I want to some of the things that we're going to see are these topics of recursion and going to lead very well into the rest of the talk. So, I just want to go and kind of refresh your mind.

So, I have a prover and a verifier. And my protocol is going to be for the empty language. So, for the empty language, there's no valid instances. So, whenever the verifier accept, I broken soundness. So, what's going to be the protocol? Well, the prover is just going to send like a message. This message is going to be thought about as some code, some like, you know, some specification of a program. The verifier is going to sample a random like a random like bit string of lambda bits.

And the verifier will accept if you when you take M, you interpret it as a program, and you run it on itself, you actually manage to hit the the R that the verifier has sampled at random. Okay, why would you ever do this? You would never do this. It's extremely contrived, but here we would just want to find a way in which Fischl Meer fails. And you can see that, you know, in the interactive model, this is very sound because, you know, M to M applied to M is just a value. And when I sample an independent random value, the probability that I hit that value is kind of like is is 1 over 2 to the lambda.

So, my interactive soundness is 2 to the minus lambda. You can compile it in the random oracle. This is, you know, it's a one-round protocol, so it is state restoration sound, and you get like roughly the terror bound against any adversary which makes you queries. Okay, let's move on the other side of the slide. Now, here I've applied the strong Fiat-Shamir to this protocol and this is what it becomes like. And now the attack is what I've you know, now I choose a concrete hash function, something that I have the code of it.

And now if I apply like the if I look at the verifier, well, now R by our Fiat-Shamir is defined is the hash of its own description. And now so the the attack is that tautology. So now I've been able to break this with probability one. So by using the code of the hash function in a in a non-black-box way, I'm able to actually break the soundness of the protocol system. Uh of course this is extremely contrived. So the prevailing heuristic for a very long time was that you know look, yes, you can make Fiat-Shamir fail in practice, but it is you know, just because

you know, you are trying very hard to design places where Fiat-Shamir failed in practice. So surely surely for protocols that we actually care about this is fine. Well, spoiler, it was not. So like there are some cases where you can like think about protocols which are very natural and I'm going to talk about one of them. And but similar types of diagonalization apply. So this in particular is a beautiful work by you know, Ron, Dimitri and Lev. And the protocol that I want to talk about is the this combination of two building blocks that we care and love about.

A polynomial commitment scheme and the GKR protocol. So let me describe what this protocol does and so what I'm the protocol does is that I am trying to prove some circuit evaluation. So I have some circuit C. This circuit is passed through an indexer to get like some short uh this of it. This is typically done for very far efficiency. And uh I want to prove that the there exists some witness such that the circuit that W gets you some Y. The protocol is the following.

The prover takes the witness, commits it to it with a polynomial commitment scheme. Every protocol that we know about basically does this as the first step of their thing. And then we run the GKR protocol. It's not too important what the GKR protocol is. We only will need two properties of it. The first property is that uh the GKR reduces like the validity of the circuit evaluation to a multilinear claim about the witness and a multilinear claim about the uh the output layer of the circuit.

So, this is a a multilinear extension of Y. The second property I'm going to tell you about later. Okay, so at the end of this interaction, you have like some claim about the witness, some multilinear claim about the witness. But luckily we are in a world where we're playing with PCSs, so I can just uh apply the PCS to open it. >> Uh what is brackets? What is C in brackets? What is that? >> Uh good. So, this is a a digest of the circuit. >> Okay. >> Think about it like like some preprocessing information that the verifier has. Uh yeah.

And typically when I put things into brackets, they're either commitments or code, depends on how I felt on the slide. Um good. So, you can take this protocol and for a sensible PCS, this you can show it's run around sound, knowledge soundness, it's got like all the property that you might want to do. And this was actually deployed in practice. There are like some few protocols, in particular I think Polyhedra, that were using variants of this protocol very similar to this. Now, I'm going to show you that I I'm not going to show you I'm going to tell you how they showed that this protocol actually has problems in practice.

So, I'm going to again pick H to be some concrete hash function. And now I'm going to use the freedom that I have in choosing the circuit. And I'm going to choose a kind of like annoying circuit, but I'm allowed to do that because what I'm trying to do in this case is I'm trying to find counter examples. And the circuit is something that the prover adversarially can choose. It is not you know, it is not something that's fixed a priori, but it's something that the prover has control over it. So, the circuit will do the following.

So, the circuit will first commit to So, okay, the circuit gets a witness as an input. And the first step of the circuit will be to commit to the witness. So, this is the first step of the of the prover. After it, well, I'm going to use my circuit and um Yes, I'm going to use my circuit to um Sorry, this should be Y prime, I think. Uh to co- in the circuit I'm going to compute the first uh the randomness that the Fiat-Shamir would compute. So, this is the Fiat-Shamir hash.

And then the output of the circuit will be any like output that I think you know, that is distinct from the claimed output from this Y, but which agrees with it at the multilinear extension. And here I can always find it. Like it's kind of like I you know, uh the multilinear extension is compressing, so I can find some two string which have like which are different, but which have at a given point have the same multilinear extension. Because here I'm changing like the the order of things. I'm not sampling the point after things are fixed and fixing the things once I chosen the point.

Okay. Now, uh say that I have like uh okay, so this is the circuit. So, this is the fact that I can compute the initial steps of the of the um the system in the circuit is what going to allow it to do it. And one of the property that we need is that actually GKR does not have this very desirable property that you don't need to commit to the internal wires of the circuit. You only commit to the input and the output. So, what happened within the circuit in a certain sense is flexibility that does not go in the Fiat-Shamir transcript.

So, this is what the goes there. So, when you run this with this particular witness, you get like a claim where like the uh the um what's it called? Where the you get an invalid claim, but then since the uh since this this identity is true, actually the claim the initial claim about GKR will be true. So, when you're running honestly the GKR MPCs, you actually succeed with probability one. So, whenever you have like a sufficiently low depth like hash function and commitment that you can compute within this GKR circuit, this turns out to just completely break soundness.

There's a you you have a I saw >> Yeah, I I think I don't understand the So, the the verifier sent Oh. >> Yeah, so I'm trying to understand the basic uh pro pro interactive protocol even. So, the Okay, the prover commits to the witness. Uh they both have the verifier has digest of the circuit. Now, the verifier is sending some random R. And now you they run GKR, but exactly on on what uh do do they run GKR? I mean the doesn't the prover need to say what what is the out output he's claiming before they run GKR like what >> the output is this is Y.

>> Oh. >> to the to the to the prover. >> But but okay, but what is R R is just not being used for anything? What is >> R I'm just putting it here because it is the Fiat-Shamir challenge, the first Fiat-Shamir challenge. >> Yeah, but in the protocol what what is R verifier sending R? What is the prover doing with this R like nothing or >> Well, you R will be like the So when I do the when I start running GKR, right? I'm basically creating an MLE claim about the either first or last layer of the circuit. I don't remember right now. And from there like I'm going to slowly reduce claims to the MLE.

So this R is the first challenge which determines the first claim of GKR. It and it's a claim will be a claim on Y. So basically I'm arithmetizing the last layer of the circuit. At this tension it should be equal to the extension of of Y at R. >> Okay. Okay. >> And it is it's not too important for the detail but I just wanted to have it as the first challenge. >> Okay. Okay. >> But good. So we don't have too much time so I'll go. >> Yeah. >> Okay. My point is Yes, even for like honest protocols and protocol people might design Fiat-Shamir can be insecure.

But you know, but this is GKR, you know. You know, most people don't use GKR we use like, you know, R1CS based things and all of this. So surely in the same way like, you know, this you know, we're really using the fact that we are not committing to these to these witnesses. So surely it is fine. So what in this talk I'm going to show is some protocol that for different classes of computation like a circuit computation which have some contrived elements in them. I will advertise that there but are, you know, let's call them tantalizingly close to practice.

So, go cool. So, I'm going to tell you a bit about something funky. I'll tell you about generator relations. So, what's a generator relation? Well, it's a generic transformation I can do to any like relation that I care about. So, I can take my favorite relation think R1CS and say like, "Look, my instance edges actually will be generated by running a program." So, my new instance of the new relation is a program. I also give it like a time bound for complexity theoretical reasons but, you know, it's not too important.

And I'm running the program for uh some steps to get an instance and then I check whether this is witness with this instance witness parity in the relation. And it's a it's quite good enough. So, first of all, you know, M is a unique you know, uniquely determines I had so because the execution for me is deterministic. If the initial relation is NP-complete, so is the generator relation.

And I also would argue that this is something that is not too far off to modeling thing that we do in practice. So, for example, when I'm actually writing R1CS, nobody ever writes R1CS by hand nowadays. You typically have some kind of like DSL of some sort. Then you run it through a compiler which, you know, mhm looks at this code and does something out of it to generate the ABC matrices of R1CS. So, I am like you know, this is not too far off from what's happening in practice.

And also sometime we even just take some spec which also is called specifying what we want to prove and we feed it into like this you know 500 billion parameter like black box which does the magic things. You know. Can I say that this is not doing that inside? I don't think I can. But so this is why I think these are somewhat reasonable things. And I'm also going to give you a case where, you know, other disclaimer this was not vulnerable in practice but it was because of an excessive question by the designer which managed to like avoid this this this attack.

So this is about proof kit. Remco talked about it. And it is this case where you do trying to client side proving. And you typically have like this application repository where people can load programs that they care about. And the programs are written in like Noir as far as I can tell. This was Noir at the time. I don't know if it is still still in Noir. And when prover and verifier want to interact they download from the repository this circuit.

They run it through the Mavros compiler which is this compiler which turns it into R1CS. Both prover and verifier do it and then the prover proves the A A B and C over there. So yes. So if you just define a Mavros M to just be the execution map that we saw in the in the previous slide, this is exactly a generator relation. Okay. So this is why I think this is a somewhat reasonable model to look at. And here's basically the all attack idea.

The all attack idea is that even though even though like X is a uniquely uniquely determined what they sorry they even though the instance of the generator relation which is the program uniquely determines what the matrices are there is a gap between like the what determines the value and what is the semantic value of the relation. And by what I mean by semantic here is what makes the relation true. So, for example, in R1CS, A, B, and C is what determine the semantic value of it. And even though the instance is a uniquely determines this, it is not syntactically the same thing. It's a different thing.

So, what we're going to do, we're going to use this mismatch, sorry, yes. >> Yeah, but why? >> [laughter] >> Sorry? >> Why to hash the first? >> Well, because uh first of all, it might be even cheaper. It might be like shorter. Like there's a you know, but it's also So, this is a contrived thing, but also I argue I could argue that you know, maybe for R1CS, for all that I know, for competitive theoretic reasons, A, B, and C, maybe they're not the real semantic value of R1CS. Maybe there's a different semantic value that is I could still try to find this gap for.

It's kind of like uh you know, I don't believe this is true for a second, but I you know, I think theoretically there's some interesting there's some these these kind of gaps between what makes a relation true and what determines the relations, I think is something where you can squeeze in a lot of attacks, but I can talk about it a bit more later. Okay. So, we have this gap, and the the way that we're going to exploit it is we're going to find some malicious statement uh which which program can output a statement uh which depends on the value of the Fiat-Shamir hash.

This is going to be our whole strategy. Okay. So, it turns out there's actually something called the Kleene's recursion theorem. You can find all of this. So, basically, if I get any program F, you can find like some you can basically find a fixed point of it. So, I can find some program S star that when I evaluate S star, I get the value of F on S star. So, this is uh this is uh basically, it's what they call a quining programming languages. And whenever you have like a programming languages which is sufficiently powerful for you're able to do this thing.

So, this is the first trick that we're going to do. And spoiler alert, F will be the the Fiat-Shamir hash. So, we're going to try to find a program which computes its own Fiat-Shamir hash. Second of it, this is uh maybe too formal for this, but I want to think about proof system which have this property, which is called a delayed statement choice. Okay, so, first of all, I what I want for a proof system and what happens in the cases that the case study that I was talking about is that the verifier depends on the semantic value of the relation rather than on on the instance.

So, if I have an X which generate a fear, I think, then the the decision only depends on this value and not on the instance. So, for example, if I have a proof system like uh for a 1-CS, it depends only on the matrices, but not on the program that was uh And here I'm talking at the interactive protocol level, not before I do any hashes. And second, I want this second property that if I you know, if I have an instance and I see all the randomness of the proof system or some part of the randomness of the proof systems, I can come up with like one bad verify which is unsatisfiable.

But for which the verifier steps. Again, this is probably too formal. I'm going to give you an example in like the next slide, I think. But once I have this notation, basically the attack is very clear. So, I I'm going to define my map to be the to be this bind map. Then I'm going to apply a fixed point so that the I find like a fixed point of this map which actually will allow me to find a program which outputs a semantically invalid instance but which will verify under my proof system.

And then I get you know, profit, I guess. Okay, good. Let me give you like an example. So, I'm going to just take this this thing. So, if you this is the standard Spartan inspired, let's call it multilinear IOP for generator 1CS. So, I'm basically I have my input program M. I both prover and verifier run it to get their 1CS matrices. And once I have that, I first I send a commitment to the proof the honest prover sends a commitment to the witness.

The verifier samples some R which does a zero check. You run a sum check protocol. You batch all the things together and then you do a lean check with your favorite PCS. This is the whole protocol. And you know, and this is in a sense if you look at the case study, this is if I had the ABC to be derived from like for example the Marbles compiler, this would be exactly what would be happening in practice. Okay so there's plenty of protocols that just kind of follow this pattern.

So, this is I'm not pulling your leg. This is just, you know, the way that you would prove an R1CS statement nowadays. >> Shouldn't mu ABC be in the lin check? Uh >> Uh no, so mu A A and ABC are the values of AZ after the sum check, BZ after the sum check, CZ. So, the the the verifier just checks, you know, EQ alpha beta mu A B. Yeah. >> Yeah, but so they're in V, I guess. Okay.

>> Exactly. Well, I mean, the V is the claim of this thing. Okay. And I'm going to show you that this is actually kind of easy to to attack this as the latest statement choice. So, so basically, if I can predict what R1 is, what the first the challenge is, I can set up the following like the following R1CS system. So, basically, I'm just going to set I'm going to set A B and zero because I don't need them. I'm going to set C to just have two rows that will cancel each other when I scale them by alpha.

A by three by R1. So, basically, this the instance I can give is invalid because you need um you you basically Yeah, one row will have a constraint of zero and one row will have a constraint of one. So, this is an unsatisfiable instance. But, if I know that the zero check is going to use R1 actually for the R1 for the for its randomness, actually the the zero check claim, the one this claim here, will actually be a true claim.

So, when I run the rest of the protocol, you know, it's a true claim, so the protocol is perfectly complete, so things will just work out. Yeah, so this is basically the whole idea of the attack. So, once I know this, and since I have like uh um this verifier is semantic, and the reason why it's semantic is because after the first derivation step, I don't depend on M in any way. So, this plus the equalization directly gives you the attack. And you can, you know, you can implement this in Python which I mean, somebody can implement it in Python. I didn't implement it in Python. Somebody else helpfully implemented it in Python for me.

Uh and you can actually, you know, generate like this a statement with this with this thing, you can run the recursion. It is actually kind of cheap and you can show that you have like a uh you have like an unsatisfiable instance but which anyways accept uh we you can get it accepted with probability one. Okay. Again, there's a lot of very contrived things in this attack. I don't want to claim that this breaks anything in practice but I think there's some Ah, okay. I thought I had a slide. Okay.

So, you can also mitigate it very easily if you actually you know, hash the ABC matrices you can actually show that the protocol is as secure as the as the the as the corresponding R1CS protocol that you would have. Of course, this might also be insecure because we don't know the Fiat-Shamir is is secure, but you know, at least it is as secure as that one. So, in an excess of caution, just hash more is maybe is maybe the mitigation for this.

But what I there's other mitigation, you can, you know, if the adversary is not allowed to submit programs that he wants to prove, then it's harder for this attack to actually work. You can the extended Fiat-Shamir by Gal and Alone actually also prevents this attack. I don't have a proof that it It but it uh it seems in practice to prevent this attack. Uh also I want to say that uh R1CS was just as a simple case study. Basically, you can mount similar attacks to whatever you want. You can actually you can even make it work on the KVMs or you know, if you want you can do Schnorr as well.

It's a very contrived version of Schnorr, but you can do it. But what I find it interesting is that this seems to be like to me something which shows some limitation on our ability to theoretically prove things about Fiat-Shamir. So, this delayed proof So, the for me the most important part is part two. It's kind of like as a competitive theorist, I think that every NP-complete problem is the same. That if I have like, you know, uh R and R prime and are both NP-complete, things are kind of the same.

In this case, we have some sort of like generated relation which have a hard to distinguish from like just kind of like looking at them uh between each other, but one of them seems to be much much harder to protect Fiat-Shamir against. So, what seems to be to So, they are to me to suggest is that we want some tools which allow us to tell when a relation is some sort of recursive uh version inside of it which make it might make it harder for Fiat-Shamir to be proven with respect to it. Like for example, I don't think that I can mount anything similar to this with R1CS because I don't have the generality.

But both R1CS and generated R1CS are just NP-complete relations. How do I tell them apart? Um There's also kind of like, you know, maybe you know, these protocols where you are Maybe there are protocols where even if you see all the randomness, you're not able to generate a false instance. I don't know. I don't know any of them. I think all of them that I know are not in this case. So, I think it's very interesting to see whether there's some contrived protocol which are able to avoid this kind of attacks. And then of course, uh you know, another uh you know, the attack that we showed also shows some I guess technically some lower bound on collision resistance

hashing because you need on collision in collision intractable hashing. So, you because you need to have your collision intractable hash be strong enough to be able to prevent this attack. So, it cannot be computed within the program that you're doing. So, in the same way that like the KRS attack showed some uh limitation for like low depthness of uh correlation intractable hash functions, this also shows some similar limitation. Great. So, yeah. This has been my talk. This has been like one way in which I think that uh Fiat-Shamir can fail in practice. I think again, I want to stress, I think it is close to what practically deployed systems have done, but it is not currently as far as I could tell and as

far as what uh models were able to tell me before they I got cyber banned, uh this did not affect anything in practice. Okay. Thank you. >> [applause] >> Okay. So, so I have a setting in which this might apply and the proposed mitigation and um the my question is is the proposed mitigation sufficient? So, let's say you have a blockchain with smart contracts where um you allow people to um check arbitrary um circuits in some

arithmetization as part of your smart contract system. Um and obviously those circuits can compute um the um hash that's used for Fiat-Shamir because you know it in advance. Suppose you require the second description to be submitted and committed to on the blockchain, and then in a later block you use a seeded hash, and when the circuit was committed you kind of would have known that seed.

Is that sufficient to prevent the attack? >> Uh well, it definitely would prevent this particular attack I have. I cannot prove it would prevent other attacks. Like it feels like it would be cuz also I have some freedom as a prover to like when I'm proving the thing to feed in the witness, the seed that I now know. >> Yes, I see. Yeah. >> So that seemed like something that I could be should be able to get around with.

>> Good point. >> When you say hash the R1CS matrices, I I guess my question is kind of like in part of the model for exact or EXE, like if you use a restricted computational model to generate the R1CS matrices, it's like like if for example if you committed to the R1CS matrices and didn't include zeros or something. Like that that that like is a very limited form of computation, and so like where is the boundary there? >> I think that's a beautiful question.

Like I mean I think we talked with Remco about it at some point because in Prove It you also have like kind of like sparse encoding of the R1CS matrices, and then you deserialize, and this you know, it depends on the full matrix. It does not seem that you can do anything like this. I would be extremely surprised if you could, but uh you know, it's not exactly clear, you know, I think trying to prove that some deserialization functions of some sort do not allow you enough power to do this particular kind of tricks is hard.

>> I think specifically you want this thing to be like you want it to be less not really able to compute the hash. I see something that just like wipes out zeros. Blankly doesn't seem like something that can compute the hash. >> Even e >> Just this hash that comes in and serializes and deserializes and compresses in between means that you have semantics here. >> Because if you can com- if you have some sparcity, immediately means that you have generated and you your Feistel-Miyaguchi semantic. Because sparcity is is semantic.

>> But but there's a question of like how semantic it is. >> [snorts] [laughter] >> Yeah, yeah, of course you can imagine that for some are not sufficient semantic, but in general whenever you your R1CS is something beyond just pure random, it's immediately semantic. >> Yeah, another maybe example that I was thinking about is kind of like, you know, when you do say you're doing Schnorr and you have like some uh field element or group element you're sending over there. Sometimes you know, you have this this curve and you do like fancy thing, you do compression, maybe you do hash to curve, whatever fancy things.

They feel fine, but I don't know if they're fine. Like I think one thing that I'm kind of interested in in this figuring out, you know, if we have a criteria for like saying saying where something is really, you know, cannot compute a hash. Of course, I think to do to fully resolve this you have to resolve some sort of important computational complexity questions. Uh like, you know, possibly even P is equal to NP, I'm not exactly sure. Yeah, at the heuristic level like, you know, look, it's very hard to compute a hash if you're not trying to. >> Uh so if we kind of relax the requirements and and say um it should be possible to audit a circuit to um

to check that it's not exploiting this technique. Um the seeded hash um seems helpful there because you can say okay, that this um circuit is not using that seed. Um and that seems like a uh an easier thing to audit automatically than is it computing a hash. >> Yes, but there's also I think a similar Let me Sorry. Similar to like uh Ron's attack, there's also things you can try to do. Like for example, you know, what if I manage to get the prover to compute some of the things outside of the of the thing and then I just move them inside?

I can like >> Okay, it could be an input and it's not obvious that the input includes the the seed that or whatever. >> Exactly. Like there's not that much I can you know, once I get into it, there's like a lot of like kind of like tiny things that you can try to like uh move left and right to try to to get around attack. It's just very hard to fully be sure that things are there. Yeah. Yeah. Oh, yeah, yeah, no, absolutely. Yeah, yeah. I think it's undecidable to figure out whether a program computes a hash or not.

Yeah. >> Um so uh thanks for the talk. It's sort of fantastic and terrifying. Um so if I understand correctly, the the the attack is basically that the prover works out how to compute the first Fiat-Shamir challenge. And and it seems like the way you've got here is you have some sort of fixed point theorem about. So I guess my question is why does this fixed point theorem break if when you include the ABC matrices? >> Uh great because uh program cannot compute the hash of its own input.

Uh output, sorry. Output. I can compute like the hash of my code, but I cannot compute the hash of my output because the you know, to do that I have to kind of like find a fi- a fixed point in the hash. And and that seems to break uh most things. Any more? Yeah, I'm terrified about not too terrified. Yeah, just the right amount. Kind of like, you know, somebody used to say cryptographers seldom sleep well. I still get like my 8 hours.

>> So so what was the thing the overcautious thing that Worldcoin did to avoid this? >> They hash the ABC matrices. >> Oh, because I remember yesterday Remco saying they explicitly go to the trouble of not fully generating the matrices. So I >> Remco. >> Like I said, this is not implemented and it is actually pending on figuring out how to solve this particular problem. But one thing you could do is extract the matrices, hash them once the first time you see this circuit, and now you just store this hash. So it's not a huge issue to solve.

>> Right. You're going to be pre-processing the matrices anyways. So in that pre-processing you might as well keep also the hash. >> Right. >> Oh, okay. >> Because they they don't really care about verifier being super sensitive, I think. So you might as well not pre-process it and you save some lookups, I guess. But yeah, so yeah, so Proof kit is not actually vulnerable. It might eventually be. I don't know know like also other engineering will will go there, but yeah. At the time they were hashing the matrices even though they could have just hash the code.

This was really annoying because I think I would have done an amazing demo. Yeah. I thought about it, but I I had matched my weekly limit. So like you know, No, look around in a terrible thing terrible thing. So I think I'm going a list of AI lab will yeah, not work. Good. So, yeah, but I think yeah, if somebody has sometimes some tokens, I think it's like probably uh a fun thing to do cuz you also need to find like a Sorry?

I didn't I didn't want to suggest it, but if you you know, if you know, represent Well, then we might as well, you know, at this point. But Perfect. Yeah, so I think we should try this. I think it I think it'll be fun. Uh also, I think you need to find uh I also know 100% sure on this. I haven't checked. I think Noir is expressive enough to have fixed points, but uh I haven't checked, so this might be where things break. This I have to double-check. Great. Uh I don't know. Maybe we should start the other discussion. I think we might be late.

Uh so, I'm running out of motivating. >> [applause]