ZK13: Formally Verifying a zkVM - Howard Wu & Alessandro Coglio

Transcript

[Music] All right. Hi. Uh my name is Howard and uh this is Alessandro. We work together. Um and today my talk is going to be on formally verifying a ZKVM. Um for those of you um who may be new to the field, um I wanted to start by talking about what formal verification itself means and what it uh aims to achieve. Um behind every formal verification system starts with a formal verification expert like Aleandro. And um what the formal verification expert is trying to do is to construct using a theorem prover a model a representation a concept um of the system that is being studied and

pursuing properties that you would like to test for and check against um to give yourself strong mathematical guarantees of soundness. Now this can be applied in many different forms. Um I think many times you can break it down into two forms. Uh hardwarebased systems and softwarebased systems. The requirements can sometimes differ in terms of what you're trying to look for in each. Um but uh at the end goal is always the same. And for instance, in a hardwarebased system, you might be trying to check for the correctness of a flow of say a risk 5 chip um and one of its op code sequence and the way that it processes um is being performed correctly. And you know that that that's kind of one example of of a form of verification in the hardware sense. On

the software side of things, often times you're trying to check for um some form of completeness or soundness about a piece of code um or a behavior of code. Um for instance, if you have a compiler and you want to write a new pass in your compiler, you want to make sure that under all circumstances or all inputs um um that uh this uh pass will behave in the expected um uh form or pattern there. And so this is kind of a way to really try and ma mathematicalize and formalize uh your notion of what you're building. So as I've mentioned, there's a correctness property here. This is what you're really testing for. um and that property is is effectively what you're trying to evaluate on. Now based on what the theorem prover says you can

get one of two possible outputs. One could be a green check that says hey the this uh this proof of theorem is correct but it's it's more nuanced than that. It's not just a simple green check. There's there's honestly much more to it. uh um you you you want to really dive in and understand what it is that it checked and and to what level and to kind of what extent um the check was complete. Um but I think one thing that's worth noting here is that this type of a check this type of a guarantee is much stronger than many other techniques that you may have heard of. Uh some of you may have heard of for example fuzzing um where you run a run a fuzzer uh with and you have it kind of uh give just a random set of inputs uh

random in random out and you let it run overnight or you let it ran run for a week and you know you you give yourself some level of assurance with fuzzers that um the system behaves as intended. However, what makes formal verification so much more powerful and why this proof becomes even more powerful is that you have a much higher assurance um than this type of fuzz testing. So you can now address cases that are really sampling for all types of integers or for all types of variables for all types of circumstances and that gives you a strong assurance. Um it can also be used to justify complex optimizations and also suggest new optimizations. So, for example, for those of you who have dabbled a bit in

formal verification, you may be aware that um if you're trying to formally verify um an R1C circuit, um often times you might actually realize by running this that yes, my circuit is uh is constrained correctly. But I actually have over constrained and I can actually reduce some of my constraints and these models are actually quite useful with the eye and interpretation of of a formal verification expert to identify that. Now on the contrary, let's say that the theorem prover errors out, it fails. What do you do then? Well, unlike unlike you know how many of the talks here on ZK proofs have gone, it's not just a simple false like it's not it's not just going to come out and be like

it it's a little more nuanced than that. Um you have to go through and actually parse and understand again with an expert why the proof itself is not working. and and this process of discovery is actually how you go to kind of remedy and find the bugs uh in the original implementation. Um you in the process of discovering this with a formal verification expert, you tend to reveal and find new bugs. Um and so that that effectively is uh is an overview of how formal verification works as a system here. Now, myself and Aleandro and many of of our team members who are here today, we all work on a blockchain called Alo. And some of you have heard of it, some of you haven't. Um, I

thought it'd be useful um to talk about form of verification in the con context of a blockchain like Alo. Why? Because Alo is a ZKVM. And just to help paint the picture for you, um I often like to use this uh graph of programmability and privacy where, you know, Bitcoin is quite low on both. it's it's just a coin and it's it's pseudo anonymous, right? So, it's not fully private. Ethereum said, "Let's take that idea and add some some programming to it." And so, you ended up with high programmability. Zcash said, "Let's go the other direction and extend Bitcoin um to offer full privacy." So, extending that pseudo anonymity into full anonymity. Um and now there's this upper right hand quadrant of saying, "Well, what if you could achieve that full level of privacy but also have the programmability of

