Designing Solidity Contracts That Don’t Fight Verification

Transcript

Does it work now? Yes, that sounds better. Okay, so hi everybody again. My name is Pamina Georgiev. I'm the formal verification team lead at Satorra. Satorra is Web3 security company or security company in general and apart from auditing, we and many other things actually, we also do formal verification. And um today I will be talking about how to write Solidity contract um that are good for formal verification.

And I will argue that if it's good for formal, it's also just plainly good written code. Okay. So, what is formal verification to start with? Um at Satorra we believe that formal verification is another security pillar that every DeFi protocol that has a lot of money like manages a lot of money should undertake because apart from testing where you run it on specific inputs or maybe even fuzzing, um you cover more paths.

Of course you do auditing, but with formal you actually try to find invariants and properties of your protocol that hold at all times or under all inputs >> [snorts] >> and that are always true. So, this is the only way that gives you mathematical certainty that certain things about your protocol are true. And at Satorra we have the Satorra prover which is an automated reasoning tool that allows us to perform inductive formal verification.

Um and to that end we can write uh these properties these specifications as rules in our Satorra verification language. Um and these are properties that all your contracts or your protocol needs to satisfy. And the prover then compiles your code and those specifications into mathematical formulas mathematical um like logical formulas and uses an a so-called SMT solver an automated reasoning tool um that check the checks for satisfiability with some potential theories um and checks whether those properties are satisfied or not in your protocol.

And that means we get a result that is either verified meaning um we always find a proof for your property and that it's that it's correct under all possible inputs or all possible computation paths or we get a counterexample which can mean that we just found a very concrete bug in your code. To give you a a short example of what this looks like first. Let's take a lending protocol borrow function. Think of isolated market lending, okay?

Often what we see this is a let me just tell you this is a toy example, okay? So this is not production code obviously. Um but we've seen this in the past in some production code as well. Or at least the problems along the lines. So what you see here is a borrow function where in order to get the collateral there is a callback. So we transfer the to the borrower first the tokens that they want to borrow and in the callback we expect um that the message sender will give us the collateral to cover the position and in the end we check that the message sender's position is healthy, right? So is healthy with regards to LTV in lending and DeFi this

means over collateralization of your debt. Now we have a property that we prove for basically every lending protocol out there which we think is very very essential which is why we also refer to it as the holy grail property. Namely that is an invariant showing that when you are when you start in any state that is where you are healthy no matter which function you execute in your contract, you cannot reach a state that is unhealthy.

And we in CVL we can do not only an invariant but we can also do a strong invariant. And a strong invariant means that we don't only check it like we don't assume it before a function and only check it after but we check it every time when there is an external call to some other contract, okay? So in this case it would be checked right before the callback and obviously we here in a state that is unhealthy. Okay, so this is what we find with the prover. We find a bug.

Now in such kinds of lending protocols um often you allow some reentrancy, right? So in this case there was in this toy example um it's possible that you rather than providing collateral in the callback just call liquidate. So all of your your debt is basically socialized. You end up with a zero debt and of course once you return um your your basically healthy again and just got a lot of free money, right?

And this is actually the same mechanism as was the case in the Euler V1 bug a couple of years ago. Now for the sake of the argument this is not probably not the right fix for many protocols that work like this but let's just say we put in non-reentrant modifier we're done, okay? You cannot reenter and let's just move on and we want to prove something else, okay? Now we want to prove that debt unless you repay debt always increases okay?

So let's say you want to check that a crew interest like the debt cannot decrease by itself it can only decrease when you repay. Now we could write a function like a rule as you can see here that is parametric that checks for any function in your contract F. So F would be instantiated when we run the prover with any public function of your contract. Um that whatever debt we have before after it's it's at least as much as before. Now the problem is when you look at a crew interest or like similar functionalities there is usually like some compounding math which means a lot of maldives um which makes things very very hard for an SMT solver. So rather than a verified

or a counterexample, we get actually a timeout. And the reason why we get timeouts is not a bug in our tool. It's a fundamental limitation of this kind of mathematical logic, okay? So when you have SMT solving with non-linear arithmetic um there are many many theorems Matiyasevich etc. that that show that there's no one algorithm that can um that can always show whether your property is satisfiable or not.

Um and uh of course this is a limitation of formal verification in general and automated reasoning in particular. Um but there are a lot of heuristic solutions that we do and that we apply that can make us still like let us verify your code even though there is a lot of non-linear math. And the main mechanism behind this that we use at Satorra are function summaries. So summaries basically allow us to tell the prover what is happening without it telling it how it's happening, okay? So we take some complex computation completely abstracted and just tell it okay the return value should be

something like that or it should be greater than this input value something like this, okay? And in the case of showing that total debt does not decrease I don't care how a crew interest accrues debt. The only thing I care about is that the value after is not small not smaller than the value that I started with right? Um so what we can do is use a summary to write that. And there are many many ways to write a summary. For example, we have this thing called ghosts which are basically variables or mappings that we write in CVL and then you have like non-deterministic values for your different inputs.

