Panel Discussion: Formal Verification & Fuzzing moderated by Alexander Hicks, Ethereum Foundation

Transcript

Uh next we've got a a panel discussion on formal verification and fuzzing. Uh moderating the panel is going to be Alexander Hicks who leads the protocol snarkification team at the EF. Uh also leads the uh formally verified EVM project $20 million grant uh program that is doing a lot of amazing research. Uh, also from the EF is Cody Gunton, uh, security lead on the ZKVM team. Uh, Valentin Worust from Diligence Security, Devin Tuma from Succinct, and Costa Ferrellless from Veradise. Um, gentlemen, check. Check. It works.

Okay, so just for the record, [clears throat] I can't see the timer, so if we go over time, just buzz me. Uh, but yeah, thanks everyone for coming. It's obviously been a fantastic day of talks so far. We've had formifications has been mentioned a couple times in the more general security uh discussion about security and harding ZKVMs and reliability and all of this. We have a fantastic panel that actually covers a lot of different aspects of formal methods. So we've got Valentine over there who does a lot of fuzzing. Cody has been doing some compliance testing and some fuzzing. Devon uh does a lot of work in lean it with uh proof assistance I guess and the manual start of for verification and then costas has been doing a lot of automated verification

wizards and to solve this. Uh so first maybe everyone on the panel can uh quickly introduce themselves. You have about you know 30 seconds to a minute to shill whatever you want and then we'll get in a chillfree discussion. >> Right. Should I start? Okay. I'm Costas. I'm the CEO of Verice. Uh so we do a lot of auditing uh but uh more related to this panel we recently released audit hub which uh has a set of formal method tools that uh already some of the zkdms in this room are using while they develop uh to find bugs and uh yeah finally in collaboration with the foundation we also uh created LLK which is an intermediate representation that tries to unify the development of uh ZK

circuits. So that way like everybody is benefiting from other people's work and like you know people can get our tools uh if they lower the circuits to LLCK. >> Uh I'm Devon uh at Succinct. have been working on uh verifying the circuit logic and I'm also a PhD student at Minnesota and I've been working on formally verified cryptography there and I've gotten involved a lot with Alex's um work to formalize uh the proof systems and the actual underlying cryptographic arguments. Um so both of those things have been uh happening in lean a proof assistant. Uh I think proof assistants are uh the way forward. I think they can do a lot of great things.

Um, so I'm glad that the EF has really invested in this. >> I'm [clears throat] Cody Gunen. I'm a member of the ZKVM team at the Ethereum Foundation. Uh, my work has mostly focused on security of these systems. Uh, compliance testing for risk 5 compliance tests. Um, this also sort of tracks progress on ISA's changes to them. And some fuzzing work. I built a risk five fuzzer. that some grantees are developing further and I've also built a plunky 3 verifier fuzzer. Um, and yeah, I'll be helping to coordinate the efforts for security more more broadly

on top of digging into a bit myself. >> Uh, yeah, I'm Valentin. I'm a researcher at uh, Diligence Security. Um uh we've been kind of doing a lot of fuzzing over the last two years. Uh focusing on various ZK infrastructure projects. Um so we've built two three different fuzzers. U one fuzzer um targets kind of languages like Noir and Circum trying to find bugs uh there. So it's already found like something like 20 different soundness or completeness bugs in various um tools. And um now recently we also started looking at CKVMs. Um we

have built another uh fuzzer there uh that has already found uh something like 11 uh soundness and complete or completeness bugs. Um three of them uh were soundness bugs. Um yeah. >> Okay. So I think it's quite an interesting time to discuss form verification uh and formal methods and fuzzing and testing and all of this in general. first because obviously we have ZKVMs which are hitting big performance milestones. So that means we're getting closer and closer to deploying them which means we should be feeling closer and closer to sleeping well as Ron would put it. Uh and because it's quite a huge complex stack where you know most likely the ability of audits to really figure things out is quite limited and we've

