Taxonomy of ZK bugs in Blockchain by Jon Stephens

foreign [Music] okay so I guess I'm gonna go ahead and start so hi my name is John and I'm going to be talking to you today about some bugs in ZK circuits so first let's just give a bit of an introduction of what a ZK circuit even is and kind of how it works and so basically the way that you develop a ZK circuit is you first write it in a particular language like circom or Halo 2. and then what that's going to do is it's going to Output two things it's going to output something called a witness generator which is going to perform some computation and then it's going to Output a set of constraints and these are the polynomial field equations and those in turn are going to be used by two things so the approver and the verifier and so the prover is going to prove that the computation was performed and the verifier is going to verify that proof and so really the source code contains uh two sets of things computation and constraints and that's the two things that we're going to be focusing on in this talk and so in this presentation I'm mainly going to be showing examples in circum so I thought it would be helpful to give you just a quick introduction of what circum even is and so here's an example circuit written in circum and as I told you before it's going to become two separate things so first you have computation over here on the left and you have constraints over here on the right and one thing that you might notice is that you know there the the template is being divided in a weird way into these two different things and so the reason why that is is because particular operations that you use within your circuit are either going to assign into your computation or your constraint and so in particular when you have an arrow with two dashes then that means that you're only going to be assigning into the computation whereas if you have an arrow with two equal signs that's going to be going into both and another important thing to know here is that you can't always assign to both because there are is a particular form that your constraints have to be in in order to go into that constraint part but eventually you decompose your circuit or the compiler decomposes your circuit into these two forms and then this is how the execution of the circuit ends up working so essentially your computation is going to take in your inputs it's going to compute your outputs and all of that gets kind of composed into this thing called a witness and so then that witness is going to go into your set of constraints and then your constraints are either going to say yes this is verified or no it isn't and so the goal of this is to produce a computation and a constraint that are equivalent and so I'm going to tell you what equivalent means but first i'm going to ask a question which is why do we care and so if you're wondering this hopefully I'll answer it now so basically the reason why we care is because in the past we've seen these equivalence bugs where basically the verifier so the constraints are going to accept bad inputs that they should not be accepting and so we've seen this in these cases right here where you know essentially these under constrained circuits or these equivalent bugs have led to potential thefts of funds and so that's the reason why we want to have a way of checking for these and we want to have a way of knowing what they are and so first let's go ahead and figure out what equivalence even means so I already talked a little bit before about the two parts of the circuit so you you have your computation that's going to take in an input X and it's going to output something Y and you're going to have a set of constraints and that's going to take in both your inputs and your outputs and eventually it's going to end up returning true or false and so really what you want to do is you want to solve this formula and so in particular you want to make sure that for every input and output of P it must be accepted by your constraints but also the only thing that is accepted by your constraints should be inputs and outputs produced by your computation and so in this talk we're going to look at ways in which we've seen this being violated uh in the wild and so first we're going to establish a taxonomy of these equivalence bugs so essentially you've got a ZK circuit and then we can decompose these bugs into a couple of different categories so first you can have completely unconstrained signals you can also have discrepancies between your constraints and computation and finally you can use sub-circuits in some unsafe way and so we're going to go into what each of these means and an important thing to note here is each of these can be decomposed into further subcategories and so I'm not going to go into extreme depth in all of these but I'll show an example of what these are and then if you want to know more information we have a paper that we're currently publishing about this so first I'm going to tell you about unconstrained signals so basically an unconstrained signal corresponds to a signal that is going to accept anything and so in this case there is absolutely no constraints on it and so we can decompose these bugs that use unconstrained signals into two different things so first of all you can have a completely unconstrained output which is bad because that means that uh essentially someone can assign anything that they want to that output or you might have an unconstrained public input and so we've seen cases like in I believe it was semaphore this has caused problems because you expect that your public inputs are going to be constrained by the proof in some way and if they aren't constrained then someone could possibly change those public inputs when the verifier is supposed to be checking them and so here as an example let's take a look at this circuit so essentially the problem that we have is right here and so what happens in this case is the developer intended to add two arrays and in this case they you know iterate over the array but they forget to iterate up until n minus one and so as a result they do not constrain that last element of the out array and so what this means is that out array is completely unconstrained and will accept any potential value within the verifier and so this is particularly bad based off of how this circuit ends up being used so an important thing to note here is that these circuits are often composed of sub-circuits and so in circum these are called components and in Halo 2 they're called something else it doesn't really matter but in either case they're essentially sub-circuits and so these sub-circuits often assume some information about how how they're going to be used so basically they often assume that you're going to end up constraining either the inputs or the outputs or both and if that is not actually performed then again that's another source for bugs and so these particular bugs correspond to to the cases where that sub-circuit is not actually being used correctly and so there are two particular cases that I've displayed here so for example you could use a sub-circuit however you might not constrain the output and similarly you might not constrain the input so let's take a look at this example so basically in this case someone has a circuit where they're trying to allow people to let's say withdraw funds so the first thing that they do is they perform some sort of range check which is great and then they check to make sure that the amount that someone is trying to withdraw is less than the balance however one thing that they did not do is they're missing a constraint on the output of this LT circuit and so the reason why that matters is because without a constraint on that output there is no actual relationship being checked between Bell and amount and so in this case it would allow an attacker to withdraw more funds than they should be able to essentially causing an underflow in that computation performed down at the bottom so the last particular category that we're going to look at is constraint computation discrepancies so these occur when computation cannot be expressed directly as a constraint and so I already mentioned how some computations need to be expressed separately and so in that case someone needs to make sure that they're modeling the semantics of the computation correctly and if they don't then again that can lead to these under constrained bugs and so this one is perhaps the most interesting because it requires someone to reason about an operation that they performed and ensure that they're actually understanding it to properly constrain the behavior and the verifier and so in this case I only point out a single case where that happens although there's many more in our paper it's really due to space reasons and the the previous tree but let's take a look at how this happens so this circuit is going to compute a multiplicative inverse and so what a multiplicative inverse is if you don't know is essentially it's going to multiply by the inverse of B modulo P so that doesn't really matter you can think of it as Division I know the the operation looks like division it's not division either way it's got similar properties to division and so similar to division the multiplicative inverse is undefined when B is equal to zero and so the reason why that's important is because if you look at the constraints below this does not consider the case where the user might provide a value where B is equal to zero and so what that means is if someone ends up providing a equals 0 and b equals zero out is completely unconstrained allowing someone to pass in any particular value that they want and so obviously that is not very desirable and so at verdice we've been working on building tools that can detect issues like these and so in particular we've built a static analyzer a fuzzer and a formal verifier and so each of these come with different benefits and so for the static analysis that I'm going to wait for a second that's very loud [Music] so if you didn't get that if you want to practice your talk before tomorrow apparently you can do that somewhere either way so at Paradise we've been developing tools each of these tools have different synergies that um I'm going to talk about briefly so static analysis comes with some guarantees in that it's going to look for particular patterns and if it doesn't find those patterns then that means that your circuit will not have those bugs however and it also has requires little specialty knowledge and is highly scalable but on the other side it provides you know while it does provide some guarantees they're fairly weak when you compare it to something like formal verification and also with static analysis you have to worry about things called false positives and so that means that not everything that the static analyzer identifies is going to actually be a bug we also have a fuzz tester and so the nice thing about fuzz testers is they're highly scalable they do not require any specialty knowledge and they give you concrete evidence of exploitability the only issue with the fuzz tester is it provides no guarantees and finally we have a formal verifier and so the nice thing about formal verifiers is they provide very strong guarantees however formal verifiers are hard to scale to large circuits and they can have potentially long run times and it's not always clear to know whether the formal verifier has stalled or if it's not going to find a solution and so here I'm going to or in this talk I'm going to highlight the static analyzer because we created a static analyzer that can detect all of the issues that we've talked about previously and so the way that we do this is we first construct this thing called a circuit dependence graph and so I'm not going to go into a whole lot of details about what this is but essentially the intuition behind it is you want to identify discrepancies between the computation and the constraints and so essentially the way that it works is each signal within your circuit is going to be a node and then the relationship so basically assignments within your circuit are going to be encoded as edges and so here if we have an assignment in the computation that will be a solid Edge and if you have an assignment in the constraints that's going to be a dotted Edge and the reason why this is useful is it allows us to start reasoning about the computation and the constraints within a single form and it abstracts away some of the behaviors within the circuit that we don't care about and so from this we created a static analyzer or we integrated this into our static analyzer called Vanguard and essentially the way this works is Vanguard is going to take in your source code and then it's going to Output a list of vulnerabilities within your source code and in particular the way that it does this is it is it first creates a CDG and then it's going to analyze it in particular ways in order to identify bugs and so this static analyzer can look for all of the bugs that we talked about previously and so we used it to analyze 258 circuits from 17 public circum repositories on GitHub and this is what we found so first of all we identified 32 previously unknown uh vulnerabilities and uh these public projects and these are the results that we ended up getting which is pretty interesting so what you can see here is that the most common reason why you end up getting these equivalence bugs is because of these constraint computation discrepancies and so the reason why that is is because developers seem to have difficulty reasoning about the semantics of the computation and so what that means is we need to develop better tools at detecting these these discrepancies such as Vanguard but also at a language level we need to make it easier for developers to use these languages without having to reason so precisely about the semantics because there are Corner cases that they don't seem to always consider such as the case where a division might be zero because that will crash in one place but it could be accepted in another place and so in case you're wondering the numbers are a lot bigger there because some of the circuits that we analyzed had multiple bugs and so in conclusion um we've been developing a number of tools at Paradise today I only talked about Vanguard but in some other events I've talked about uh other tools that we've developed some of them are open source like picus also we've been partnering and working with a number of people in the ZK space including these people and if you're interested in you know working with us or being audited by us you know let me know and finally there are the socials which are important so if you want to follow us on Twitter we're at Paradise Inc and our webpage is paradise.com so thank you [Music]