Ethereum Foundation DevCon 6 - ZKPs: Privacy, Identity, Infrastructure & More Track, 15 Oct 2022

Previous Meeting Next Meeting

⏯

youtube image

►

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

Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on Swarm, IPFS and more.
https://archive.devcon.org/archive/watch/6/are-your-zero-knowledge-proofs-correct/

Recent efforts have made it possible to write zero-knowledge proofs without having deep expertise in cryptography. Nevertheless, these proofs can be subtly wrong and result in situations where the application erroneously “verifies” bogus information from an attacker. In this talk, we will give an overview of our research that can be used to reason about the correctness of zero-knowledge proofs and highlight some of the open-source tools that Veridise has developed to find bugs in ZK circuits.

Speaker(s): Jon Stephens
Skill level: Intermediate
Track: ZKPs: Privacy, Identity, Infrastructure, & More
Keywords: Verification,Zero-Knowledge,Security

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

A

A

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.

A

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.

A

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.

A

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.

A

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.

A

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?

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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?

A

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.

A

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.

A

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.

A

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.

A

You don't have to provide it any additional inputs and it will give you a list of possible problems.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

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.

A

So, let's look at an example of how this actually works.

A

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.

A

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.

A

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.

A

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.

A

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.

B

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.

A

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.

A

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.

B

Well, I want to know what kind of bugs or issues cannot be found by those two tools.

A

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.

A

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.

A

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.