Um but the point is if your code is written in a nice way, it allows for summarization. And if this is not the case, then we face something leading then we face either timeouts or we need to refactor your code, which we refer to as munging at Certora. Um, yeah. So, if we look now at our timeout, uh, the code is actually written quite nicely, namely there is a function calc debt that does the actual compounding computation of the interest. And rather than looking at the calc debt itself, we just tell the prover, rather than using calc debt, um, just use this um, this debt ghost mapping, which basically tells it over

the three inputs that you give to the function calc debt, return some non-deterministic value. And with this axiom, we just say, uh, this value this value should be greater or equal to the original debt, so the D. Um, and then basically what we cover not only the actual computation your code would do, we cover more. So, this is a called an over approximation. And with such a thing and we can very simply uh, show um, that this axiom, for example, is true uh, based on how calc that is written.

Um, we we actually prove even more uh, than we would assume uh before. Okay. So, this is one one of the things that allows us to write summarization, okay? So, I give you now three patterns um, that uh, that I see or we in Certora see very often that make us that um, drives us into munging your code. So, the first one is the one we already saw before, namely um, computation mixed with storage updates.

Please use libraries, use pure function, use pure functions uh, in order to extract the computation that you do um, from the actual storage update. So, the more modular uh, your code is, the easier it is for us to summarize complex math. And I also argue the easier it is for auditors to understand your code, the easier it is for anybody to understand and maintain your code. Um, uh, so if you do that, um, it allows you, as we said before, um, to use a ghost or to use some sort of function summary um, rather than using the actual code.

Now, another thing uh, that we also often see is circular dependencies and spaghetti code to some extent. So, let's say you have a contract vault that calls uh, the strategy and the strategy immediately calls back the vault. Uh, this is super entangled and we want to verify each contract as individually as possible at least. Um, so this rewriting this a little bit differently and um, as you can see here in the preferred version, uh, allows us to do this kind of modular verification.

And then a third thing that that we often see are overloaded param parameter semantics. Uh, if you do it, at least use enums, please. Um, it makes it a little bit more explicit, it's easier for us. We want to reason about different things when we do when we when I see a withdraw or a deposit, not they're not necessarily always have the same properties that I want to prove, right? I want to prove them individually or different things for different parts of your code. Um, so these are uh, this is another one.

Um, I encourage you, please go to this blog article. Um, I only mention these three because I think it makes for a very boring talk to just tell you what to do um, instead of what you shouldn't do. Um, but we have a list on our blog. If you're interested in formal verification, please make sure uh, to look into that. Um, [snorts] also if you do and have any questions, I'm happy to take those. And um, of course um, basically there are some principles that make good and nice nicely written code, right? That is not only good for formal verification, uh, but is generally good code in my opinion, like modular architecture.

Separate your concerns, use libraries, isolate complex math, um, things like this okay? And without further ado, I'm happy to take questions. Thank you. Uh, sorry, not really a question, but the QR code scanning didn't work. If you can show it again. >> Sorry.

Um, it's the if you go to Certora certora.com/blog, it's the first blog at the moment. Um sorry. Um, just want to ask about offense for the top five. Um, just want to ask about like how's the performance like when you convert uh, using the prover converted to the SMT language, when you encounter those kind of like uh, dynamic storage load or like the byte type operation, those kind of like weird type rather than the rather than the numerical type like you in I'm pretty sure that the those kind of U M type like the solver working quite well. And those kind of like weird weird like dynamic tuple, dynamic array, how's the performance and yeah, how do you go around with it?

Usually it involves a little bit of munging. So, it depends a little bit if there anything that's dynamically sized, um, we usually need to do something about it. Um, we try to or actually I think we're pretty good at making it quite safe. Like even if we do um, what is called under approximation, like not checking the whole state space, but under approximating in a good way so that technically by induction, you could lift what you just proved um, to even dynamically sized um, arrays. But yes, um, you are correct that this is also I think it it should be somewhere in the list. Yeah.

Any other questions? Can I ask that? Yeah, sure. [laughter] Yeah, cuz I I'm the next session. So, how are you doing? Cool. >> [laughter] >> Um, um so actually like I want to ask about like slightly out of context is like uh, it's just the AI era that everyone talk about the AI. So, so I'm trying to uh, wrap my head around like how's the LM to actually help the whole uh, formal verification process. Like the natural things that kicking in my mind is like you were talking about like writing the property testing, the invariant, which is like a natural things to think about and I think this is like something that definitely execute executable feasible.

Um, but like what I'm really concerned about like when we uh, when when I back in time test around the the the solver we send another solver, it's like the C3 solver actually take really long time to solve. And by any chance that like we can uh, use like what was your take of like using those kind of AI actually potentially either help the solver like in the underlying side that like the C3 solver or the conversion of the SMT SMT language? Yeah, there is I don't I don't think there is a limit on where you can apply it actually. You can apply it at any stage. Uh, it might be helpful at any stage.

We're working also in our R&D department, we have a lot of people exploring that for sure, right? Um, uh, and and yes, um, I stay tuned. >> [laughter] >> Thank you. Thank you. Thank you. I think that's good. Thank you.