definitely seen obviously bugs happen to you know fairly heavily audited code bases u but also because we've also reached several milestones in terms of form verification and fuzzing. So as Vanathan just mentioned, you found several soundness and complete issues in ZKVMs. Uh we've had Devon was part of the first effort to formally verify a risk 5 circuit and they've done so successfully obviously in collaboration with NES and then on coster side with Veradise they were obviously I guess one of the first to apply SM solvers to some of the pre-ompiles and circuits that you see in ZKVMs and showing determinism you know in a way that can be integrated into CI uh which was with zero. So I think we can all agree that security is great, formation is great, we should do

it, so on and so forth. It's extremely bland. Uh what is probably much more interesting is to try and figure out how do we actually do it and how do we actually try to get coverage over the entire stack because the stack is pretty big. uh as the first panel today hinted you know there were some suggestions that now that we're hitting performance milestones you know the next sprint is going to be about security and it's going to be about trying to solve all of this getting obviously provable security on you know the side of cryptography uh but also more generally about the huge software stack that we have to cover and we have a variety of panelists who are working with a variety of tools that all have different trade-offs and I don't think we want to argue that any tool is best I don't think either of us think

that any tool is best even if we have preferences about using lean uh but I do think we want to argue about maybe you know how do we make this complimentary because maybe where there is some friction is both in the fact that we don't have good integration of fuzzing in form verification within uh ZKVM development teams maybe with the exception of succinct who have devon and we also don't have good integration between people using different tools uh so maybe let's you know start on on that angle of you know how do we get a lot of that friction away and actually speed up all of this.

>> Uh I can start. Yeah. Uh so I guess like you know as you mentioned yeah like there we all of us cover different parts of the stack right and then like you know each of our tools has kind of like their strong suits and like you know somewhere that they don't work very well. So I think first of all we need all of us to start talking the same language right because as we mentioned earlier LLCK came to kind of like you know uh bring some unity in the fragmented kind of like space of ZK DSLs and ZK languages and I think it's a perfect vehicle for you know our tools to also start like you know uh talking the same language

and then like you know start combining techniques like you know fuzzing which like you know I think might also benefit from specifications and also like you know the same for uh theorem like automated theorem proving and like you know uh proof assistance and like you know people in our kind of like branch of academia have kind of like you know been doing that for a long time where like you know you have a part of the system that is kind of like you know being verified like you know automatically and then like you know it gets stuck at some point and then like you know somebody provides an action and like you then the whole thing becames becomes push button again.

Yeah, I guess I would mention that yeah, having multiple tools uh even if they overlap in places is also like very useful. Uh like when we [clears throat] work with Veradise has found bugs in our code at least a specific bug before you know weeks before I even started getting to the actual formal verification in lean proof assistant of that because it moves much slower. Uh so having like automatic tools that can give quick feedback um and then also slower more stronger verification is also I think very helpful. Um I think the tools are additive right you can only make things more secure you can never have besides resource usage and you know being able

to actually do it having more tools is is very positive I think. Yeah, I mean my mind goes to where the teams uh spend their time and where they spend their time is determined uh you know by the overall direction of this project the ZK EVM scaling project and you know events like this I mean we've pushed really hard on performance and that means that there's less time toward integrating security tooling building security tooling or you know accepting um external contributions by the way Please merge my PRs um when they when they come your way. Um >> who's not merging?

>> Huh? >> Who hasn't merged your PRs? >> Call them out. >> I'll I'll uh I'll do my third emoji react there. Approval but non-merging comment. Um yeah. [clears throat] So I think that yeah, I I would like to just see an overall shift in the emphasis. Um I mean it's good to bounce between different fosi, right? Like you have performance, you have a security sprint, you have a kind of cleanup sprint. So I think that that can help. Um yeah so I can me maybe mention um how we've so as I said we basically started with a fuzzer that was targeting not CKMs uh specifically and there we have a lot of experience working with the linear team um so we used to be in in consensus until a few months ago and

