From High-Level DeFi Properties to Concrete Security Bugs

Transcript

So, uh hi everyone. Is it loud enough? Am I doing okay? Yeah? Good. So, um yeah, my name is Nurit Tedor. I'm VP Product at Certora. My background is, of course, computer science and many years in the field of security, and I joined blockchain and Certora 3 years ago. So, uh yeah. I'm going to talk about high-level DeFi properties and how can they come find a concrete bug? So, we will see many bugs. We will go a little bit fast, but all the slides are available.

So, properties are conditions that has to hold. We have discussed a lot in variants properties, and it's for a specific system. Um there are different ways to actually formalize. I will show two. Uh we know that all systems, we don't like to say it, but we all know that all systems have bugs. Um so, defining these properties can help finding bugs. And it can also be automatically checked, but just about thinking about them, and there are different way to actually check them. So, it's not necessarily only formal verification.

Okay, so how do I think about properties, and this is what I advise now all our customers to do. I try to split them into a few categories. So, just for the example, I'll show this on something that is not DeFi, so it will all be easy for us to follow and understand. So, a unit test is a very basic test. It's what we all know from basic programming. It's just checking the functionality of one thing. So, if we have an elevator, it will check that the door can open.

Another thing that I call valid state, what would be a valid state? Things that has to always hold. So, the door should always be closed while in motion. Variable transitions are things that actually change. So, there is a state before and a change after. So, the floor number has to change when when we are expecting it, right? State transition, this means that I'm looking at the system or some element inside the system, a user, or something like that. And I'm I want to define what is the state. It's like looking at the system as an automata.

So, it's not busy when it's stopped and no further calls. High-level properties would be something that is not dependent on the implementation. It's something that should happen and something that should hold regardless on how it is implemented. So, every lift, doesn't matter if it has this button or that button, but eventually every call should be attended. And the risk assessment, it's a different way of thinking. And in this case, we think about what are the worst thing that can happen, right? So, like thinking backwards, like, "Okay, this should never happen." So, and what

we see here is that the door is closed while in motion, that would also be a risk analysis. And it's okay that it was also our valid state because it can be that there is more than one category per property. And what also can be is that a same bug, the same bug can actually be detected by more than one property. So, it's not like distinct, nothing is distinct here. And now I want to talk a little bit about coverage. So, we all define coverage different ways.

There is the traditional code coverage, which we already know that it's not very good, right? Because usually bugs are not as on a specific line on every execution of that line. Um it depends on the value. And also path coverage, that is a little bit better, but still it doesn't give a lot of confidence. I like to think about coverage, and I like to think about what are all the possible bugs that can happen. The problem is that it's not computational, right? I mean, it's not something that we can compute. But we can think about it. So, when we think about our testing, we actually think

about this property, this unit test, it actually checks for specific types of bugs, and that is what it covers. Okay? And then I can have my other properties that also um give me some kind of coverage. But as I said, we cannot actually compute this. But what we can do is do the bug injection study, like what we heard yesterday, a very good talk from you trying from uh Trust Token. So, bug injection is the way I would measure coverage.

Okay. Now I'm going to talk about how I specify property. So, from the logic point of view, it's um there is a few notations. The most common one and the most uh uh used one is called whole logic. What it actually says it's that if there is a condition that need that holds, and we execute some kind of statement, then Q must hold afterwards. But and this is a good way to think about our properties. Okay? Um it's not easy to define it this way.

So, we define it with in something that looks like a program, and this is um Okay, so this is the whole logic. So, it says there was a condition before. I don't have a mouse here. There was a condition before, and then there is the operation that we do. In this case, it's transfer, and then there is the expression that must hold after. A different way to express properties, but they are the same, is something that looks a little bit like a program. And this is our language at Certora Certora verification language. But there are other ways.

Also, Fuzz has different ways to to write properties. But the general idea is the same. There is some kind of precondition, and then there are some kind of operation, and there is a postcondition. Okay, so the precondition here again is the assignment to the balance before, and there is an operation, and there is a condition that must hold. Okay. So, this was all like introduction, and now we can drill down into properties and the nice bugs that they find.

So, the first example is OpenSea. OpenSea, probably we all know, we heard about it. It's a very big project that has been launched a few months ago. It's live. The code base is very very complex, super optimized, lots of inline assembly. Um And the way one thing to handle here is to do a lot of unit test properties because there are so many functions. So, here, for example, when I'm thinking about unit test properties, I'm not trying even to look at the exact implementation. I'm trying to look at the interface and think about properties and reason about the arguments. I don't

want to copy the code. So, if I see something, I try to understand even just from the signature of the function. There is a revert on invalid, a boolean, right? So, it means that if it's false, this function should not revert. So, I will write a property that will say that on each value, on every value that is possible to give, if the revert on invalid is false, then this function should not revert. That is a very high level property, and I want to check it on all possible values, like what Sam told us today to do our unit tests on all values. So, this is a good way to have thinking

about the all possible values. Another thing that I do in my unit test, I want to compare different runs of the same uh program, of the same function. So, for example, here, I want to uh compare um reverting and non-reverting, the same flag, true and false. So, if it if it reverts on on the true, that means that when I'm calling the same function with the same arguments, with the false flag, it should return false, right? I mean, otherwise, there was some kind of inconsistency.

Okay. And this uh nice property found a bug. But, the problem is with unit test is that if it's a unit test of a very internal function, that means that it might not be uh a reachable state. Okay? So, it found a specific bug on a specific set of arguments that are passed to this function, but actually, the function never passes this set of arguments. But, it's still very good to do this kind of unit test and understand the exact functionality and find those bugs.

