Formally Verifying Morpho

Transcript

So, hello everyone and thank you for joining production. Um so, yeah, I'll be I'll be talking about formal verification and about Morpho and I think that formal verification will become more and more important as time goes by in the device space. And I'd say the same thing for Morpho, so I thought it would be a great opportunity to to talk about both. So, I won't assume any knowledge about formal verification. Uh but my promise is this, by the talk you you will know what formal verification is or at least you will have a sense and an intuition of what it is.

And you would have seen examples of formal verification being applied to DeFi and being applied to to Morpho. All right, so first what's Morpho? So, Morpho is a peer-to-peer layer over lending pools. So, we call that Morpho optimizers. Um and so, you have one instance of a Morpho optimizer for each pool. So, one for compound V2, one for RVV2, one for for RVV3. And what Morpho optimizer accomplishes is that you have the same risk parameters as the underlying pool.

You have the same liquidity, but you have improved rates. So, how can it do that? Well, in the lending pool setting, you have this pool supply APY and this pool borrow APY. And the fact is that the pool supply APY is lower than the the pool borrow APY. And the reason for that, the main reason for that is that you have less borrowers than you have suppliers. So, all the the interest generated by the borrowers, they are split among the suppliers. And that's the main reason for the spread. But in Morpho, you have a peer-to-peer layer, which means that for the matched amounts, you have the same amount on both sides. And so, you can decide the rates. And you could and what Morpho optimizers do is that they put the rate in the middle. Which

means that win it's a win for the borrowers because they they pay less interest and it's a win for the suppliers because they they earn more. All right, and then you need to have a fallback in case one of the party exits. And you also need to have a fallback that is in in constant gas. And that's not so easy to do. So, that's the the delta mechanism. So, we have plenty of documentation. You have a we have a yellow paper that is available also. And more broadly, if you're interested about any of the stuff that I'll describe in this talk, you can find it online. Everything is open source.

And there's one last thing I I didn't talk about in for Morpho optimizers is that it's a layer on top, but it means that you have additional contracts. And so, it necessarily means that you have additional risks. The smart contract risks. And this this is why you have an emphasis on on security where there are many tests, invariants. We have monitoring of different kinds on different platforms. We have audits with carefully chosen auditors, internal review process, and also formal verification, which is the the topic of this talk and I'll explain briefly what it is now.

So, what's formal verification? So, it's a domain that is in between mathematics and computer science. Just for that, I find it extremely cool. But also, you have a powerful idea underneath it, which is that you you try to match the code with the specification. And you want to do that in a formal and rigorous way, a mathematical way to ensure great guarantees about your code. Um and this can be done with giving and getting a formal specification. So, that's not typically typically what you get. So, if you look at some documentation, you get more informal specification, something like returns a valid value, which may not be that

useful because what's valid in that case or sometimes you don't even get So, for example, if you have a deposit function, maybe the documentation is okay, this is the function to deposit the funds, but it doesn't tell the whole story to because the whole story is like what happened to the funds, what's the yield, how can you withdraw them, what's the risk associated. So, a bunch of things that are not specified. And what you want for formal specification is the kind of the opposite of that. You want to specify everything and you want to do that in a rigorous way. So, an example of a formal specification simple that I wrote here is that for every input X, if you apply F to X, you get a value that is greater than 10. So, that's formal, that's great.

So, once you have that, what you can do is match the code with this formal specification. And out of that, you get what is called a verification condition. So, this is simply a formula that when you you verify it, you know that the code matches your specification. When that happens, we say that the code is correct. So, you you cannot really say that code is correct without a specification. You always have a specification in mind when you say the code is correct. All right, so it's a bit abstract, so I'll try to take an example. So, let's take back the formal specification that we had on the on the bottom left.

And we have this snippet of code that looks like some Solidity code. I removed some keywords to make it fit on the screen and and I'll do that for Solidity code. And we want to get a verification condition of that part of that. So um So, here just quickly, you have an array of size three that is holding integers. You have a function G that is unspecified. And if you want the F the function F to respect the specification, what you look at is that the return value G should be greater than than 10, right? But this should only be needed when X is greater than two.

