Fork-Choice enforced Inclusion Lists (FOCIL)

Good morning everyone. So today I'll talk about fuzzing for zero knowledge infrastructure and this is joint work with my collaborators from the Technical University of Vienna. So just to kind of make sure we are all on the same page, let's have a short definition of what I understand by zero-knowledge infrastructure. So for this talk I'll define zero-knowledge infrastructure as software components that are used for compiling, executing, proving and verifying ZK circuits. So examples would be the processing pipelines that are commonly used by DSLs for describing ZK circuits or maybe in the future we'll also look at entire ZK EVMs.

So with this out of the way let's look at why this is an important topic and why more people should be doing this. Well first zero knowledge infrastructure is highly complex and highly critical. For instance it's used in several L2 chains so kind of bugs there could have catastrophic financial and reputational impact, and we should really make sure these components are as bulletproof as they can get. While we haven't seen a really catastrophic incident in this field, maybe perhaps comparable to the DAO hack in 2016, it's really important that we have rigorous testing for these components and we use, you know, the best engineering discipline that we can have, right? Because these components are really complex, and getting them right is not easy.

So what is fuzzing? I don't think I have to explain this after the last talk, but fuzzing is widely used in industry. For instance, at Microsoft, Google, Meta, they're fuzzing a lot of their infrastructure to catch bugs before hackers can actually exploit them in practice. So in this talk, I'll give you an overview of our fuzzer for finding critical bugs in processing pipelines for zero-knowledge circuits. The fuzz is called Circus, and it already supports four of these pipelines, namely Circum, Corsair, Gnark, and Noir.

And there's a gazillion of different DSLs popping up, it seems. Like you walk around here and you see another one in the corner. And we've already found 16 bugs in total for the four pipelines we looked at. 15 have already been fixed, so that kind of shows that these bugs are really taken seriously, and developers sometimes respond within hours to actually get them fixed. You can also see a kind of breakdown of the different bugs and where we found them.

And as you can see, they're kind of very evenly spread across the different pipelines, so it's not like there's one pipeline that's responsible for all the bugs that we found. Now, kind of to make sure that everybody understands, I assume not all people are aware of what these processing pipelines look like, here's a short summary. You can see in the yellow box, there is a circuit that the user writes that goes into the compiler, and then the compiler hands some output to the witness generator, and the witness generator can then take the input, so the user input to the circuit, and generate a witness that can be then used by the prover and then the prover generates a proof that can then be verified to essentially check that the circuit was actually executed. So now that we have a bit of an understanding of how these pipelines look like, let's dive a bit deeper to understand how we find these bugs. So first, I wanna be very clear, we are not cryptographers.

This is not my background. My background is in software security, program analysis. And for this reason, I can't really you know try to understand the the logic that's in the intricate logic in many of these components which is why we treat these essentially as a black box so much like what a typical user would do we just view them as a black box. So how can we still find all these bugs? Well first we have a lot of experience in testing complex software for complex domains and building fuzzers for them.

So we've done quite a bit of work on fuzzing for smart contracts. It's probably the work that's most closely to the audience that's here. And for instance, we created the Harvey fuzzer many years ago, and we're still kind of maintaining it. We also did some work on ML models and on testing ML models and testing program analysis tools. If you want to know more, check out the papers that are online.

And the second reason why we were able to find these bugs is that we have a not-so-secret weapon, which is called metamorphic testing. So before explaining in a bit more detail what metamorphic testing is, let me just give you kind of a short summary of how we got here, how we got into this, interested in this topic. So we were, as I said, we were working on fuzzing for smart contracts mainly for many years and then at some point I guess maybe like a year ago roughly, Consensys, they released the linear blockchain. That is one of the first ZK EVMs. And we were like, well, this is really complex.

We started looking into it a bit. And we saw that there are these components like the GNARC library and the Corsair language for processing zero knowledgeknowledge circuits. So we were like, oh, what can we do to test these? What can we do to make sure that there are no bugs in these components? And that's when we started building kind of a predecessor to this fuzzer I'm presenting today, which is called Rio.

So Rio is a fuzzer for the GNARC library, specifically. And then essentially this Circus fuzzer I'm presenting today is essentially an evolution of this fuzzer that is a bit more general and can target multiple DSLs. All right. Now back to metamorphic testing. So what is metamorphic testing?