there we worked very closely with the linear team in particular with the team um we have been essentially fuzzing uh their um their system for more than a year now um continuously. So and they there you usually try to kind of uh keep basically put as little burden on them as possible. So the way that we use we're doing this um is by essentially running like a once a day we kick off a fuzzing job and then every morning or whatever when they wake up they get essentially like um a message just telling them you know everything's good and if if not we will kind of try to provide a minimized counter example try to give them a test and that they can

use for essentially reproducing the bug and fixing it and this has been uh very successful in my And the team also has been yeah very receptive of this kind of way of collaborating with um our team but also with the fuzzer. Um yeah so I think following on this how do you see things going in terms of an end stage of ZKVM security efforts? Do you see it going where you know are we aiming to get every single line of code of every ZKVM of every guest program you know all kind of formally verified in lean which you know if you have an infinity of guest programs is maybe unrealistic

uh you know same with SMTs with fuzzing like where do you see the kind of ideal end state of all of this in terms of combinations of tools running on different parts or running on the same parts but on different timelines and different levels of integration with CI uh if you if you have you know a wish list or of where you want to see things go. >> I mean, I think like from my uh perspective, I think it's it's quite likely that, you know, we will there will always be some gaps um somewhere. Um but I think the point should be to h to use the tools that we have in the most effective way to cover like basically have like several nets of of security. So for instance, I can say from like our fuzzers, we essentially target kind of like the whole system. So

we basically we try to cover all the the components. Um but obviously like there can be specialized uh ways to target individual components more more thoroughly than what we're doing for this the entire system. So I think this is really an opportunity to kind of combine different tools and then give us more confidence that these tools are actually ready to to be deployed and to go live. Um, I place a I mean audits aren't a silver bullet. Nothing is, but I I think they're very valuable still. I mean, things can be missed, but many things are not missed. I mean, the teams do very good jobs auditing. Um, and so I don't know, as an end state, I mean, I

imagine you sort of releases uh with periods of open bug bounties and auditing and attention, you know, careful attention to big changes. um you would know best about the sort of potential realistic scope of these FV tools, but I mean it seems like things are coming along extremely well actually in there. So bullish on that. >> Yeah, I mean I think to get the proofs the you know the different verifications to cover everything well. It is also important to acknowledge like the limitations and the trust assumptions you have in everything you do. like there's there's many assumptions we need to make in order to verify our circuits, for example, and clearly stating those.

Also being, you know, conscious of things you might miss. Uh if we don't know exactly what each tool is covering, it can be easy to, you know, not fully cover the surface. Uh so I think just being really honest about limitations or strengths of >> but I think that's not only from the tools themselves but also from being able to work off of common representations >> so that you don't have gap off of whatever representation you're feeding into each tools. >> Yes. >> Which is a maybe tricky part. >> Yeah. And like from my perspective is like I don't know my my ideal world like you know moving forward is that like you know uh have kind of like a very thorough security checklist right and then kind of like assign tools to take as many items as possible from that

security checklist. Uh and then like you know of course the end of the day we're going to have like you know some aspects that are formally verified. Uh but like you know we need to kind of like you know push automation as much as possible uh in my opinion and then like you know also auditing like this type of like you know very complex systems manually is a nightmare and internally from like you know our experiences or our experiences from auditing some of these manually before having the the tooling infrastructures.

Uh now that we switch to a model where like you know we have a tool to assist us like we feel like you know way better to the extent that like you know if a new tech stack approach uses to kind of like you know uh audit their circuits manually. We offer them initially to kind of like integrate uh our uh formal verifier picos to kind of like you know take a huge mental load uh off of the auditor. Uh and then like you know we're also happy that you know we're seeing teams like succinct and like you know risk zero kind of like integrating our tools into their uh CI/CD while they're in develop so they can you know detect like you know bugs