Ethereum, aka private smart contracts?" That's the that's the holy grail. That's the kind of goal that that we wanted to build and achieve with Alio. And so this this graph is meant to illustrate that. Now based on what I just described, you can probably imagine that there is a myriad of potential risks in building a system like this because you are now building a general purpose VM uh that is being proven mathematically using zero knowledge proofs using uh circuits and constraints under the hood. And so you to to really give you the level of assurance that this is working and this works especially with privacy you want something like formal verification. And so to give you a sense of all the parts where things could go wrong, this is an illustration of the actual dev flow of

the actual user flow from top to bottom. Um user comes provides some LEO code alongside it. They provide some public and some private inputs. Um that then gets operated on and run via dev tools specifically uh you know the program is compiled into AVM bite code. um and you get out these public and private outputs and you get out this zero knowledge proof, this proof of um an off-chain execution. You've ran your code, your smart contract code offchain. And in addition, your your your contract might say, "Hey, uh in order for me to finish, I need to settle on chain." And when you go to settle on chain, there's some settlement logic that you need to finalize as well before it fully lands uh in in a block. And so this is kind of every arrow that was illustrated here is

a potential point of failure. And so we wanted to formally verify as much of this as possible and yeah more so once you've done all that then you need to submit it to the blockchain right so the AVM by code on the left gets sent via a deployment transaction it's like deploying your contract on any blockchain um and then over here you have the verify and the execute pieces so you need to verify the proof of your offchain computations and to settle you have to run a small bit of code for settlement um and and that's that's this execute piece which again lands in a [Applause] So, you may be wondering why apply formal verification to Alio. Well, I've already started to prime you and give you some of the answers. Um, but to make

it very concrete, bugs in blockchain software can lead to, for instance, the creation or destruction of currency. And as we all can agree, the soundness of your money minting system is pretty important. Uh, I see some thumbs up there. Um, but even more so, we're talking about a chain that actually is going to offer users privacy in their accounts onchain for the first time. And so for their program privacy and for their program data, they may not want to make it available and revealed to everybody. And so a loss of data privacy or integrity would also be detrimental to a system like this.

And for the cryptographers in the room, I think you can also come to understand that um a lot of teams especially in this room are working on new ZK circuits. There's new I I hear and see new circuits being built day in day out. And um under constraint bugs can be particularly pernitious. You may ask what are under constrained bugs? This is a bug where um you expected the adder to take in two two variables x and y and spit out the value z uh being the sum of x and y but maybe you forgot to think about overflow and underflow behaviors to make it safe.

In that case you would have under constrained because you didn't provide the necessary checks the value checks and balance checks to reflect for the case of when that happens. And so these are the types of models that you know you you tend to run into and tend to get caught fairly quickly when you're using a formal verification uh method to to kind of formally prove the correctness of that circuit. So you know that is that is kind of what under constrain means. Now you can fool a verifier to accept the fake zk proof then with that technique. You know if that if that overflow bug exists um I could exploit that and then convince someone that I actually had all this money when I didn't have all this money. uh that would be very bad. Um but I think the bigger problem and as many of you know

is that as an industry a lot of teams in ZK are moving fast and shipping fast and uh these are bugs that are very hard to test for and to make sure that you actually catch these bugs there's very few techniques that get you that strong level of insurance. We alluded to fuzzing but in reality formal verification is probably the most surefire way that we know of today to actually detect these types of issues here. And so formal verification can prevent that. And in order to demonstrate that uh I'd like to hand it over to Alessandro uh for him to walk you through a few examples of how formal verification applies in ALO.

I think you have a mic. Here's the clicker though. All right. Can you hear me? Yes. Good. So formal verification can apply to uh different parts of the uh Alo ecosystem. Here's a notional flow let's say of data. you know, you know, one writes an AO application, uses development tools to build transactions that include, you know, zero knowledge proofs, finalization code, etc., and that gets gets deployed to the ALO blockchain. So, there's a lot of components here where you can apply for notification. One is to check uh application properties of of LEO programs. You know, for example, is the program secure? Is it leaking information? Is it doing the right thing? Things like that. development tools they do compilation of chain