I think the shortest way to summarize it, it's kind of a way to define test oracles in a pretty elegant and concise way. So to illustrate, I've collected a few examples that explain this and try to explain what metamorphic testing is. So the first example is how to actually test that the sorting function, sort for an input, let's say an array of integers x, actually does the right thing. Well there's many ways to check this, but here's a way to check it using metamorphic testing. So you sort the input x, and then you also sort x, but you shuffle it randomly.

And these two, the output of both of these invocations of the function, they should have the same output. So pretty nice and concise specification. So let's look at another example. Here, we want to test essentially some procedure for computing the shortest path in graph G between the nodes N and M. So how can we do this with metamorphic testing?

Well, one way to do it is to say, you know, the shortest path between n and m in the graph G is less than the shortest path between n and m in the graph where we take G but we remove some random edge, right? Because that edge might have been on the shortest path, and then the shortest path could become longer, right? So we can also apply the same kind of principle to more complex components, like an entire compiler, right? So here's an example of how to do this with metamorphic testing. When you take a program P and you compile it and then run it, you should essentially see the same behavior as when you take the program P, but you add some dead code somewhere randomly.

And you compile it and you run it. Shouldn't matter. It should give you the same output, essentially. So with this, let's look at how we can apply the same reasoning principle to zero-knowledge circuits. So the fuzzer, what it does is it first generates a random circuit, C1, and then it applies a random transformation to C1 to get a new circuit, C2.

So now we have two circuits that are essentially syntactically, perhaps completely different, but semantically they should have the same behavior. And now the fuzzle generates an input, I, and invokes the processing pipeline for both of these circuits. And if there's any difference in the output or the behavior, then that's a bug somewhere in this processing pipeline. So for instance, for one circuit, we might not be able to generate a witness. But for the other one, we would.

Then there's probably a bug somewhere in the compiler or in the witness generator. So let's look at a few of these transformations to kind of understand how the fuzzer does this. So here's a very simple transformation. If you have somewhere in your circuit an expression E, you can always multiply the expression by 1. That should not change anything.

Or you can also multiply the expression by one, right? That should not change anything. Or you can also divide by one. Again, shouldn't have any effect on the circuits. Another transformation is to basically negate the expression E twice.

Or you can also apply other transformations, like swapping the two operands of a multiplication. And then we also have some transformations that use essentially new randomly generated expressions. So here, for instance, we replace an expression e with e minus some random expression plus some random expression. That should, again, not have any effect. And we have a small DSL for describing these circuits, so there's many more of these transformations.

So currently we support roughly 90 such rules, but you can easily add more of them and think of new ones if you would like to. So we also found a number of bugs in the different pipelines, and let's look at a few of them just to kind of give you the idea and give you a concrete example that you can look at. So here on the left, we see a small example circuit in the circum language. You can also look up the GitHub issue if you'd like to. But this is actually a minimized, cleaned up version of the circuit.

And as you can see, there's a variable P. In practice, this is essentially just a constant. It just didn't fit on the slide. So I put it at the bottom. But think of P just as a normal constant in your program.

And now what the fuzzer does is it generates a transformation of this circuit, which is the one that's shown on the right. And here it applies a number of metamorphic transformations. So, for instance, it seems like the fuzzer first multiplied the expression P by 1, then subtracted 0 from 1, and then divided that expression by 1. And when we execute these two circuits, we can see that the output out 1 and out two actually are not the same. So this is bad and this was a bug that we found.

It seemed like there was a bug in the witness generation part. And here's another bug that we found in GNARK. So at the top you can again see the original circuit that the fuzzer generated. And then we can also see the transform circuit where the fuzzer essentially changed the expression zero to just zero or zero, which should be equivalent. And here, we observed that for C1, there was no witness that was generated, whereas for C2, there was.

So this, again, is a bug somewhere in this pipeline. And yeah, now that you've kind of hopefully got an overview of the tool and saw a bit how these bugs look like in practice, I hope more people will start looking into this problem, because I think it's a very important problem. We need to really make sure that these components are bulletproof, because otherwise pretty bad things can happen. And it's better to do this before some, you know, attacker does it, right? And you don't need to be a cryptographer to actually find these bugs.

So, you know, that gives us a lot more people that can actually look into this. Because I think so far we only really sketched the surface, so there's more things that need to be done to test these components. Also, there's components like this popping up every now and then. So we really need to make sure they're safe. And we also should do continuous fuzzing of all these components.

