Formal Verification and the Holy Grail of Software Correctness

Transcript

Okay, hello hello everybody. I'm Charles Cooper. I'm the lead developer of Viper. And today I want to talk about this very fun title which is the holy grail of software correctness. Formal verification and how we make sure that everything is correct. So first of all, what is formal verification? Quick background for people who aren't familiar. Formal verification is basically the use of mathematically rigorous techniques, logic, logical steps to prove that software is correct. So we want software to meet this is kind of a philosophical question, right? Like what does it mean for software to be correct and let's just say that we want it to meet a

certain specification. So we have a bunch of code. How do we know that the sum of the user balances always equals the total supply? There's an ERC-20 kind of standard exercise. Users cannot withdraw more than they deposited. People can't lose money. Only authorized parties ACL access control. Like how do we So we have a bunch of code. How do we know that it actually satisfies these properties? So in many safety-critical industries by the way including DeFi we formal verification techniques formal methods are used to kind of prove software correctness.

And I think that in DeFi as you know TVL grows or sometimes it gets lower as this year but as TVL grows and like we want to become more credible to the outside world or the every all other industries we want to have very good techniques for showing that software is correct. And especially in in age of AI where replicating hacks for example last year I'll talk about this a bit later but after the balancer hack last year why ETH was probably AI assisted as according to Twitter analysts because they use similar kind of

techniques exploiting some rounding issues. So in web 3 the gold standard for like a protocol is like that it's been audited. And I'm over simplifying maybe but because people also use formal techniques Certora is a very famous auditor that uses formal techniques. And the issue with kind of just reading code and reading about it is that you can find bugs but you can't really prove their absence which is kind of crazy.

And also auditing is hard. Typically you want to if you're an auditor you have limited scope of time that you can like actually work on it. So you I know there's many auditors in the audience so so I want to be fair but like you want to like look at the source code, right? Like you're not going to be thinking about the compiler. You're not going to really be reasoning about the the byte code usually. I mean some people do if there's a a really fancy audit say big deal protocols are going to pay auditors extra to like also verify the byte code.

But I mean we want to kind of break it down into two parts, right? So we want to show that the the source code satisfies the properties that you want and we also want to show that the actual byte code. Which is that the actual artifact the thing that's actually running on chain also preserves those properties. >> [snorts] >> So um the compiler part I want to address. So as many of you may know Viper which I'm responsible for had a compiler bug three years ago now two and a half years.

And that was in the non-reentrant implementation. A lot of the funds were recovered but not all. And so this is kind of a a wake-up call to everybody that like even if you like are positive 100% that the the source code is correct the compiler can still have a bug. And that is kind of really what pushed us to look at more rigorous methods for like making sure that the compiler is correct. So that's why I'm here to talk about formally verifying the compiler and also formally verifying source code.

>> [snorts] >> So what we're doing is in the style of I guess CakeML and CompCert which is like we have an optimizing compiler and we actually want to prove that it how do I say this? It preserves semantic correctness. So you have a definitional interpreter. So you have formal semantics of the language which is like you define what the language is supposed to mean. And then the compiler is the the program that translates source code to byte code and you prove that at every step every step of the compiler going from source code to IR optimizing the IR and going from IR to byte code each step is semantics

preserving individually and transitively they compose into a semantics preserving function. And yeah so as a detail we're using the Verifier formalization of EVM. So and that is a >> [clears throat] >> I guess you can think of it it's kind of simple, right? Because the EVM is simple. It does pass East which is a fairly hard bar. So you can think of that as like kind of a part of the trusted computing base but which has also been extensively tested.

Um the the the reason it's part of the trusted computing base is because like the the clients that are running the EVM on the network can maybe actually be running a different EVM and you wouldn't really know that until you like hit some specific block. And this this is this is kind of similar to a consensus failure, right? Like the clients in general can disagree on like what the EVM is. And actually I was curious if anybody knows like what happens if there's a difference between yields like the execution specs and like probably the majority client go Ethereum.

So if you know the answer come find me afterwards cuz I'm very interested to find out what happens >> [laughter] >> if they disagree. Okay and the current status here's a QR code for you to kind of investigate our progress. Um So the two previous compilers that I mentioned CompCert and CakeML are for C and Standard ML respectively. This is to our knowledge the first formally verified compiler for smart contracts. And we have like completed the design and we're in the middle of the proofs.