Um valid state properties. So, on the elevator it was like the door is closed while in motion. And those are expression of the system variables. Um and I do this by identifying groups of related variables. And it can be also variables that are not necessarily internally to this contract. It can be also things that are externally dependent. So here's an example from a compound compound V3 that Jared told us about it. Um so it's also uh the code has been simplified compared to compound V2, but still has a lot of uh optimization and nice features.

Um so a valid state property here. There was um there is There are two main structures. There is one structure for every user that has a bit representation of which asset is a collateral. Okay, so there's a it's contract its comment has 15 collaterals as a 15 tokens as collateral. So there is um a uint16 that just turns on these bits. And then there is also a mapping that stores how much collateral a specific user has for a specific asset.

Okay, so it's like two um variables that actually represent something that is dependent, right? Because if the bit is turned on, that means that this user has put collateral in this asset. So there is a very simple invariant here that should hold, right? If the balance according to the balance if it's greater than zero, then the relevant field of that asset has to be turned on. And this is an if and only if, right? It's be um it it's both direction it should hold.

So this found a very uh um nice bug, very common bug. We see this a lot on uh wrong bitwise operation. Okay, the general issue was that there was a wrong casting here, and what it actually meant is that um half of the collateral were not counted. So, someone can be collateral, has collateral, but also be liquidated. So, um this is a uh one bug bug that was found by this con- property.

What is going on here? Uh but uh this property also found another bug. And the other bug is a failure to set to false the bits on liquidation. Um so, the first bug was high severity, the second one was Okay, so the bits are turned on, but no no balance, it's not the end of the world. But the nice thing is what we see here is that the coverage that this property gave us. We actually checked all functions in the contract, and we actually looked deeply into all the updates to both the balance variable and to this bit vector representation.

Okay. Um this is me. Okay, so variable transition is properties that we reason about things that can change. So, we want to know when can something change, and we want to know who can change, and what change is valid, and when must it change, and if it change, what else should have changed? All those different questions that we can ask when we reason about a specific change to the contract. Okay. So, um this example is from Silo Finance. Uh this is a lending protocol.

Um also trying to reduce the risk. Um this core was built and all the properties were designed by the Silo team. Um yeah, very nice work. And this is a very simple property. What it says is that so there's total deposit and the total supply. Okay, it's like a liquidity pool that we can envision. But basically the idea here is that if the total supply change, that means that also the deposit change. And this is a very simple property, very easy to think about it. It actually even very we we

can think about it as doing this even stronger by having more relations. So the issues that was found here is that also some kind of wrong computation. And what meant is that there was a it was a high severity issue and all the interest that the protocol obtained was lost. And again, very nice property. It covers all the functions. Okay. High-level properties. This is when we want to reason about auxiliary information. Actually, information that is not even in the code, but we can think about. So for example, that the sum of all the balances is the total

supply. We want to reason about external dependencies. So for example, in a liquidity pool, the amount of asset in the right in the underlying token that should be hold. And this found also another this very simple property found a very critical bug. Um and the high-level properties are not dependent on the implementation. Risk analysis, as I said, those are like thinking what is the worst like putting on our black hat hat and thinking how would I attack this?

Okay? So, in SushiSwap, this is a Dutch auction. The price is going down and basically when the auction is closed, anyone that signed up as a buyer, multiple buyer, can claim. And a very simple rule will say that, right, no one can claim twice or if someone can claim after he claimed, the amount of claimable token has to go down. Well, apparently not in this case and there was an issue, also very common issue, we see this a lot, mistakenly use of message sender as opposed to some other address that

should be taken into account. And usually in these cases, what we see is that there was a unique test, but it usually checked on the message sender as the argument because it's easier, right? And that's the nice thing when we think about properties, we're going to write it very general. Okay, so back to coverage. So, the Dutch auction, this is a postmortem on real bugs. We had a nice set of properties and these properties covered a nice set uncovered a nice set of vulnerabilities, but it also missed one, okay? We were lucky enough, we and SushiSwap that this was a white hack and

Sam has found it and this also gave us the idea that we need to do much more understanding what is the coverage. So, we started more coverage testing and what we are actually doing is a bug injection study. And the main idea for me and the main takeaways I want to see what type of properties give us the good coverage. So as we see here, one just one high-level property. There was five, but one found two issues. And I said of state transition found a few other rules. We see that the coverage here there is not much overlapping.

Um okay, so here there are four unit tests that did find the same bug. But usually uh we see that there is not much and this is another this is so this is from Silo another coverage study that we have done. Uh they as I said this team did a amazing job on defining properties and we did a a bug injection of six. The nice thing here is that um many properties uncovered about the bugs, but there was not one bug that was caught by all right by all the properties and there

was not one property that caught all the bugs. There was a lot of overlapping and it is what we see here is that nothing is redundant. All many of the properties uh here it's like 20 properties that uncovered at least one and this is very impressive. Okay, my takeaway is that specification can help find the critical bugs. And only thinking about those properties and manually checking the code, that's a good step. I mean sometimes those corner cases are hard to see by by by the eyes, but sometimes just thinking about those properties uh we find bugs just by trying to understand

what are the properties that should hold. Um as we all know that defining the specification is challenging and our testing is good as our specification. But I think what we have seen today is a methodology for designing those spec and trying to take the time and step-by-step and not like okay, what are my ideas? There's a way to actually do it very much the technology. And actually how do then specifying is understanding what is the coverage of our specification.

So we can have good rules about our properties but not necessarily understand what is the coverage. And the best thing to do is a bug injection. And again, this could even be manually, okay? You think about your properties, have someone else just say I'm going to insert this bug. Is do you think one of your properties is going to uncover it? And tools can aid in verifying checking properties. There are fathers, formal verification, and hopefully maybe one day we will even check the properties during execution before the execution of the transaction and and help improve security also at this phase.

Yeah, that's it. Thank you.