Safely Snarkifying Ethereum: Formal Verification and Protocol Snarkification

Transcript

Hello. Great. Hello. I'm Derek Sorenson. I'm part of the Ethereum Foundation research team. I'm on the protocol snarkification initiative, which is chiefly aimed at safely snarkifying the Ethereum protocol. So, snarks, ZK-VMs, this zero-knowledge proof technology is central to the Sorry. central to Ethereum's roadmap to lean Ethereum, to scaling Ethereum both at the execution and at the consensus layer.

What a snark does in practice in this case is that it means that a client does not have to replay all of the transactions, but can instead accept a proof of correct execution so that the a proof that the updated state is the result of correctly applying the transactions in a block to the previous state um which means that bugs in the cryptography and in the snarks that we're using can, um, introduce, uh, pe- people can steal money, people can compromise the security of Ethereum protocol, which is of course a a serious problem. So, snarks are critical infrastructure in the long term for

Ethereum Foundation. Which means that on top of our normal testing and fuzzing and hardening techniques that we need to apply to, you know, everything we ship, we need to treat snarks as, uh, requiring the highest assurance possible. And therefore, we should apply the methods that deliver high assurance, uh, code. And in this case, uh, formal verification. Formal verification, um, is a practice where you take a program and you take a formal description of what it means for that program to execute correctly, and then you prove, uh, with formal logic that your program satisfies that description of correctness. So, this

very simple example that I've included on this slide here is suppose you have a function and you've optimized it. So, your function F, you've optimized it to a function F optimized, and the definition of correctness for this optimized functions is that it behave the same as your previous function aside from performance. So, it kind of in an extensional sense, it behaves the same. So, we can state this formally, um, in, uh, by saying that in this case, uh, what's on the screen is a pure functional representation, but you can, um, you can say for all inputs, for all states, um, applying F optimized gives the same result as applying F. And that

is a formal statement of correctness. That's what you mean. So, if we can prove F optimized to be correct with regards to this description, we say that it's proved correct with regards to this, uh, yeah, formal specification, this description of correctness. And, uh, my slide has an asterisk there because there are some some caveats, uh, that I won't say anything about now, but I will at the end of the presentation. Our work with snarks and ZK-VMs as it applies to Ethereum is, um, is to obtain the highest possible level of assurance for ZK-EVMs.

Our our end goal is a bug-free ZK-EVM. And um we're doing this work in three main tracks. I'll give a quick summary of each of these main tracks and then focus on the last one. So, the first is, uh, we're doing a lot of work at the RISC-V level. All of the ZK-VMs that are part of the EthProof's initiative and that are candidates for the network of provers that will scale Ethereum implement RISC-V semantics, uh, at the ISA level.

And so, they're RISC-V ZK-VMs. So, what we need to do is we need to uh, formally verify that the polynomial constraints implemented by these ZK-VMs correctly encode the RISC-V ISA. And we have some really good tools to do that. Uh, first of all, the RISC-V ISA semantics, um, are available, uh, in various Ethereum provers, including Lean, which is the one we use. Uh, and also we have developed tooling, uh, to extract the polynomial constraints into into Lean. So, to to kind of, um, to take what's in the Rust code and put it into a place that we can reason

about. Um, side note, by we, I mean about 30 or 40 collaborators in the whole ecosystem. So, it's not just the Ethereum Foundation, but it's it's, uh, many many collaborators, um, throughout, um, Then, at a level higher than that >> [clears throat] >> is the EVM level. Each of these ZK-VMs, uh, will run the EVM in RISC-V. And so, these are called guest programs. So, we need to formally verify that the guest programs, um correctly uh, are are correct implementations of the EVM, which, uh, seems like it might be a simpler task than, uh, than the RISC-V semantics, um, verification, but it has its subtleties.

We have managed to prove, by by we, I mean a collaborator, uh, Runtime Verification has man- managed to prove that ref, the, uh, the, um, RISC-V code that ref produces, um, is formally equivalent to a formal model of the EVM called K EVM, which is one of the first and oldest and most storied uh, formal model. So, that that is a proof of correctness. There are some caveats here, um, and a lot of work to be done. Um, >> [clears throat] >> the state transition function was not formally verified in this case, um, and there are some questions about the boundary of verification.

>> [clears throat] >> Last and finally is the cryptography track. So, we have thus far cared about, uh, the implementations of, um, of virtual machines and, uh, RISC, you know, the EVM and RISC-V taking for granted that the underlying cryptography is sound, but the cryptography that produces a snark as a zero-knowledge proof is actually quite elaborate and complex, and it requires a lot of advanced mathematics and abstract algebra, um, including finite fields, um, polynomials over those finite fields that have, uh, and elaborate operations on top of those. And so, we need some way of

