Towards Formally Verified zkEVMs

Transcript

[music] [music] >> All right. Thank you. So I can't explain why these slides are bright green. Something has happened in the plugging the laptop and I hope they're legible. Um yeah, I work on the ZK EVM team at Oh. Uh seemed to have lost [laughter] [sighs and gasps] Okay, maybe that's a suggestion. Um Sorry, I don't I seem to have lost slides also in the past minutes. Let's go here. Um great.

So right, let me start again. So I'm on the ZK EVM team at the Ethereum Foundation and we're not building a ZK EVM team or ZK EVM of our own. We are standardizing testing quality controlling ZK EVMs that other teams build. Um and in particular, I'm not talking about Lean VM which is for proving other kinds of statements than EVM execution, just to situate the work. Uh So let's let me start with some takeaways I want to leave you with. Uh first is that I believe we will have uh and must have ZK EVMs with significant formal verifications shipped to scale Ethereum or formal guarantees attached.

Um but that AI does not make that like automatic um especially if what we say is end-to-end formal verification because there's quite a lot to cover. Um so so far even though we've made a lot of progress, in my opinion, we do not have a clear story for how to ship ZK EVMs that are high performance, that are with high assurances where really like you mean very very high assurances everywhere and that are also maintainable. So let me give an update on where I think we're at with respect to the different components of this uh challenge.

Uh I I don't want to talk too much on the for this. I gave a talk with Ignacio uh that I linked to here. And by the way, the this QR should take you to these slides if you'd like to visit any of these links. Um but this displays a bit of the components uh in the in the in the questions that I just described. So in the inner box in the top part of the diagram, we have the EVM implementation roughly roughly speaking um with a little extra stuff to make us have a stateless guest which uh does the work of checking the transactions. And um that is happening inside of a virtual implementation of a RISC-V machine. And I'm saying RISC-V kind of simplifying

the picture going with the canonical at this point approach. Other solutions are available. And inside of that, we have a cryptographic uh layer that absorbs the execution and creates a proof. And all of these things have um you know, you could think of formally verifying them. Uh the other half of the cryptographic implementation is in the verifier in the lower box. And that also uh is a critical component which we should ship with formal guarantees. Um so let me start by talking about the problem of formally verifying ZKVMs. Uh we have more progress here than I in my opinion than we have on the guest side.

Part of that is due to the fact that there is a canonical specification which is suitable for proving that is not maintained by us. The RISC-V community has this thing. They're the experts and they maintain it. And that's great. That solves a big problem that if you attended Derek uh Sorensen's talk earlier, um he he addressed and that we'll come back to. Um that's in a language called Sail which has backends to produce code in other languages suitable for proving uh statements and also suitable for execution. You can make a C guest for instance and you can execute it um and check compliance against that. And indeed, we've we've been doing that for about a year and a half already on the testing side. Um the statement we'd like to prove uh has two

components. There's a completeness part and a soundness part. Completeness says that every valid RISC-V execution is accepted by the proving system, roughly speaking. And soundness says that nothing else uh is accepted. Um so uh let me talk now about the soundness part. Uh we have progress there. About a year ago, a little more than a year ago, we had the first um RISC-V verifications come out. Uh the first was this collaboration between Nethermind's uh formal verification team and the Succinct team to check correctness of the RISC-V circuits in Succinct's SP1.

Uh and then after that the work was done also for Open VM and Pico and then for uh Zisk. Um and we have seen this this these efforts catch serious bugs. Uh so at the very least it's a powerful technique for steering the agents with some like concrete metric, which is can you close the proof? If not, maybe there's a bug. Um so at the very least we do this to catch bugs. Um but there's a question which is maintenance of these. We have not seen these efforts be maintained. We've not seen them integrated into CI. Uh in general there is code which is written and loosely coupled to a specific version of the

ZKVM and maintenance is having agents rewrite. So we need these extractions to be reproducible. Um we need to stress test these. I've done some of this work in the Zisk formal verification. Um but I'd say it's not done there. If you want to contribute, there are lots of open issues to make that uh closing those gaps really concrete. And finally there's testing. We have a lot of trusted components. We have to test the boundaries where we move from trusted to verified. Um and there's very little work on this that I've seen. Uh next would be the soundness of the accelerator. So we can't just execute pure RISC-V and prove Ethereum fast enough. Uh so what we do is we introduce special circuits that do really heavy

operations very fast such as catch caching modular exponentiation and things like this. I I think there's some progress in recent um times, but the only things that I have seen are formal verifications of some hashing precompiles in Open VM. So, there are certainly some gaps uh there for all of the different accelerators that we um standardized. Uh how about standards compliance? So, our team maintains a a a set of standards for these ZK VMs which make it uh which are you know help us to test them, which create an environment where guest developers can target different ZK VMs with more ease um and also handle some very critical questions like how do