as they arise and kind of like you know removing items from like you know the that like checklist. So I think I have I think two points I want to come on the panel stool and one of them follows directly on this uh which is that indeed auditing is very standard as I've already said it's you know with the complexity of what we're looking at it seems very hard to audit it also seems as economically based on numbers that I'm hearing about the cost of auditing uh which I can only you know assume that I'm getting correct numbers and based on the numbers in terms of what it takes to formize something for which I have the very exact numbers it seems to me that also audit eding is becoming both economically and timewise inefficient compared to the progress that we're seeing in you know better testing and

fuzzing and SMT solvers and proof assistance. So I think maybe you obviously have a view because your business does both and I guess maybe on you know your side as well you have a view where you kind of do both and I think maybe on the success side you you know have paid for audits so you maybe have a view as well. Uh do you have I mean do you have a sense of you know not just where audits fit but but also where you think you know we have a lot of this a lot of these audits are being done with finding critical vulnerabilities in code bases have been audited audits also maybe are not kind of forcing functions if an issue is found. We've seen this with plunk history and you know the the fry verifier skipping the degree check.

Um yeah, what does it look like to try and get more representation of formal methods and you know in places where auditing hasn't been enough? Uh and as part of that you know potentially getting to the point where or we're providing higher assurances in a shorter amount of time in a way that's maybe more robust you know to changes as well. So I mean like the whole thesis of our company is that like you know uh manual auditing like you know it's not enough and like you know we that's why we have been spending so much time like you know building like you know these tools not only for ZK but like you know for other uh ecosystems uh as well uh like I agree that like you know auditing like I mean in this industry right like

it's a time boxed uh endeavor right like you essentially set up a timeline you set up a scope there is a lot of back back and forth to kind of like you know negotiate both the scope and the duration uh of the audit and then you kind of like you know uh reach to something that is of course suboptimal because there are constraints from both ends right constraints from the client on their budget and constraints from our side uh for like you know how much we can dedicate for like you know a single uh client so uh yeah I mean like you know for us like you know going the formal how kind of like you know way forward is why we started the company to begin with and we are really excited

that like you know they start happening in the ZK space and you know uh specifically in the you know ZKVM uh subword of like you know the ZK development. >> Yeah, I mean I think it also having the formal verification I would think would make the auditing easier and probably shorter, cheaper. I would I would hope uh like our circuits if the auditor can just look at here's the assumptions in the lean and we have a full proof [snorts] of all the arithmetic ideally they don't need to go through the math proof themselves right so even if you can just cut down a lot in that way I think that's also valuable in in reducing the problems with it uh

>> I'm not totally clear on the full optimist picture of what formal verification gives but I mean does it does it cover CUDA kernels Not yet. >> Yeah. So I mean that's a lot of what that's where all the complexity's gone for the past four months. >> But a a lot of vets are not just looking at the cuda kernels. >> Say what? >> A lot of vets are not looking at the cuda kernels. >> Well that's that's really a shame. I think [laughter] maybe maybe they should. >> They should. >> Yeah. Yeah. >> And we should fuzz them. >> Yeah. I mean the pessimist case is that you know you build these tools but they're so rigid or they break so frequently that people don't maintain this formal verification and invariant and there's a lag and they don't actually I mean if if we find and we did

hear in a conversation earlier that oftentimes the proofs don't break even under what seem like complex changes. So for me, I don't have an opinion until I I have some more personal experience and hear more from teams about. But I think that um yeah, I don't I don't back down from the idea that people reading code and teams reading their own code at some point is incredibly important. >> Writing tests. >> Yeah. Yeah, I mean I think the there's there's a lot of um there's a lot of tools, different approaches um and we yeah we we should we should kind of use them in the way that they they fit best into the the workflow. So from what I've