evaluating these ZK-VMs, um, on the basis of their cryptography to ensure that the cryptography itself is sound. I don't know about you, but in when when I interact with kind of real-world protocols, sometimes I'm tempted to take the cryptographic guarantees, uh, for granted, but, uh, bugs in the cryptography, um, kind of compromise everything at at the base level. And this is what I'll be talking more about. To address issues in, uh, in the cryptography itself, we have developed a library called Arclib, this one here in the middle, which is a library of snarks, um, and

everything that kind goes into building a snark, which I'll get into some more details in in a minute. Um, this is part of a large family of libraries. If you, uh, if you go to this QR code, it will take you to the the website of of our whole project. There's an associated GitHub that has maybe about 15 or 20 repositories that all do their own thing in this in this ecosystem. And, um, Arclib is one of the principal ones of these. It's supported by several repositories. I've included two, the one above and below here.

The one above is called VC VIO, and it formalizes all of the oracle uh, computations. So, if you're familiar with STARKs, there's, uh, there's this interactive oracle reduction framework where um where you uh, you you uh, produce a witness, uh, there's a challenger, and you kind of go back and forth, and that's how you get your, uh, probabilistic cryptographic guarantees. So, all of that is formalized in VC VIO, and Arclib relies on it. And Arclib also relies on is fundamentally operations on polynomials, and so we have a library called CompPoly, which is a library of computable polynomials in Lean, and it does all the polynomials and field arithmetic. Um, so this is kind of the

machinery that we're using. I'll dive a little bit more into detail on Arclib as a library, just to kind of give you a sense for, uh, for what it looks like. So, if you go into Arclib, there are, uh, it's doing, uh, a lot of things. Um, like I said, it has oracle reduction, has, uh, um, commitment schemes. Maybe the principal, the kind of most, the core aspect of Arclib is this, uh, proof system directory. And the proof system includes all the standard, uh, proof techniques that you will find in the wild for ZK-VMs and snarks. And so, this includes Batch Fry, uh, Binius, um, Fry Plonk STARK WAR SumCheck.

These each of these is kind of is a is a large task on its own to formalize correctly. And um you know, has experts working on on on each of these. Um, Um So, here is an example of some of the kind of formal code from the FRI spec. FRI has various folding rounds, and you need to There's a consistency check on folding rounds. This is a statement that says our specification of FRI um in these folding rounds, if you give it a correct witness, um the folding rounds will will uh recognize it as a correct witness, and it will um the consistency check will pass.

Um As you can see, the syntax is fairly is is fairly elaborate. It's It's one of those things that once you kind of get to know the the model and things, it's uh more straightforward to read. But, this is a statement. This isn't actually the formal proof. If you see the by down there in the corner, um what follows in the code base is this formal proof of correctness. And so, um Arclib is an interesting uh case study because in the case of formal verification um it's tempting to think that your If you formalize a description of correctness, uh and then then and you prove your code uh correct with regards to that specification, then your code will just

be correct. But, specifications can be very elaborate themselves. Um Cryptography is a good example of that. So, in the case of Arclib, there are is kind of a multi-tiered approach. On the base level, we have a formal description of how a proof system should work. And above those, we have checked our description to be correct with theorems like this that check, for example, our our description of how rounds should execute in FRI is correct that it takes a good uh uh correct inputs and it actually um produce it It says correct inputs are consistent.

On top of that, for cryptographic protocols, there is what's called a security proof, which which takes the whole elaborate scheme of, for example, a SNARK and proves that that interactive, you know, uh in in in this case, um this this uh polynomial reduction scheme over interactions with oracles actually uh produces the cryptographic guarantees. Oops. There it is. Actually produces the cryptographic guarantees that we uh that that we want. And so, that is a high-level kind of almost like a meta specification. Um And I guess what I'm describing could easily sound like just this

insurmountable amount of work. And one of the limitations of formal verification in real-world production code thus far has been that it is a lot of work to develop these specifications. It's a lot of work to develop the proof tools to formally verify and to write the proofs. Um but, we have seen such uh with with advances in gen AI, um this actually allows us to speed up our work dramatically, and we can do so securely because it's accompanied by formal proof of correctness. And so, the uh what I think a lot of engineering teams are finding right now is that with AI, it can be hard to verify if the code

produced by AI is is good code, um especially when there's so much of it. In the case of this these formal languages like Lean that have proofs, um the the verification uh process is much lighter because the proof uh as long as it type checks, as long as it compiles, is correct. And so, you only need to check statements. And so, it allows us to dramatically scale our efforts. We also have a lot of expert collaborators on this. And so, despite the elaborate nature of this project and the ambitious nature, I guess, uh we are making rapid progress and expect to be able to formally verify all of these proof systems that we we use in in a highly rigorous way.