This is so, this is the first line. And also in the other cases, you want V to be greater than 10. But since X is a non-signed integer, it can only happen for X = 0 or X = 1. And this is why you get this verification condition. So, it sounds pretty easy, right? But actually, for programs that get a little bit more complex, it can be tricky. And I I leave you with a little brain teaser. So, let's say in the condition now, instead of X, we have X++. Or maybe ++X. So, maybe we'd be a little less confident about what the verification condition would be.

And in the general case, it's actually can get quite quite complex. But hope what's what's good about that is that since both the codes and the formal verification are formal objects, you can actually apply algorithm to them. And you can do that automatically using a verification tool. And so, that's one part that is done for you. So, if we recap a little bit, assuming that you have your code, you have three steps to verify your program. So, first you need to come up with a formal specification. So, that's the first step.

Then you need to apply a formal verification tool. So, that's the step we've just seen right there. And then the third step is to actually verify the condition. And verifying the condition, even even if the second step is is done automatically for you, verifying the condition is not always easily done. Like like this, like automatically finding a proof is is hard. Um And uh So, I've seen verification conditions of 2,000 lines of code. It happens.

So, it's not easy to do by hand. Um all right, so it can get quite complex. So, why bother with formal verification? And I think if there are three reasons for that in the case of DeFi. First is that you have small programs. So, this is kind of embedded in the in the system. You have a limit on the contract size on Ethereum. And also related to that, you have this open source culture with having readable code. And also, it helps for maintaining the code, but it also helps to to reason about the code.

And this is typically what you do when you do some formal verification. So, that's the first point why why formal verification is a perfect fit for for DeFi. And the second point is that you have a critical system where potentially you're managing a lot of funds. And you really want to get it right the first time and that's why formal verification shines in this in this setting. And finally, maybe a bit less talked about, but in the blockchain setting, you have this idea that you don't want to be able to rewrite history.

But at the same time, it means that you the mistakes that you make, they they are potentially permanent. And so, same thing, you really want to get it right the first time because this mistake won't disappear. And so, formal verification gives you great guarantees there. All right, so this is the general overview of Morpho, of formal verification. And I'll give more concrete examples of how it is applied to the Morpho protocol using the free tools that we use at Morpho, namely Certora, Almos, and Wi-Fi. And I'll start with Certora.

So, Certora is a great tool for many use cases. And in the case of Morpho, we use it in particular for data structures, verifying data structures, verifying optimization. So, let's say you have one function and then you have an optimized version of that function. Then then you want to verify that that they they do the same thing. So, you also use it for verifying the Morpho token. And I won't get into the code, but just know that in the Morpho token, you want to have an authorization setting where you give users some roles and that's useful if you want to make the token transferable at the right time.

So, you have these two functions that is user have role, which is a view function, and then just you have this set user role function. All right, just so just know that and in Certora, what you do to be able to to specify is that your your contract is the right a rule. And a rule is just basically a formal specification where if I add I dissect that rule, I have this first this boolean does user have a role uh then I call any function F on uh on any argument, and then I store this boolean again.

And what I say at the end of the rule is that if the fact that the user has a role has changed, well, it means that the set user role function uh it's it's the set user role function that was called. So, in a sense, what this rule means is that uh only the set user role function is able to change uh if a user has a role. And so, this is not maybe not the first rule that you would have come up with, so I wanted to show it that formal specification is not easy sometimes. And this is actually a really useful rule. So, you can put that in your CI, and when later you add a new function, uh it will check for you with uh perfect certainty that you did not add a new function that was modifying the roles.

All right, so second tool I want to present to you is Why 3 that we use at Morpho Labs. Uh and this tool is uh a general-purpose verification tool, which means that it's not uh designed for Solidity uh directly, so you need to have to this translation, and it's a deductive verification tool where you it does not make any uh compromise in terms of soundness, and you can verify uh uh contracts with arbitrary uh number of iterations in the loops, for example. So, it works in a modular way, and this modular way mimics very well the contracts where when you call from the the outside, you cannot change the the storage variables.

Uh and so, we use that to uh translate our code into uh Why 3 code. All right, so this is kind of the architecture of the the program the verification, and I want to show an example of how um of a theorem that we managed to uh prove using Why 3. So, I won't focus too much on the syntax uh because it's another language, but basically this theorem is really not so easy to to come up with and also to to prove on paper. And when you want to formally verify it, you also get uh arithmetic and the rounding errors that you need to deal with.