execution the knowledge proof generation. So do they do that correctly? So do they preserve the semantics of the application which is what the user is writing things the smart contracts in. Um and also in the blockchain itself there is a consensus layer to uh organize the transactions into blocks. uh there's the mechanics of zero knowledge proof verification onchain execution and so on and those you know for example for consensus we want to show livveness and safety properties uh for knowledge proof verification on chain execution we want to uh show correctness is it doing the right thing you know what um so that that's where it applies so uh to date we have applied these techniques to some of

the components and so initially we we worked on the Leo language we formalized its syntax and semant semantics. Uh it was for an early version so we we need to update it but you know it was complete at the time and we also uh developed a tool to generate theorems um every time the compiler runs for just initial phases of the compilation. So like parsing and what you call canonicalization and we did find bugs in the parser in in that way. So that that was useful. Um later we we we moved to uh the zero knowledge circuits that Howard was describing. So what we did is formalizations and verification of a number no good number of the uh operations of the circuits uh in the uh

in our blockchain that implement operations and we did find both bugs and optimizations in the process. Uh more recently we worked on the consensus layer the BFT Alo BFT protocol. We formalized the protocol uh verified uh main property which is blockchain nonforking and you know we are extending it towards other properties and we also found some bugs and some optimizations. Uh so let me give you some details about the last two the circuits and the BFT. Here's a super simple example of a of a circuit which is uh in R1CS because that's what we use. Um it's what does it do? It's a division. You know the X and Y are the inputs and outputs NC is the

output. It is the quotient if Y is not zero. Otherwise it's an error. So um for this we want to prove two properties for this kind of circuits. One one is soundness which says that every solution to the constraints corresponds to a non-erroneous computation and the other property the converse is completeness. So for every non-erroneous computation uh there is a solution to the constraints. So another super simple example of a circuit that is actually wrong is the one for positive square root. If you write the circuit like that it's under constraint. That's what our mentioned before uh which is a problem.

So we we we try you know because it allows a negative root. So we we cannot prove soundness it does not hold and when we do the proof we we discover why. Oh yeah because there's another solution. Um incidentally completeness still holds but you need both. Um now briefly the the the off gives you the flavor. The circuits are more complicated the ones that we did but this is a simple example. So the the consensus protocol here um it's there's a number of validators. Some are correct, some are faulty. The red one is faulty. They achieve consensus. And our protocol starts from the the existing narval protocol which serves to uh partially order transactions into a DAG.

If you can see the top parts of the green boxes, there are little DAGs. That's what they agree on. Uh and then there's the Bullshark um protocol which locally linearizes the DAGs into blockchains. And that's the the lower part. You see the little blockchains there. But then we made some significant I mean the whole team Alio and Provable made significant extensions which was one is that the validators are dynamic. So they can change potentially at every block even though usually they don't but they could. Um also we use a stake and not just numbers of validators. And then there's also a phase of syncing when the validator comes up it has to sync and there's some no subtle issues there for correctness. So what what we did um here

is that we formalized the protocol as a label state transition system like an infinite state machine and we proved properties mostly in the form of invariance which say that you know the invariant holds initial state and is preserved in um in every state. Um the main thing we proved which involve quite a bit of work was to show that blockchains never fork you know. So essentially if you have two correct validators, they have the wrong copy of the blockchain. So sometimes they have the same blockchain, that's fine. That's perfectly good. One may be a little ahead. That's okay. That can happen. Uh but they cannot be incompatibly ahead of each other. So they they they need to so that would be uh would be wrong. And so

we we proved that for every reachable state from initial state you will never end up in a state where they have forked. So blockchain is never that's the formula just if you're interested. Um more information there are some papers uh if you want to take a picture you can on my web page just look up my name and you'll see there and uh with that I will give the mic back to Howard who has a call to action. I think we're out of time. I think as a just finishing thought for those who are interested to give this a try uh there's the Leo playground. It's a play.org. Um obviously Alo is at alo.org and Provable, which is the Ali Labs company, is at provable.com. Go check out our Twitter as well. Um, but with

that, I'm out of time. Thank you very much. It's a good, man.