what happens when a program terminates? Do we handle that? Should the should the verification fail if the termination is abnormal or should it attest to an abnormal termination the proof these things must be worked out. I mean any any issues even really small silly ones can be catastrophic and we have to really So, whatever we have these standards and uh they have some tests that are under development. They're not completely tested uh but there's no formal verification of those standards. Uh there's no spec for them. There's no attempt at all.

What about um completeness? That's the other side I mentioned. So, we want to know that every valid risk five execution could be accepted. Um oftentimes completeness is overlooked as being less critical than soundness. I don't agree with that whatsoever. Um you know if you have a completeness bug that's exploitable, it means that the prover cannot prove a valid execution which concretely in the Ethereum context would mean you just the network stops processing. If we require these proofs that it's it halts. So, we have to get that right. Um there's an related kind of notion of uh of completeness that you may see if you look at some clean circuits that's a circuit language that's in use. Uh Uh, that's that doesn't solve the

problem. That's you know, you can have complete circuits that don't correctly accept RISC-V program executions. So, what about prover liveness? I mean, circuit completeness is one way that provers can fail to be live, but there's all other more dumb ways like the the CUDA code could segfault. So, that's uh that's not addressed whatsoever by formal verification. Um, last I knew there weren't good formal models of the ISAs for these for GPUs and we're running these provers on GPUs. I Googled yesterday and there's some, you know, generated spec that came up a week ago. I I don't know if we trust it, but there's no work whatsoever on showing that the actual implementation of the prover

doesn't have a bug in it that could cause it to to crash. And again, that could that could mean the network can't produce that the prover's running like supporting the network could not produce proofs and therefore the network would halt. There's also unsafe Rust. It's the same question there. Um, we don't get guarantees from the compiler and so even if everything were ran in a CPU and we were able to extract it to Lean and prove statements about that, the extractions don't cover unsafe code as is. So, special work has to be done there. I I believe there's progress, but I'm not totally aware of all the all the approaches.

So, yeah, we don't want to The meme looks horrible in this green color. I'm sorry, but it's a very shiny engine on top of a duct tape together frame. And, you know, we could have formally verified components and catastrophic problems because of the foundations that support them. Yeah. Um, all right. So, what about more progress? Well, what about the security of the actual cryptographic protocols? There we have good progress in my opinion. Um, in the past we would have experts reading formal descriptions of the protocols written in papers. Um, I think now with formal verification we should formally specify the protocols in languages such as Lean and then make the proofs um there.

Often in the past there would be some small, you know, maybe you your your snark or stark accumulate some small changes that you believe are secure and then eventually there's like a ship of Theseus where you're you know you don't have the protocol that's written in a paper and you don't have a security proof that should be viewed as unacceptable now that we can maintain things with AI and write down these very precise proofs. Um so we have a library that has good uptake called Arc Lib. Arc stands for arguments of knowledge. It's something that you can use to build formal specifications of the cryptographic protocols that we that we care about and you can then make machine proofs of of the cryptographic correctness that there

are so and so many bits of security and this is quite advanced and I'm very confident that this will this will work and we will we should require this of ourselves. Also just as a side note we have many protocols with nowhere near enough actual bits of security. You can look at the sound calc reports so I would add that add that as a a security challenge which is only relate like we would encounter this problem if we tried to formally verify the implementations of those. All right so then here we have another funny meme this like you know you only have the security of your weakest component is the idea of this meme from Tao who by the way contributed these memes even

though he was unfortunately unable to co-present with me. All right so then there's the gap of recursion so all of these ZKVMs produce lots of proofs at a base layer using risk five and maybe in some cases other ISAs and then they need to do some work to check those proofs and compress them all to something small enough that we can send it to the network and that stuff last I knew is is uncovered entirely. Maybe there again maybe there's some progress things move so fast.

I think I would know about it though. So usually I mean these have different proving systems that are can be customized. They have different arithmetizations you know leaf versus compression VMs and so on. Um, and the spec now is something that needs to be specified. We're specifying a verifier algorithm. So this would be something we specify with Arkworks. I'm not aware of specifications of of those verifiers yet. Um, so I would consider this quite open. And there's also maybe a caveat to say even if we tried to prove some statements theoretically about Arkworks specifications of these verifiers, there's even an open question of what is the right framework because of some issues about using Fiat-Shamir

inside of a circuit. So we need to even have theoretical cryptographers make some decisions there about how to how to handle this. So what about protocol implementation? So even if we had good Arkworks specs, how do we know that the protocol in the software matches the spec? Very often it does not. We've seen all kinds of bugs um of that sort. So [sighs] um just to look again briefly at Lean VM. So in that case the it's an all CPU prover. There are some SIMD instructions and like customization for different hardware to contend with. But we have tools that can take safe Rust so at least the safe parts of of Lean VM and turn them into Lean.