seen um in my in my experience is that you know building a building a fuzzer is not I mean it's it's something you can do in you know like a simple prototype is something you can build in you know maybe a month or something just to kind of and you're getting essentially results like pretty quickly. Um, and I think this is definitely something that, yeah, makes makes a lot of sense and also gives you some I mean it doesn't give you the guarantees that you maybe get with formal verification, but it gives you some um reassurance that you know at least you're there's no nothing like um yeah, there's nothing completely off in your system. And um and then afterwards once you know what what

properties you actually um want to test uh then you can kind of move further down the the sort of the stack like you can do formal verification you can do audits and so on but I think in many in many cases like even the like the formal properties that you want to check are not like they're yeah the specs are not there usually and they have to be developed and there's obviously also room to have specs that are not quite right. I mean, this is I mean, I've done formal verification in the past. I mean, this is always the case, right? You you rewrite the specs and uh in many cases, you realize, oh, the spec is actually off in some way. So, you need to go back

and fix it. And this is a perfectly normal experience, but it it obviously takes a lot of time to kind of do this iterative process. Um so yeah that's why I think makes some sense to kind of start with things that are more lightweight and then kind of move towards more expensive and more also um yeah more time consuming um yeah sort of safety measures um further down the f further down the line. Right. By the way, just to defend our former verification team, uh like we have like something that like you know can run without giving it the specification.

It's like a prof and it's not like like that heavy weight. So I think I agree fuzzing is it is it has its place but like also I think like you know formal tools that like you know combine like you know static analysis and verification that can run kind of like effectively they do also have like you know their position early on in the development cycle. I mean having shared specs is also very useful. When I first was working on this at succinct, we were sort of writing our own specs and then Alex, I think it was Cambridge, >> Cambridge and Gwa >> uh had the back end for sale. So now we can sort of trust the spec more or at least more people using the spec means more eyes on the spec. Things like that I think is also really helpful. Teams

writing their own internal specs for everything is probably not good uh at all for anyone. [snorts] And then so as I guess on this mention of you know iterating and going through the motions a big part of I think integrating any of this successfully is trying to get it to run in tandem with development both for the reasons that you don't want people to be pushing you know performance optimizations but you need to delay deploying them by x amount of time because you need x amount of time to do audits and verification and fuzzing and testing and all of this. Um, two also because like you're saying if you have things that are lightweight, you can actually use them, you know, maybe on every PR whilst we're developing things to catch bugs early to hopefully help

actually your development process. If anyone has seen any past talks by me, at some point I always have a slide that references a blog from AWS that goes on about how they're getting they're shipping faster, better code because they've integrated fuzzing and SMTs and manual form verification in their process. That's with the caveat that they have 100 people doing for verification at AWS where we have less than 100 people doing it in the entire ecosystem. Um but but I think I person there there's a big view of for version of this is like you know we have to slow down to be able to do it. I actually quite enjoy taking risk. I would rather see people do like super sketchy stuff and work really hard to be able to like actually make this not sketchy. So if anything I want people to accelerate

even more. Um I think what can we do you know to make these tools that we have and that we're developing you know more robust so that we can actually run them on every PR and instead of just being you know maybe just a security thing we can try to see them as you know ways to actually try to drive performance engineering and we don't have a performance engineer on the panel to like give us feature requests uh but maybe we do have a sense of you know how how we can integrate these to get quick feedback to maybe get clues as to how to make things simpler flow, how to make things faster, how to make things more efficient. Uh, which at the end of the day, I think is what matters first and foremost is no point having something secure but slow.

>> I mean, engineering teams do not want extremely heavyweight CI on every PR and they they shouldn't have it. It's like it's not good. So, I think nightly jobs or >> you can do performance engineering on SMT solvers to get faster feedback. >> Yeah. Yeah. I mean, it's it all just it depends how heavy it is and how long, you know, how flaky it is, these kinds of things. But also I think what's the kind of feedback that the tools can provide because it's one thing if you have a tool that says okay we caught a bug in this you know PR you're making on this branch I think it's one thing and there's another thing which is you know for example with writing specs a lot of times writing specs you know forces you to try to reason about your code and you just end up finding optimizations as a