So for the Gnark team, we actually implemented a continuous fuzzing of all these components. So for the Gnark team, we actually implemented a continuous fuzzing setup, where whenever they commit the latest version to master, we start a new fuzzing campaign. We run for 24 hours. We tell them if something is wrong. And then the next day, same thing happens.

We're also planning to do the same for Corsair. And if you're interested in us taking a look at your ZK infrastructure, please reach out. And if you want to know more about what's going on in the fuzzer, then please check out our paper. You can scan the QR code there if you want to take a look. Yeah.

Fantastic. Thank you, Valentin, for this presentation. Let's get to the questions, shall we? Yeah. All right.

So I've sorted the questions. Again, you have a QR code here. You can ask your questions, and I'll ask the ones that are the most upvoted. So let's go to the first one. When you identify a bug, can you just say, hey, there's a bug, or do you provide a path to fix it?

Do you identify where the bug exists within the circuit? We don't directly identify where the bug is, but when we generate the test inputs, like the circuits, we try to minimize them. So we try to keep them as small as possible so the developers can really, hopefully quite easily identify where things go wrong. So far, I think the developers were very happy with the bugs reported. And I think there was no issues finding the bug once they had the input.

Makes sense. Thank you. Second question. Do you fuzz logical expressions during coding in circuits? Yeah, we do.

I think, yeah, so for instance, we apply some, you know, some common transformations like applying the Morgan's rule and so on. So there's a bunch of these transformations that we use in the fuzzer. Wonderful. Third, where is the bug nest? Where do bugs usually reside in your historical fuzzing, from what you've seen?

I think it's hard to... You really derive enough data from... You found 17, right? Yeah, yeah. I think it's probably too early to say, but we did observe that the fuzzer found bugs basically in different components.

So we found bugs in the compilers, we found bugs in the witness generator So we found bugs in the compilers. We found bugs in the witness generator. We found bugs in the prover as well. I don't think we found bugs in the verifier. It seems like, yeah, that's kind of towards the end of the pipeline.

And I think many people are very concerned about getting the verifier right. So maybe that's also paying off here. But we'll keep trying. We'll see. Nice.

Okay. When Cairo fuzzing? Yeah. I guess you answered it in your slide. If we're interested, people can talk to you.

If somebody from Starkware wants to look to look at more at Cairo, then yeah, please reach out. We're interested. It's definitely a good idea to do that, yeah. Wonderful. Well, I'll reach out.

What do you think of concolic testing of ZK circuits? I had to ask Chad GPT what concolic testing is. Okay. I still don't understand it. Okay.

Yeah, so concolic testing, essentially, I mean, for the audience, maybe it's essentially a way to, you know, generate new inputs by doing some kind of symbolic execution. But basically, for some expressions, that might be really complex. You have non-linear expressions in these circuits. So there, you might want to concretize some inputs. And that's the concolic part.

So it's concrete and symbolic. But yeah, so I think that's an interesting area. It's not what we focused on because we're not so much interested in actually generating inputs for these circuits. That's something you would probably want to do if you want to have a specific circuit that you want to get right and you want to make sure it satisfies some properties, then you probably should think about concordant testing for that circuit. Yeah.

Perfect. Thank you. How does it feel to find a bug? Like, literally, when you find one, is it scary? Is it exciting?

I mean, you're looking for those, so it's probably a bit exciting, but it's also scary. There's probably money on the line. How does it feel? No, it's definitely, I mean, it's definitely definitely exciting. I work a lot with students.

You can see they're excited when they find a bark. They're happy they're making an impact. And also the reactions from the developers are a great motivation to find more barks because usually they're very... Yeah, they have been very positive. I don't believe you.

There's no way you go to people and say, I broke your shit. And they're like, oh yeah, amazing. Yeah. I mean, if you're sort of... If you're...

Yeah, and L2 and one bug like this can wreck your system, then in some sense your job is also on the line. So you should... You want to find those bugs. I'm not saying you don't want to. It's just a theory.

When I think about bugs, I think like, yes, I want to fix them. But the first thing that comes to mind is like, oh, yes, no. But you're right. It's better to be aware of first than not. Okay, we can actually take the last...

Oh, one second's left. Let's wrap it up, or do you want to... Are you using property-based testing for choosing the input? I mean, you can call it property-based testing. We're generating the inputs right now completely randomly, so it's kind of black box fuzzing that we're doing.

And we're also considering to do more, you know, feedback-directed fuzzing, like you saw in the last talk. Yeah. Fantastic. Thank you, Valentin. Thank you.