So, what is the goal, I guess, of having these um these Arclib specs in in Lean? The goal is to take ZK-EVMs in the wild written in Rust, the ones that will run, the ones that, you know, production, they're optimized, all the good stuff like that. And And our goal is to formally verify them to be correct with regards to uh Sorry, formally verify the cryptography aspects to be correct with regards to our specification in Arclib. So, that will require some translation between Rust into a formal language like Lean, which is the one we use. So, I guess that's one strategy, and uh we're actively working on that and making rapid progress and expect to to be able

to do this well. When you translate code in order to formally verify it, you know, from Rust, for example, into Lean, you introduce a trust uh assumption that the translation is correct. There are a few ways to to address this. One of them is to formally verify the the translation, which can be done by metaprogramming, which, you know, I I recognize that what I'm saying it sounds like we're just formally verifying everything on top of each other. Anyway, that is one way to do it, and it has been done. Uh not in this case specifically, but it has been done in other cases. It's feasible.

Uh Another way to do it is to to look at code on the bytecode level. And uh this previously has been uh so difficult to kind of tinker with, so [clears throat] hard to read and reason about, that it um Yeah, so hard to reason about that it's been infeasible. But, again, with advances in gen AI, this really empowers us to formally reason at a lower level. And so, the exact mechanics of how we'll formally verify these things are still being decided, but uh one way or or another, we will do it.

Uh Right. And so, circling back to the the main goal of this whole initiative, it is to obtain the highest possible level of assurance for ZK-EVMs, and we're aiming at bug-free ZK-EVMs, of course. And now I will revisit this asterisk. So, there are always caveats, unfortunately, to formal verification. A lot of mathematicians try to sell it as these silver bullets that will eliminate all bugs. And in a sense, there are some guarantees that you can make, but there are always assumptions that that have to be made, which means that we have to employ all of the other techniques that we already, you know, this has to be just an additional technique for high assurance. We need to fuzz, we need to stress test, we need to harden, we need

to do everything we can to root out all the bugs that we can. A few of the assumptions that are made that are kind of subtle. The first is the verification boundary. Um Anytime you prove a program to be correct, you're always proving it correct with regards to a description, and there's always a limitation to that description. You can't describe every last piece of software in the whole world and natural phenomenon, you know, software doesn't run in as an island. So, there's always a verification boundary, and you need to keep that in mind. Uh Like I said before, sometimes there are bugs in specification, but there are ways to address this. And sometimes there are bugs in the proof tools, for example, these extraction tools, uh which uh which, you know, we have methods to address, but also it's uh

it's worth keeping in mind that formal proofs add a lot to the assurance uh high assurance of software, um but, you know, we still need to be on our guard. That is all I have for you today. I think we have a couple minutes for a 3 minutes for questions. Thank you. I uh This is amazing. Thank you. Um I'm just wondering, let's say this all goes well and the whole thing gets formalized. I'm just wondering, do any of the cryptography schemes you're using, like, where, for

example, do they have assumptions that aren't proven? Like, so that, you know, is there a chance in 5 years you come along and you're like, we made this whole proof, but there was this conjecture in the original cryptography that wasn't there? Or is like everything proven all the way down? In the case of So I >> [clears throat] >> I think any cryptography that will be used in production will have uh security proofs. So, these proofs that the scheme um actually produces the cryptographic guarantees.

Any security proofs have associated assumptions. So, there are there are some What the proof actually is is that uh you have these cryptographic guarantees, if you see these guarantees violated, then one of your assumptions is wrong. And so, there There's inherent There's kind of you need to take the leap of faith with these axioms, uh these assumptions, to even be able to reason about anything. And so, uh yeah, there There will be those. Typically, these assumptions are deeply believable. And so, and so, seeing a violation will uh will will kind of shatter some concept of reality. Um >> [laughter] >> uh But, yeah, I get Yeah, there there are there are there are some assumptions

that that that could be there. Yeah. I Uh do you think when, like, uh like, ZK-EVMs start going into like production and you're trying to kind of like test them out on like a kind of a beacon chain type situation where you can kind of get a like pre-production um chain, do you think it could be useful to say, similar to like optimistic roll-ups, you you like create the like ZK EVM chain, but then also have like a fallback where if there's like you you could basically say like oh, there's a reward to

validators who maybe can naively execute the transactions and then if they find incorrectness, they get a reward to kind of like uh I guess create like bounties so that you can so that it doesn't just completely fall apart if there's a bug. That's a good question. I am I'm I'm not involved in the in the discussions on at at this level, I guess, the fallbacks on consensus. Um I know that before before uh before relying entirely on ZK EVMs, there will be kind of there will be a hard fork where proofs are optional, they're accepted, and um

and then you'll you'll have still have people actually executing every block. And then there will come a time where proofs are mandatory. Discussions still need to be had about exactly what that looks like. Um I think having a fallback um is is always a good idea. Yeah. Cool. Thank you very much. Thank you. Welcome.