And those are I I think some of them will harden and be widely used. So maybe we can trust those. And you know, in that case we would be able to check the prover and the verifier also is implemented in Rust with fewer bells and whistles. So there there's a good story. For ZK VMs, as I've said, the prover is large parts of it and increasingly more and more of it is written in CUDA and we don't have these sorts of tools and there's all kinds of unsafe Rust. And yeah, the verifier maybe has some similar has similar considerations which for time I'll I'll not go into.

But we want to make sure we're not in the situation where the circuit is, you know, Fort Knox and then the verifier is the [laughter] cupboard, I guess. Um, all All So uh let's talk now about guest programs. As I've said, uh the situation is more difficult there. First of all, there's not a canonical specification by any means. There's a Python specification for the stateless guest that my team maintains, which is not uh merged yet because this is still speculative stuff. Um but it's not suitable for formal proving. The existing ZK or the existing EVM specs, as Derek said before, are not really appropriate for these tasks. Um and they're in various

For instance, they don't they're not covering the stateless guest anyway, but they um you know, they're maybe in different different some of them are in different states of maintenance and and they're not appropriate in other ways. Um we have proposed EVM sale, which would have the same nice properties of being extractable to different languages. Um Tao on my team uh built this uh and it it would If this could become a canonical spec, it would be nice, but it's not yet um at all. And there's some other work in progress like Alex Hicks, who I work with, uh has a lean pure lean implementation, which if we converge on lean for these tasks could could become the canonical spec.

Um so yeah, maybe for time I won't go too much into this. Derek covered it very well. Um but we had an experiment to write a guest directly in lean or sorry, in in RISC-V using like a lean layer on top of it. Um the a conclusion of that is that even though um it's executable and and plausibly, you know, could be optimized that we we're not able to prove compliance against even a a fixed spec there. And now there's another iteration uh using a language called pancake to try to make use of the formal verification of that compiler so we don't have to worry about the assembly and maybe focus on like a higher level description of the guest in this language pancake. Um but there's no compliance proof yet. Um and we have a

sort of some progress there where we're kind of proving um bounds on how much execution you have to put into a guest in EVM fast. And that's against the fixed pancake implementation again because of this spec ambiguity and the lack of a a baseline proof there. So there's a gap also of like what is the performance of the verifiable code. EVM ASM doesn't have good enough performance. Maybe it could be optimized. You know, we wouldn't expect something written in lean. If you trusted lean to see I don't think I would expect that to have sufficient performance.

So then there's the question of okay, well, if we need if performance is is paramount as it is here. I mean, this is a very constrained environment. We have to optimize these guests a lot. Then what can we do with like normal languages like Rust, C++, Zig, C Sharp? And the the fact is that it's a difficult task even if you trust the compiler and the compiler is another whole can of worms, I would say. So if we're not using safe Rust, which we aren't in the provers, we have runtime safety concerns as I've said.

But also runtime even for the the guest, which is what we're talking about now. So the guest could Oh, sorry. Yeah, so the guest could could crash inside of the ZKVM and give us a you know, we would not be able to prove execution of the of the block. So yeah, there are some we have some an intern who looked at these allocators. There are some questions about the safety there. And we would need in any case to go from the source code to the formal verification and we don't have tools for that yet. As I've said, they're being developed for Rust. I'm not aware of them anything that has a big uptake for Zig or C++ or C Sharp.

So another thing you could So okay, so then like it'd be great if we had formally verified compilers because that would solve the compiler bug problem or at least like could plausibly solve the compiler bug problem. We still want to stress test that of course. There is a C compiler, but we can't use it because of licensing and nobody has a C guest anyway. Maybe if they would let us use it, we could write the I don't know. We didn't ask. There's no it's kind of moot anyway. Um, there's this pancake language which does have a formally verified compiler. Um, and it's like kind of low level, but there's no runtime safety guarantee, so we we would have to prove that um, anyway. [snorts] Uh, here's a link to the that thing I've alluded to, the the guest in pancake for those interested.

Um, so what about the Rust compiler? Well, if that were formally verified, that'd be great, but it's not and it's a very big complicated thing built on a big complicated framework called LLVM. There's a long-term project to make a framework VEIR, which is like MLIR, but where you can prove statements about it's like a lean framework for making compilers. But that's, you know, potentially years away. I would love to be wrong and gladly would just use that. We have a kind of AI Slop project where we're turning the CraneLift compiler, which is a much simpler Rust project, Rust compiler into lean and then proving statements about that, um, which I can link to, but I mean that's super speculative and it would have to come a long way for us to