They're almost done. I promise. It's kind of like a lot of code and a lot of work but we're making I'd say very fast progress compared to what would have been possible before the age of AI and I'll talk about that a little bit more later. But okay now that we've talked about the verifying compiler we're also interested in actually like like okay verified compiler is very cool, right? You know that the compiler is correct but like now you want to actually prove things about Viper programs, right? User programs. So um here's a list of like common exploit

vectors. It's by no means exhaustive. We're not trying to pick on anybody but like there's just like millions of like failure modes, right? You know like and rounding rounding errors are like a really interesting one because they're very difficult to reason about in general. Both for humans and also um for AI and also formally. Um So it's kind of an interesting case because uh often times you have like a function that you know is like correct in the like the the continuous real valued form is correct but once you start doing like losing precision due to division integer division then like

all it can be very unintuitive. Like you can like have rounding that like errors that kind of compound and explode and then bad things happen. But that's just an example like we our goal is to be able to prove like any useful and interesting thing that you want to know about a protocol's logic. So here's a kind of case study Snake Mate. It's a third-party library kind of standardly standard used library for Viper. And we looked at the the math library which has a bunch of stuff in it including muldiv which is like 512-bit muldiv operation.

It has transcendental functions logarithm the natural log exponential it also has cube root and the implementation is using a Newton-Raphson iteration. And these are kind of interesting functions because we know how they behave in the continuous domain but as I mentioned before like rounding errors are very hard to reason about. It's an approximation. So you want to like be able to very you want to be able to formally define or characterize how the approximation behaves with respect to the real function.

And if like these functions don't behave like you want them to then you can lose money. I hope the reason for that is clear but basically it's like if you have some math function that like defines like how much two LPs are supposed to get in a trade or something. And like the math function is wrong, then that can be exploited. And by wrong, I guess the uh doesn't match expectations. Um so, uh here's one of the functions. This is uh What is this? Log the natural log, right? And this is like Yeah, this is cool, right?

>> [laughter] >> Uh we've got all these constants. Uh we have all these like the weird I mean, it's some kind of expansion. Uh I don't know exactly what expansion is. It's like not Taylor, something more fast or something. Um but like yeah, look at this. How do you know if it's correct? Like raise your hand if you know. >> [laughter] >> Um and the interesting thing is that it is. Uh this was a bit surprising to me, uh which is that the error with respect to the real valued natural log function uh is bounded by three halves of a of a watt.

Um so, this is the theorem statement in Hall 4, which is the the um prover language that we're using. And you can actually prove this. It's a quite a long proof and it uses some very interesting techniques. Um but it's provable. Um this was the case for uh almost all of the functions in Snake Make that we found, actually. Um uh that they're like bounded very accurately um by the function. Or sorry, by some error. Um except for the exponential function. And the interesting thing about that is that it actually grows with the input. So, um E of X for a very large X can diverge

from the real valued um E of X by um a constant factor, actually. Um so, and if you think about it, it makes sense because like you you you just can't get enough um um precision in the domain in order to get precision in the output. Um so, here's another thing we're working on, which we're we're kind of excited to announce, uh which is that we're working with Curve Finance to do something more practical. Uh which is kind of like Okay, so let's look at this function. Oops.

Back. Okay, uh back again. Whatever. Uh but everybody pretend they remember the natural log definition. Uh it's kind of cool, right? It's a function that you can use, but like it's not a it's not really an end-to-end program. Like it's a building block that you might use in your protocol. Um but like in in real life, you want something that is about a real program. Uh and so, this is about the stable swap implementation. And uh what we're doing is proving that users can never lose funds. And this is a kind of uh you can think of it as being exhaustive. So, the the the theorem statement is that there exists no entry point into the contract where users can

lose funds. And the way it's stated is in terms of virtual price. So, if you're familiar with uh Curve code, that basically means like the user balances. Uh so, it means that like the users can never lose money via a rounding error is how you can think of it. Uh as everybody knows, you can like lose money in AMMs through impermanent loss, but that's not what we're characterizing. We're like characterizing that you can't lose money in an unexpected way. Um and this is actually uh this is simplified a bit. Uh but basically, we're saying that like if you run uh if you call the stable swap contract on the pre-state and you and this is the post-state, then like the virtual price of the post-state is

at least the virtual price of the pre-state. Uh which is a succinct uh definition of users never lose funds. Uh so, we're very excited to finish proving this and announce the results. And I think this is like kind of uh everybody's like nightmare, right? Is the opposite of this. Uh so, you like put your funds in a protocol, it's been audited, but like you don't really know all the edge cases. So, this is like uh uh uh kind of the contrapositive statement, which is like there is no edge case for which users lose funds.