Uh but basically, what this is is that Morpho is uh a contract that aggregates users. Uh and as such, it has a position on the pool on the underlying pool. And that means that um you need to make sure that it's it's not being liquidated. And this is what this theorem is about. So, if you take the supply on pool that um the Morpho contract has, you multiply it by the liquidation liquidation threshold, this gives you the borrowing power, and you show that it's greater than the actual bar.

All right. Um So, last example is about Halmos, and um yeah, you can see that you have run really cool property of Halmos is that it's uh really tightly integrated with uh Forge. And this looks really much like a Forge fuzzing test, and actually it is, so it works if you try to to run Forge on it. But when you run Halmos on it, you get additional guarantees. So, pretty nice. So, this particular example is taken from the data structure that is used in Morpho AAVE 3.

Um and this data structures works with buckets uh with uh ranges where the bounds of the range are powers of two, consecutive powers of two. And the bucket is identified by its lower bound. All right, so uh this data structure is improving fairness, is very efficient, and we want to also formally verify it. And this is what we do here, so we say, "Okay, so the bound is indeed a power of two, and any value uh that we get is in the bounds." And this is automatically automatically verified, which is very cool.

So, let me uh finish with the the contributions. Um so, I've shown formal verification that is done um on on Morpho protocol. So, for that, we use direct verification of Solidity code using tools like Certora and uh Halmos. And we also defined a methodology to translate Solidity code into Why 3 code and uh to verify it. And uh that's it. I think uh that's all there is about formal verification, uh but if you have more questions, I think we have a bit of time, right? Um yeah, thank you, Quentin, and we have 2 minutes for questions.

And I already see one. Yeah. Thanks for the great presentation. I am very interested that how long does it take to verify a protocol like Morpho? So, if you compare the in-house effort that you've done and say formal verification services by somebody else, so how does how does the comparison work? Why did you opt in for in-house verification, basically? That's my question. Yeah, that's a great question. So, that's kind of my my core knowledge, so I'm formal verifier at at heart, so I didn't opt in for that. But why Morpho did is because you need to have deep knowledge about the the the protocol to be able to really understand

and formally uh reason about it. So, it's not necessarily uh the case for every protocol, so sometimes it's a bit easier to verify. But Morpho optimizers have really deep and untangled uh protocols, so you need to have deep knowledge of that. And so, for your question about uh how much time it takes, it's also a tricky question because it depends on like how much you know the protocol and like what tools do you have, and also uh how deep you you are willing to go. And if you want to really verify everything and take everything in, so that can take years, basically, so it could be almost impossible, I think, to do.

But uh if you want to really verify the logic, which is what we did uh using Why 3, for example, you can do that, and you can do that uh rapidly. So, if you really focus on the the important stuff, the core core protocol logic. Uh hi I have some experience with formal verification, and the way when we get stuck that maybe you can help us how you verify complex interactions. For example, Morpho interacts with Aave. Aave is a huge protocol.

Morpho is a huge protocol. If you start to mock a lot of stuff and dependencies, it means that you formal verification relies more on your mocks than real code than not real code base. I think you can understand the problem. So, what's your findings here? How to make this complex formal verification for interconnected contracts and a huge code base? That's that's a great question. So, indeed, it's very complicated, and different tools provide different ways to of handling it. Handling it. So, in Certora, you can have a dispatcher, for example, you so you say, "Okay, when I have I'm dealing with tokens, I'm dealing with this sets of contracts."

And this is a way that you can like have your dependency. So, it's really neat way because you can like really specify what what you want. But in the general case, it can be yeah, indeed, quite complex. And so, one general idea that is um that I found really useful is to start small. So, you start with a small dependency version that uh so, a mock contract of Aave, and try to come up with a formal verification about that. And then so, you have this behavior that you're you're mimicking. And then once you have that, you you you can separate it because now you only work on Aave to show that Aave actually does um uh show this behavior. So, you kind of

separate the two, the dependency on a with a particular specification, and then you take the specification and try to verify that it works on Aave. Does it Does that make sense? Yeah. Okay, uh thank you, Quentin, and