result right in the same way when you try to write down some idea on paper you know suddenly you figure out you know that you need to think a bit more about your idea and when you try to implement it in code you figure out you need to think a bit more about what you run on paper. >> Yeah. >> And and then when you try to write specs when you try to run when you try to set up you know tools at the start of your development process maybe rather than at the end you know is there some gain. >> I think just like something granular of course helps here right so if you can just reproof some part of it and you have something built where you kind of just maintain this one proof and then it propagates you don't have to check the

rest this is good or like you know when certain files change you run a nightly fuzzer job. Uh that that makes sense to me for sure. But I Yeah. >> So, we've got some audience questions here. Uh, letting you guys cook for a little while. We're at time, but um, mind if I just throw a couple of these up? Yep. Okay, great. Um, are there any efforts to fully certify compile the compiler pipeline due to concerns of LLVM being the target and op uh, being the target and optimization leading to unsoundness of elf binaries?

>> Uh, I have two answers. >> Okay. One is that LLVM to risk 5 specifically there is an ongoing form refiction project around this happening in Cambridge. I have a draft paper I'm not allowed to share. Uh but it's happening uh not the entire LVM yet but a significant portion of LVMIR. Uh and two I think there's something very interesting to say about compilers in the context of ZKVMs which is that you have you want a general purpose compiler for the guest program. So if you're running rest as your guest program, you probably want to run this through the Rust compiler. And I don't think we want to try and rewrite the Rust compiler.

And formally verifying the Rust compiler was something that at some point DARPA was talking about doing and then Trump happened and so it's not happening. Um but for things like circuits and provers and verifiers, you can probably do with quite a minimal compiler which can both support uh optimizations that are probably not in the Rust compiler because they benefit from representing your program with a high level of structure for any algebraic optimizations or anything like this. And two, the range of things that they operate on and the range of operations that they do is very constrained to get compared to everything that is in LVMIR or just mainstream, you know, kind of monolithic compilers. So we can I do want to maybe bet that we can write

compilers that are quite a minimal to form verification and can produce, you know, maybe faster verifiers and better circuits, potentially even faster provers than we currently have. Uh I want to say maybe 2027 ace proof day next year wherever DevCon is. I can give an update on that but we we would like to attempt this. >> Excellent. >> I actually have a funny anecdote about this. So the first bug that we found with um with our Argus fuzzer for ZKVMs was actually um it was actually a compiler bug. So we were like very very excited. I found the first bug and [snorts] then we we shared it with the team and they they debugged it. They actually figured out that they've been

using a slightly outdated uh Rust version. Uh and there was a bug in that Rust version that the the father actually found. But yeah, [laughter] >> this is the thing that keeps me up at night. It's not bad for security. The com the compiler is extremely scary. Yeah. >> Then a quick final question. Um why do you have to formally verify the prover? Isn't having a robust verifier sufficient for safety? So the verifier gives you soundness. The prover gives you completeness. Technically speaking, completeness of the proof system is deterministic for something like fry. Um but obviously if the prover is not able to generate a valid witness or just, you know, panics for some reason,

>> uh you might then have a livveness issue on the L1 because you won't have you know a proof to be verified. And so you would want to avoid that. Uh but obviously as was hinted by uh Cody, we're not currently aiming to formally verify handwritten custom CUDA kernels uh because we lack the tooling to do so. So I think for that it will be a lot of yeah testing and hopefully at least fuzzing. >> Excellent. Thank you all so much. Um, we've got a short break now and then the last the last chunk of programming, it's going to be uh keynote presentations from the five real-time proving teams that were up here on stage earlier, plus a really special presentation from Jolt uh the A16Z um ZK VM that's being developed and

coming to Ethroof soon. And then our final prover final panel who pays the provers. Um, I'll see you back here at the half hour.