Are Your Zero-Knowledge Proofs Correct? by Jon Stephens | Devcon Bogotá

foreign [Music] I'm John I'm also the CTO and the co-founder of veritis and so today I just want to ask you a question are your general knowledge proofs correct why don't we find out so just a little bit about verdice all of us come from an Academia background so on the slide right here you can see some of the main members from Paradise so on the top those are the co-founders including myself and on the bottom you can see some of the other people that we have here at Defcon so if you have any questions please come and find us ask us questions they're also right there in the third row but yeah so just a little bit more about us uh we are a security company so we provide Audits and we also prefer or provide Tooling in order to find vulnerabilities in all aspects of the blockchain and so basically we build tools to help ourselves and other people find bugs and defy applications blockchains and what we're going to be talking about today zero knowledge circuits and yeah we're very interested in making our tooling available and so today I'm going to talk about specifically our open source tooling and not about the tooling that we're providing as in our security as a service Suite so uh to begin with I think that would be useful to talk about what sort of bugs we actually see and zero knowledge circuits and so the reason why we want to do this is because these circuits are extremely prevalent especially in L2 blockchains and so that means that you can see these circuits integrated into smart contracts themselves like tornado cache and semaphore and blockchains and also there are a number of libraries for circuits as well like the the circon lib and so one of the interesting things that we've seen is these circuits present new challenges especially for you know people who are interested in security and the reason why we want to do this is because we've seen a number of exploits in a or in all aspects of the blockchain from Smart contracts to the blockchain itself and these zero knowledge circuits are a relatively new domain and so while we haven't seen very many uh hacks in the circuits themselves other than luckily the the ones that tornado cash found before it was exploited we want to make sure that people are thinking about the security of these circuits as they develop them and so the way that we want to do this is by or for varadise we want to provide tools and so I think that the best way to start is to talk about some general types of bugs that we see and to do this I need to kind of establish like the model of the zero knowledge circuit that we're assuming here just because these circuits can be fairly complex and so here's a simplified model of the circuit so basically what happens is there's going to be a witness generator this could be a blockchain or a smart contract or something like that and it's going to take in a set of public and private inputs it's going to generate a witness and this witness is going to be provided to the prover along with some additional information which will generate a proof and then finally that will go to the verifier and then the verifier is going to say yeah it's correct or no it's not and so when someone wants to create one of these circuits there's a couple of ways that they can do so and the simplest model they simply write a single application so this would be their circuit application written in something like circom or Cairo and then that will generate a the witness so your smart contract for example and it will also generate a set of finite field constraints which is later used to generate the prover and the verifier and so the interesting thing that we see here is you have a single application which is used to generate uh two different or two different applications which do slightly different things and more interestingly they can be out of sync and so one type of bug we see here obviously is if someone doesn't Implement their circuit correctly so if that happens then we have a functional correctness violation and it basically just means you know someone needs to go back and rewrite their circuit in a way that's correct the more interesting bugs though are when the witness and the constraints are not in sync with each other and so this happens because generally these languages provide ways for you to um put specific logic in your witness and put specific constraints in your finite field constraints and so if it turns out that your constraints are less permissive than your generator you could reject valid interactions with the application so for example if you have a blockchain it's possible that in this case you could have a denial of service where the blockchain wouldn't be able to process transactions which you know wouldn't be great the worst case or the more dangerous case though I should say under constrained is an under constrained circuit so what happens with an under constrained circuit is the the constraints are more permissive than the witness itself and so the reason why this is more dangerous is because while the witness might be correct and it might provide all of the interactions you want and they're all accepted by the constraints everything seems great however an attacker could then come in and they could provide an alternative witness which might be used in order to get some alternative transaction or logic accepted by your constraints and then proven and this would necessarily be bad because let's say one of the constraints which uh didn't end up in your finite field constraints was equivalent to uh the sender is equal to the admin right obviously if someone was able to bypass that then bad things could really happen and so the way that we deal with this in Paradise is by using a um a field in computer science called formal methods and so formal methods provide a way of automatically reasoning about software and so it does this by uh understanding and understanding the semantics of the underlying program and iterating over that program in order to determine information about it and so basically what we're going to do is we're going to use formal methods in order to find bugs and create proofs that the software is correct and So within formal methods there's basically three different fields so there's automated testing so if those of you are for those of you have heard about fuzzing that falls into this category and so basically in that case someone is just going to run the program on a bunch of inputs and so this is useful for finding bugs next we have static analysis we'll see a static analyzer in this talk which is going to analyze your source code for a particular class of bugs and the important thing about these static analyzers is if they can't find the bug they it has proven that the bug does not exist in your program however you know the more interesting case is if it does find a bug and then last we have formal verification some of you might have heard about this there are multiple ways to perform formal verification but at Paradise we're particularly interested in automated formal verification and so basically what this is going to do is it's going to analyze your software and make sure that a specification where a specification is essentially a way of expressing the intended behavior of your application it'll make sure that that specification holds for the application and so that means that after using a formal verifier one you can verify custom correctness properties and two you will have proven that that property holds or that your implementation is correct and so as we go across the Spectrum it takes more effort in order to uh both build and run the tool but it also provides much stronger guarantees and so we're going to be looking at some of the open source tools provided by veridice that fall into these categories and so first we're going to talk about a static analyzer which performs common vulnerability detection on Cairo Pro or circom programs so basically what I'm going to describe this is the type of bug that is found by a a static analyzer that we created called pikis and so basically what it's going to look for is uniqueness bugs and so what a uniqueness bug is is it happens or it occurs when a constraint allows a single input to map to multiple outputs and so what I mean by this is if you look at this circon program over here you don't have to understand what it does but basically there's a bug that's circled in red the reason why that's circled is because it constrains all of the outputs except for one very specific output so decoder is supposed to Simply uh zero out all of the bits except for a single bit that is specified by imp and so what happens here is if you look over on the right you'll see that the constraint specifies that that multiplication has to be equal to zero so there's two ways that it could be equal to zero it could be equal to zero because the output is equal to zero or it could be the case that imp minus I is equal to zero and so all of the cases where uh imp and I are not equal to each other our constrained but in the case where imp is equal to I we find an unconstrained bit and so what does this mean this means that an attacker gets to decide what the value of out at imp is so it could be the desired value which is one or it could be zero and so why does this matter well because of the reason that I told you about earlier it means that depending on how this circuit is used someone might be able to leverage this uncertainty in order to violates some assumptions that you have made and hack your protocol so what can we do about this well I already told you that we're going to be using static analysis and so there's two types of ways that we can solve this problem one is we can just perform straight static analysis and so what this is going to do is basically we'll just look at the inputs and outputs and we'll say that if the output is a linear combination of the inputs then it must be constrained so that works however it also produces a lot of false positives which is undesirable because then you have to go and you have to determine is this real or is this not so instead you could use something called open to solver so what an smt solver is is it's simply a a program that can solve mathematical formulas and so because you have constraints uh you can encode this mathematical formula that states whether or not a particular output is constrained the problem is normally there are many constraints and so if you tried to send that to an smt solver it would quickly become it would quickly bog down and it most likely would not be able to solve a uniqueness for large circuits so basically we see that static analysis is scalable but not precise and we see that the smt solver is precise but not scalable and so what we have done is we've developed picus and so pikis is going to take in your constraints and it's going to Output one of three things so it's going to Output yes this is uh this particular circuit is entirely constrained no it's under constrained or I don't know but the way that it does this is by using a combination of static analysis in smt and so what I mean by that is we're going to have two phases that are going to iterate and so basically in the first phase what we're going to do is we're going to take those constraints and a set of signals which we've already proven are constrained and then we're going to compute a new set of constrained signals and so this will give us a set of constrained signals that we we already know are constrained and so if we end up finding that all of the output signals are constrained great we're done otherwise if there are some output signals that we haven't been able to determine if they're constrained we can go to the next step and so the next step is the s t phase so what happens in the smt phase is we take these signals which we have already proven are constrained and then we again take the set of constraints and we use an smt solver in order to try to find additional output signals that are constrained and so if we happen to find that all the output signals are constrained again great we solve a problem if we find an output signal that is unconstrained because we can prove that in this case then we say all right you have an under constrained signal and it's specifically this one and then otherwise if the smt solver fails for some reason so basically that happens if K prime prime is equal to K then that means that we've basically stalled and we'll instead just return I'm not sure so it I mean the last case is if we ended up making progress then the important part is we can go back to the static analysis case because we have now proved more cases are uh constrained and so that means that the static analysis phase might be able to make further progress and so basically we'll do this in a loop and we find that in this case picus is able to scale much better than the previous attempts that we saw so basically we evaluated this on a set of circuits and uh picus was able to solve I believe that comes out to 98 percent of the circuits that we threw it at whereas if we look at static analysis and smt static analysis returned a bunch of false positives and smt timed out on a lot of the benchmarks and so this is the first tool that we look at so the important part is you provided a circuit and then pikis does all of the work for you you don't have to provide it any additional inputs and it will give you a list of possible problems the next thing that we're going to look at is a verifier so this performs automated verification so what I'm going to talk about next is a tool called Magi so what Magi does is it performs automated verification on Cairo programs and so the way that it works is you will provide Medi with your source code and a specification and as I stated before the specification just specifies the intended behavior of your Cairo contract and then Magi will spit out either yes or more interestingly it'll spit out no and it will tell you why and what I mean by why is it will provide you concrete evidence of why uh your specification does not hold and so the way that it does this is it's going to take your specification your program it's first going to translate it into a symbolic representation it's what I mean by a symbolic representation is rather than having you can think of the symbolic representation as being unconstrained so basically any value in your program could map to any other value in your program and so then once it does that it's just going to run this through it's it's going to run your program symbolically and I'll show what that means in a little bit and more importantly it's going to interact with an smt solver in order to generate proofs that your uh any or as it runs your symbolic program it's going to use the smt solver to prove that your behaviors are consistent with the specification so let me get a little bit more concrete about this in order to do this you need a little bit of information about symbolic execution so basically the way symbolic execution works is looking at the very top you can see just a set of variables and so we start with these variables being mapped to any possible value so unlike testing where you say like in this case U is equal to 5 we say U is equal to some symbolic value so it's going to map to any value within the range and then when we symbolically execute the program what we're going to do is we're going to essentially just run through your code and generate case statements so for those of you who remember you know your your proofs class basically we do case splits whenever we come to like conditionals and so here what you can see is starting at the very top we have everything unconstrained but then once we enter that first if statement that you see you'll see on the left hand side that U is equal to 5. but then we also need to consider what happens if you don't enter that if statement and in that case U is still some unconstrained value and the important part is at the very end of this after executing the entire function we end up getting a set of symbolic equations which we can then send to an smt solver to make sure that it's consistent with your specification so some of you may have noticed that it seems like there's a fairly large spread so if we look back at this it you kind of get this tree like structure with a lot of breadth and so in order to make this actually scale what we do is we have to perform a basically intelligent merging so essentially what you can consider is after we execute an if statement once control flow joins back we can also join those States and so if you don't understand what this means that that's okay basically all I'm saying here is that in order to improve the scalability of this tool we push some of the work off onto the smt solver and we you basically have to balance the work that your symbolic execution engine is doing and the work that the Sim that the smt solver is doing so let's look at an example of how this actually works so here you can see the move function in maker Dow's Cairo implementation and so the specification that we're trying to check is basically that move transfers funds correctly and so the specification that you see on the right hand side basically says that after the move function has executed the uh the die balance of the destination should be greater than or equal to the die balance at the beginning and then the die balance of the source should be decreased by an appropriate amount and so the interesting thing here is Magi reports that this does not that this is not sound this specification does not hold for the code on the right hand side and specifically it says that it does not hold when rad which is you know the amount that's being transferred is equal to some specific value and so the reason why it reports this is because in Cairo you have this interesting case where because of the size of the large primes they are going to be less than the size of a uint-256 and so Cairo ends up splitting your un256 into two parts the lower 128 bits and the upper 128 bits and so importantly the reason why Magi reports there's a violation is because the maker dial developers here forgot to constrain the value of rad and so the way that you do this is in Cairo they provide a specific function in order to make sure a uint-256 is properly constrained and if you leave that out that means that your un256 is not well formed and so once we add that check back in and then we send this back to Magi Magi will report yeah everything's right the the specification holds and so in this case we have properly guaranteed that this move function transfers funds correctly and so this was just a very simple case however we've been working with the makerdale people in order to verify their Cairo implementation of uh their protocol and so as we've done this we've ended up finding I think at least one bug that the maker Dow people have merged into their um their implementation so that's all I have for you today if you are interested in learning more or seeing demos of these tools uh in about an hour or so at three o'clock we will be down at the ZK Community Hub just giving a demo of these tools and a couple of other ones also on the left and right you can find links to the repositories for picus and Magi so if you're interested in trying them out please do and um there's also a Twitter link so if you want to follow us on Twitter that would be fantastic [Applause] hi uh thanks for your talk uh just a question when you're talking about uh these Cairo contracts and could you say if I didn't have access to the source code and I just had this circuit that's like how easy is it in practice to exploit these uh you know kind of arithmetic errors or constraints so if you're an attacker and you don't have access to the source code how easy is it to figure this out um yeah that's a good question uh you know attackers are very good at looking at low level code and figuring out how to exploit it and so I would say that you know if you were trying to get security through obscurity that's really not going to work for you here because generally your code is going to be public somehow and so if someone is able to gain access to even the low-level implementation of your code then they could possibly figure out how to exploit it and on top of that we've seen cases where even if someone doesn't have access to your code but they're able to query it they can also find uh potential exploits well I want to know what kind of bugs or issues cannot be found by those two tools so what kind of bugs cannot be found by these two tools okay so uh for picus because it's not performing functional correctness checking it can only find under constrained bugs and so that means that it won't be able to find like if your program is written incorrectly for Magi because it is verifying functional correctness it relies on the quality of your specification however if we assume that you have specified the behavior of your program properly it should be able to find any potential bug in your program so for example one thing that we see is if you write a specification that says let's say the die is transferred correctly but then it turns out that due to an under constrained bug or an under constraint bug or a uniqueness bug it doesn't end up being transferred correctly imagine I will point that out however it depends on the quality of your specification and um yeah and also won't find bugs in anything other than your Cairo contract so if you perform interactions let's say with other with other applications that Magi doesn't have access to their source code imagine I won't necessarily be able to check and make sure that everything is correct it has to make simplifying assumptions basically