even consider using it, but we're kind of wondering how how much work it would take to get it there. We have found bugs in CraneLift um, doing this. There's no bare metal support for RISC-V. Maybe we'll vibe some up though. [snorts] Um, or there is there's sorry, there's RV64GC, but we need a more bare metal target, so we'd have to build that. Um, okay. And then finally, what about formal verification of binaries? Well, um, I've tried that, others have tried that. It's not there. There's no maintenance story, but we have some improvements um, coming from automation and we have now anthropic and theorem showing you can do it in some moderate complexity cases with enough tokens, but they don't have

compliance. They just have runtime safety um, guarantees except in one case. And that that's that they published those results only maybe a week or or Um, and we also like the maintenance story is the big question there. So yeah, to conclude, um, here is where II think we're at. Risk five and accelerator compliance and protocol correctness, I think that's all. We can count on that. Uh, seems pretty doable to me or like the recursive layer and the the verifier that will run um on in an attestor. I think we can have good guarantees there.

But really like quite open I think as guest compliance, standards compliance of the ZKVM standards, prover runtime safety, and then the sort of maintainability CI uh questions for all of this. So yeah, if you want to work with me on any of this, here are some links and uh thank you for your attention. >> [applause] >> Okay. Nice presentation. Let's take the first question. Cody, uh it's pretty sharp. Some ZKVMs like SP1 claimed in the past being formally verified, but later there was a soundness bug appeared. What do you think about the ZKVMs claiming false FV and can we

mitigate this type of >> Um, I'm I'm not aware of of this. I wrote a blog post that reported on a different kind of bug that it was not a soundness bug in uh the formally verified core of F of uh SP1. It was a completeness bug. And I think the the gap there was really about communication, about the guarantees. Um, you know, that you write sort of public facing blog posts. You It's a question of how um explicit can you be about what's there. There is code. You can look at it and that's how I found it. So I wouldn't I I I I wouldn't um you criticize them too much. I I I think maybe the the the um communication could have been better,

but it wasn't a soundness bug. It was They They didn't claim to exclude the kind of bug I found. >> Yeah, I I think probably there's a big gap between like sort of what the Persia present to the public and sort of what kind of the proof really shows an underlying for this kind of ZK-EVM. >> Yeah. >> Yeah. >> I mean the code's there. Like I looked at the code. It's there's no they're not hiding anything like >> Uh so by the way, if you want to ask questions, just scan the QR code there and all the questions go through the mirror cat. Uh the second question is like how much improvement we will get if we use something like EVM ASM since we already have the they

already have the EV, yeah. >> I mean there's there's like an hypothesis that you know if you have an AI write every line of assembly, then it ought to be better than a compiler. But I think we've just seen that that's simply not true and not not just in the EVM ASM setting, but somebody I don't know have a reference some guy on LinkedIn I saw him saying totally unrelated to Ethereum saying this. So I don't know that the question is really well formed. If if the I I read improvement as about performance, but if you mean in terms of security, I would say massive improvement in terms of security.

>> Yeah. Um and then the other question I do you think we will eventually migrate to RISC-V VM instead of EVM? Especially right now in the new roadmap, there's a lot of discussions on this kind of stuff. >> Yeah. That I view as being not too closely related to the work that we do. You still have to I mean it would be the guest program would yeah I mean like whatever your the compilers would produce smart contracts that are more similar to the ISA in which you're executing. I have not looked deeply into this nor have I but I have asked and I haven't

heard anything convincing in terms of performance. I think it's nice if you can use standard tools to write the smart contracts, but we have a whole ecosystem already and Solidity and I don't I don't have an opinion really Not from a security perspective. >> Uh >> Actually, you just mentioned there's a lot of existing firmware verification tools for different language, right? Like Rust. Like do you think this kind of recertify VM have better support compared to EVM? >> Yeah, I mean there's a question about you know existing like migrating users and what we have a lot of tools already.

But yeah, I mean again I don't really have an opinion. >> The next one will be what's the general cost per iteration for the verification? Because you mentioned about like people constantly change the code, right? And after developer change the code like typically how long and how much does it cost? >> Yeah, if that's a question like the overhead to developers to maintain formal verification right now I think it's very large. And the story to make it better is to create like better frameworks, have reliable extractors and I you I mean you need to put the

friction in place, have it in CI and then have the developers kind of dog I guess dog fooding is not quite the right word. But you have to sort of chew the glass >> Have a rough number? Like >> I don't know even what I don't to be honest not totally sure what the question's asking. In terms of like hours spent or >> Yeah, hours spent or like >> I I'm sorry I can't say a lot. Yeah. >> [laughter] >> A weeks or days or month? >> I mean I think a small change could probably be fixed with I'll just you just want me to say numbers. Like I have four six hours of of AI time could could make could fix a 10-line Rust PR change would

be my I'll I'll make that bet. >> Okay. Like the last question I think we will get like discussed later. Yeah, let's give another round of applause for Cody for his presentation on the QA. Um, and we will sort of >> [music]