Um Okay, um how much time do I have? 5 minutes, perfect. Um so, this is a little bit extra for anybody who's kind of interested in theorem provers. Um SMT solvers are uh generally a little bit limited in expressive expressivity. Um for example, they have trouble with for loops. Um uh the reason I wanted to look at the these functions, the log exp cube root mul div, is because in Snake Make, there's some Halmos tests uh which are like uh not proving about uh boundedness, like the error bounds of the functions, but they're proving that the um

the Viper uh implementation is equal to the Solidity implementation. And the the solver that Halmos uses in this case, Yices 2, is like it like can't solve it. It times out, runs out of memory. And so uh we're very happy to say that we're able to solve it. Um and this is kind of like a detail, but there's other theorem provers, Lean, um it's now renamed to Rock Isabelle um LCF architecture for if that means anything to anybody. Um It does to me and maybe some other like nerds but uh they're they're conceptually all kind of

similar. Um They're they have some higher order logic and they're expressive enough that you can prove kind of I I would say like anything useful that you want to say about a about software. Um and the differences are mainly in tooling, uh the community. Uh we have actually been submitting some stuff upstream to Hall 4. Um which um >> [snorts] >> makes um the experience better for agents. Um so, uh this ties into the context of like we're in the age of AI, right? Um AI-assisted hacks are getting better.

AI is writing more code. How do we verify all the AI code? And uh what we need to do uh uh is basically boil down all of software to the things that you need to know, which is what is the software supposed to do and how do I know it's correct? And that happens when you have um well-specified uh contracts and you have a theorem prover. And actually, we're working on a prover agent, which will do these proofs for you, so that all you need to do is think about like uh what does it mean for my software to be correct? And then the end goal is you push a button and then you know it's correct. And uh we believe that this uh scales to other languages, not just

Viper. C, uh these are some kind of like well-known uh high-assurance languages, C, Cobol, and Ada. So, um I want to go to the last page first, which is cut off. Okay, so those are our socials. Um the other page uh Well, you can book a call with us or reach out to us on Telegram. Um and I'm happy to take questions. >> [applause] >> How do you go from the theorem to the to the actual proof?

Uh So, the question is how do you go from the theorem to the actual proof? Uh well, you ask the prover agent to prove it. >> [laughter] >> Uh Is that your question, like how do you actually produce the proof? Uh yeah, you I I can describe the architecture of it. So, generally, what you want is like a an easy-to-understand model of your code. Uh so, for example, the Snake Make properties that we're proving are things like it approximates the real valued function. And the real valued function is something that can be expressed in Hall 4. Um which is kind of crazy because like some of these like real numbers are like not actually representable. Um but you know, it's like a Taylor expansion and it has a mathematical representation. Um

So, you have that model, which is like some Hall 4 function, and then you need to prove that it's equivalent to the source code. And basically, you need to prove that into it's called simulation. So, you if you run the program through the interpreter simulation, then it matches the the pure function that you've defined. Uh and the correctness properties can also be like this function is monotone. Um or like uh this function only ever touches these storage slots. Uh-huh. And then um Yeah, and then the the proof propagates to the bytecode by the compiler verification proof.

Hey, thank you and nice talk. Um So, I'm just wondering how much time have you actually spent uh building the verified compiler? And and if you could you extrapolate that to how long it might take to build a verified Solidity compiler? Uh I'm not really going to comment on building a Solidity compiler because I'm not familiar with that compiler. Um It took about, let's say, a year to define the formal semantics for Viper. And then since December, work has been progressing more much more quickly. Um Like 3 months to get to 98%.

Yeah. Um CompCert took 15 years. So, we are really are in a new era. Um can I ask how low-level you've done the verification for? Is this just machine code or do you go down to register transfer level or even lower? Uh so, we prove equivalence with the EVM bytecode. So, we have the like I mentioned earlier, there's the the EVM model in which is Verifierium. Uh which is an EVM implementation you can live it as.

Uh it passes East. So, at the proof is that the the bytecode semantics is equivalent to the uh the the the Viper semantics as we've defined it formally. Does that answer your question? And that includes all the optimizations. So, including like lowering to like EVM operations memory um stack spilling, and all this stuff. Um Yeah, so it includes like correctness of the stack spilling algorithm, um all of the optimizations, control flow stuff. Yeah. Semantics preserving.

Okay. Um I'm around all day. Um feel free to come talk to me. Uh oh, uh I didn't put my Telegram here or Twitter, but it's big_tech_sux.