Fuzzing Zero-Knowledge Infrastructure by Valentin Wüstholz | Devcon SEA

[Music] 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 um let's have a short definition of what I understand by zero knowledge infrastructure so uh for this talk I'll um 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 uh dsls for describing ZK uh circuits or maybe in the future we'll also look at entire ZK EVMS so um with this out of the way um let's um look at why this is an important topic and why um 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 uh could have uh catastrophic financial and reputational uh impact and we should really make sure these components are as bulletproof as they can get um while we haven't seen a really catastrophic incident uh in this field may maybe perhaps uh comparable to the Dow hack in 2016 uh it's really important that um we have uh rigorous testing for these components and we use um you know the best ering uh discipline that we can um have right uh because these components are really complex and getting them right is is not easy so what is fuzzing I don't think I have to like explain this after the last uh talk but fuzzing is widely used in industry um for instance at Microsoft Google meta uh they're fuzzing a lot of their infrastructure uh to catch Buck before um hackers can actually exploit them in practice so in this talk I'll give you an overview of our fuzzer for um finding critical bugs in processing pipelines for zero knowledge circuits um the fuzzer is called Circus and it already supports four of these pipelines namely uh circum cor uh gar and Noir and there's you know like a a gazillion of different dsls popping up it seems like you walk around here and you see another one in the corner um and we've already found uh 16 bugs in total for the four uh pipelines we looked at um 15 have already been fixed so that kind of shows that these bugs are really uh taken seriously and um developers sometimes respond within hours to actually get them fixed um you can also see a kind of uh 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 uh pipelines so it's not like there's one pipeline that's you know responsible for all the bugs uh that we found um now kind of to make sure that everybody understands I mean like I yeah I assume not all people are aware of what these uh processing pipelines look like look like uh here's a short kind of summary um you can see in the sort of yellow box um there is a circuit that the user writes um that goes into the compiler and then the compiler um hands some output to the witness generator and the witness generator can then take the input so the you the user input uh to the circuit and generate a witness uh that can be then used by the prover and then theover generates a proof that can then be very verified to essentially check that the circuit was actually executed so um now that we have a bit of an understanding of how these pipelines look like let's uh dive a bit uh deeper to understand how we find these bugs so first I want to be very clear um we are not cryptographers this is not our uh this is not my background my background is in you know uh software security uh program analysis um and for this reason I can't really you know try to understand the the logic that's in the integrate log logic in many of these components um which is uh why we treat these essentially as a blackbox so much like what a typical user would do uh we just view them as a blackbox so how can we still find all these bugs right well first we have a lot of experience uh in testing uh complex or software for complex domains and building fuzzers for them so we've done quite a bit of work on uh fuzzing for smart contracts it's probably the work that's most closely to the audience that's here um and for instance we created the Harvey fuzzer um many years ago and we're still kind of maintaining it um we also did some work on ML models um and on on testing ml models and testing program analysis tools um yeah if you want to know more check out the papers that are um online um 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 um explaining in a bit more detail what metamorphic testing is let me just give you kind of a uh short summary of how we got here how we got into this uh interested in this topic um so we as I said we were um working on fuzzing for smart contracts mainly uh for many years and then at some point um I guess maybe like a year ago roughly um consensus they released the linear blockchain um that is one of the first ZK EVMS and we were like well this is really complex uh we started looking into it a bit um and we saw that there are these components like the Gnar library and and the corset language for um processing zero knowledge circuits so we were like oh what can we do to you know um test these what can we do to make sure that there no bugs in these components um and that's when we started building um kind of a predecessor to this fuzzer uh I'm presenting today uh which is called Rio um so the Rio is a fer for the Gnar Library specifically and then essentially this uh C ccus fuzzer I'm presenting today is essentially an evolution of this uh fuzzer that is a bit more General and can Target multiple um dsls all right now uh back to metamorphic testing so what is metamorphic testing um I think the shortest way to summarize it it's kind of a way to define test oracles uh in a pretty elegant and concise way so to illustrate I've um I've uh collected a few examples that um yeah explain this uh and try to um explain what metamorphic testing is so the first example is how to actually test that the Sorting function uh sort for an input let's say an array of integers X actually does the right thing well there's many ways to to check this but here's uh a way to check it um using metamorphic testing so you take you sort um the input X and then you also sort for uh X but you Shuffle it randomly right and these two um the output of both of these invocations of the function they should have the same output right so pretty nice and concise uh specification so let's look at another example uh here um we want to test um essentially some procedure for computing the shortest path in uh graph G between the nodes n and M so how can we do this this with metamorphic testing well one way to do it is to say you know the shortest path um between n and M in the graph G is less than uh the shortest path between n and n and n and M um in the graph where we take G but we remove uh some random Edge right because that edge might have been on the the shortest path and then the shortest path could become longer right so we can also do apply the same kind of principle to more complex uh components like a entire compiler right so here's an example of how to do this with metamorphic testing um 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 um the program P but you add some dead code somewhere randomly right and you compile it and you run it shouldn't matter right should give you the same output essentially so with this um let's look at how we can apply kind of the same reasoning principle to uh zero knowledge uh circuits so the fuzzer what it does is uh it first generates a random circuit uh 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 uh but semantically they should have uh the same behavior and now we the fuzzer generates an input I and um invokes the processing pipelines for both of these circuits um and if there's any difference in you know the output or the behavior then that's a bug somewhere in this processing pipeline so for instance um the for one circuit we might not be able to generate a witness but for the other one we would then there's probably a bar somewhere in the compiler or in the witness generator so um let's look at a few of these uh Transformations uh to kind of understand how the fuzzer does this um so here's a very simple transformation uh if you have somewhere in your circuit an expression e uh you can always apply um you can always multiply the expression by one right that should not change anything um or you can also divide by one again shouldn't have any effect on the circuits um another transformation is to basically negate the expression e twice or you can also apply other Transformations like um swapping um the two oper of a multiplication and then we also have um um 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 right that should again not have any effect um and we have a small DSL for describing these circuits so there's many more of these transform formations um So currently we support roughly 90 uh such rules but you can easily add more of them and think of new ones if you want like to so uh we also found a number of bugs in um the different uh pipelines and let's look at a few of them um just to kind of give you the the idea and show give you a concrete example um that you can look at so here on the left uh we see uh a small uh example circuit in in the circuit circum um language uh you can also look up the GitHub issue uh if you if you'd like to um but this essentially a minimized uh cleaned up um version of the circuit um and as you can see there's a variable P um in practice this is essentially just a constant uh just didn't fit on the on the slide so I um yeah put it at the bottom um 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 this circuit which is the one uh that's shown on the right and here it applies a number of um metamorphic Transformations so for instance it seems like the fuzer first um multiplied the expression P by one then subtracted Zero from one and then divided um that expression uh by one and when we execute this um when we execute these two circuit we can see that um that the output out one and out two actually are not the same so this is bad and this is was a bug that we found um seemed like there was a bug in the witness generation part um and here's another bug um that we found in gnark um so at the top you can again see the the original circuit that the fuzer generated and then we can also see the transform circuit um where the fuzzer essentially changed the expression zero to just zero or zero which should be um equivalent right and here um we observed that for C1 uh there was no witness that was generated uh whereas for C2 there was so this again is um a bar somewhere in this uh pipeline and yeah now that You' kind of hopefully got an overview of the of the tool and saw a bit how these bugs look like in practice um I hope more people will you know uh uh start looking into this problem uh because I think it's a it's a very important problem uh we need to really make sure that these components are uh bulletproof uh because otherwise you know pretty bad things can happen and it's better to do this before the some you know attacker does it right um and you don't need to be a cryptographer to actually find these bugs so you know that makes um gives us a lot more um people that can actually uh look into this um because I think so far we only really scratch the surface so there's more more things that need to be done to to test these components also there's components like this popping up um uh every now and then so we really need to uh make sure they're safe and we also should do um continuous fuzzing of all these components so for the gnark team we actually implemented a continuous fuzzing setup where you know they when they whenever they commit the latest version to master uh we we start a new fuzzing campaign uh we run for 24 hours we tell them if something is wrong and then the next day same thing happens um we're also planning to do the same for cors and if you're interested in um you know us uh taking a look at your uh ZK infrastructure uh please reach out and if you want to know more about uh what's going on in the fuzzer then please just check out our paper uh you can scan the QR code there um and if you you know want to let take a look um yeah fantastic thank you Val Valentine for this presentation um let's get to the question 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 voted so let's get 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 like do you identify where the bug exist within the circuit uh we don't directly identify where the bug is but when we generate the the test inputs like the circuits uh 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 um and yeah so far I think the complaint the the the developers very very happy with the bugs reported um and I think there was no issues finding the the bug once they had the the input makes sense thank you second question do you fuzz logical Expressions they're encoding in circuits uh yeah we do I think yeah so for instance we apply some you know some common uh Transformations like applying the Morgan's Rule and so on um so there's a bunch of um these Transformations that we that we use in the fuzer wonderful third where is the bug Nest where do bugs usually reside in your historical fuzing like from what you've seen um I think it's it's hard to like can you read derive U enough data from you found 17 yeah yeah I think it's yeah it's probably too early to say but we did observe that um the fer found bugs basically in um different components so we found bugs in the compilers we found bugs in the witness generator we found bugs in the approver as well I don't think we found bugs in the verifier seems like yeah that's kind of towards the end of the pipeline uh and I think many people are are you know very concerned about the you know getting the verifier right so maybe that's also paying off uh here um but we'll we'll keep trying um we'll yeah we'll see nice um okay when Kyo fuzzing um yeah we're I guess you insert it in your slide if we're interested people talk to you somebody from starware wants to you know uh us to look at more at CYO then yeah please please reach out um we're interested um it's definitely a a good idea to to do that yeah wonderful well I'll reach out um what do you think of concolic testing of Z circuits um I had to ask chat GPT what concolic testing is okay and I still don't understand it okay um yeah so concolic testing um essentially I mean for the audience maybe it's essentially a way to you know generate um new inputs by doing some kind of symbolic execution uh but basically for some Expressions that might be really complex like you have non nonlinear expressions in these circuits so there you might want to uh concretize some inputs um and that's a con concolic part so it's like concrete and symbolic um but yeah so the I think that's that's an interesting area it's not sort of what we focused on uh because we we're not so much interested in actually ating inputs for these uh circuits um that's something you would probably want to do if you want to have a specific circuit that you want to you know get right and you want to make sure it h satisfies some properties then you probably should think about you know concolic testing for that circuit um yeah perfect thank you how does it feel to find a bug it like literally when you find one is it is it scary is it exciting I mean you're looking for those so it's probably a bit exciting but it's also SEC there's probably money on the line how does it feel no it's definitely I mean it's definitely exciting um and I work a lot with students um and you know it it really you know they you can see they're they're excited when they find a bark uh they're happy they're making you know an impact um and also the reactions from the developers are a great motivation to find more bugs because usually they're very um yeah they have been very positive I don't believe you there there's no way you go to people and say Yeah I broke your and they're like oh yeah amazing yeah I mean if if if you're sort of yeah if you're um yeah L2 and one bug like this can you know wreck your system then yeah in some sense your 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 scary when I think about bugs I think like yes I want to fix them the first thing that comes to mind is like oh yes no but you're right it's better to be aware of FR than not okay we can actually take the last oh one seconds left let's wrap it up or do you want to are you using property based testing for choosing the input um we're I mean you can call it property based testing but we're generating the inputs right now uh completely randomly so it's kind of blackbox 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 um yeah fantastic thank you thank you Valentine thank you