Best of both fuzzing and formal verification: introducing Bounded Model Checking

Transcript

My name is Zuri and I work at Stora. It's a web3 security company that had built a few public goods uh in the in the space. And today I'm going to talk to you about a $5 million bug that no one caught in time, why it will be challenging to catch it with fuzzing, and while it will be pretty difficult to catch it with forification, too. And then I will present a different idea called bounded model checking. We'll talk about what it is and how it works. And by the end, we will know uh another tool that we can use in our arsenal.

On March 6, around four months ago, $5 million were stolen from 1 in, which if you don't know is a decentralized exchange. The vulnerability was live on mainet uh for two years and it was missed by nine different audit rounds. The vulnerability lied in the function settle order. Um this function received a structured call data input and moved it over to resolvers. It handles swaps in in one inch.

Um part of the expected buffer had a section called the interaction and that interaction had a declared length. The attacker exploited this function um by first of all creating a normal swap except he traded pennies for millions. And the way he did it was by giving it a bad length, a negative length of minus 512.

That caused the memory pointer to underflow. And unfortunately, we were inside an assembly block. So no underflow guards were present. And the attacker could put whichever uh data he wants inside the interaction section. So that means that he bypassed all access controls and could do whichever fund transfers he wants. So uh why did it miss so many audit rounds including some of the most well-known auditors in the space right? Um the first reason was that uh the function was deprecated and thought to be unreachable.

So uh it seems very likely that the auditors didn't spend that much energy on it as they did in other parts of the code. It was also a level low-level code. It was ule so it's harder for us humans to read it reason about it and also it required a very specific input especially the number minus 512. So it's clear that sometimes human arders can't catch all the bugs and that's why we strive to use as many automated tools and not automated tools as we can to increase the security of smart contracts.

And one of the first tools that uh we can use is fuzzing. So fuzzing, if you don't know, is the process where the computer generates a lot of dimped inputs, hammers them all into the test. It's some sort of a brute force approach, and we try to see if one of those randomly generated inputs will cause a failure. Let's delve a bit deeper. So here I'm going to show you some uh code examples from Lido. Lido use uh foundry. So the code here is in solidity more or less.

Every first test starts with a setup function that kind of initiates uh the world for us. So um it will call the constructors, it will set up a few different accounts. Uh it will give some access controls and the idea is that we want to start from um a state that is interesting that something could be stolen, something could go wrong, right? If there are no accounts in the system, then that's not very interesting and doesn't really represent how it will work like in the real world. And after that, a test will usually look like that. We have some assertions which are conditions and we have some function calls in between. And the important thing is that the parameters of these

tests um will be uh randomly generated by the computer. So here we have uh two different inputs, right? We have the number here, the data, and we have the bytes, the position. So the computer will try to generate many, many, many different inputs. I'm talking about hundreds of thousands, millions. Um, the more the marrier. Fast testing, however, is a bit limited in what it can do. Um if we want to find um an exploit, we need to um get the right condition with the right functions before it, which is sometimes something that's very hard to do. For example, in one in's case, we thought that the

function was unreachable. So maybe no one would even uh write a test like this. And that's why uh we have other tools that are doing some in something called invariant testing. An invariant of a smart contract or software in general is something that should always hold true. And if it doesn't, it means that we're in trouble. For example, for a decentralized exchange, one of the environments we can say is that an account should not lose funds due to another account's actions. What does that mean? If I have an account in one, then I may lose funds. I may lose some

money due to market conditions. The token went down, but I shouldn't lose money if Bob decided to swap, right? That's not related to me. And there are actually tools that can try and see if the contract behaves according to this invariant. And today we're going to talk about three of them. We're going to talk about invariant fuzz testing, formal verification, and bounded model checking. Invariant fuzz testing is um the next level of fuzzing in many ways. Again, we start from the same set of function like the one we saw before except now instead of calling one specific function, we are calling a random external function in the contract. And like previously with

fuzzing, the inputs are also randomly generated and is also sent by a random address. And after calling this function with the random inputs from the random address, we check if the invariant still holds. And if it does, we just do it again. We call another random external function and check it again. And so on. We usually do it for 15 20 times. Uh that's the the usual amount. And if it all passed, we start all over. We go back to the sub function. We call again random functions with random inputs and check and run and check. And we continue to do that for many many call sequences. Again, we want to run

hundreds of thousands. So this is already a step up from fuzzing because we now call all the functions, right? We don't call a specific function before we check our test. But still the input coverage of fuzzing is relatively low. For example, in the bug that I've explained before for one inch to get to the exploit the call data has to have the correct layout otherwise uh the function will revert and we will not see the exploit. So not only does it need to have the right structure, it also needs to ha to have the correct length of minus 512.

And the chance to stumble upon all that if we just randomly generate numbers is slim. There is another issue with uh invariant fast testing and that is uh program state coverage. A program state is the content of all the storage that includes right about the funds, the accounts, the access controls, everything that we can say about the world that's the state and obviously um a lot of exploits require some specific states.

There are practically uh infinite states for a program. There are a lot of different options of a program state. And in fuzzing uh invariant fuz testing we cover some of them right we always start from the same initial state the one that the setup function defined for us and then whenever we call a function unless it's a view function we reach a different state and then whenever we do another step we reach another state. So the number of states that we explore grows linearly with time which is uh nice compared to regular fuzzing but it's a drop in the ocean compared to the number of infinite states out there.

So that's why we sometimes want to go to a different tool for example uh formal verification. Formal verification tries a different approach. We're not trying to randomly generate inputs. We're trying to prove things about the system mathematically. How does it work? In general, we get two different inputs. One is the code that we try to secure and one is something we call a specification. It's basically the test that has the invariant that you're trying to test. We put them both together to the software which compiles them to a mathematical logical formula and tries to prove it. If we get a

proof, then the proof always holds. It's like a theorem in mathematics. We don't actually have to try all the different values of x to say something with a theorem about a number x. And we do the same here. That's why we can do that. We cheat. We use math. However, if we can't prove, many times we find a bug. So when we see that the theorem doesn't hold, the tool will tell us it doesn't hold when I call this function with these inputs starting from this state.

So that's great and let's look into a little more details how we check in variance with forification. We start from an arbitrary state which is not the same as the initial state we had before and it's not randomly generated. What it means is that we give the prover um we give the prover the freedom to choose um the inputs that will cause a violation. And that means that it will think like an adversary and try to give inputs that will cause a failure of the invariant.

And then we're going to call the external functions all the external functions in the contract except now instead of trying to randomly generate the inputs we're going to use symbols like x in a math equation. So it can take any value and again we use math at the end. So that's totally fine. It's not going to run again from a random address and then we go on and we started from an arbitrary state and at the end here it's not an arbitrary state but it's a class of states that uh are symbolic states. Uh all the states that I can reach from one step by calling the deposit function.

I do that for all the external functions in the contract. And if I get a proof for all of them, then I've actually covered all the starting states, all the inputs, it's perfect. Except now we have the opposite problem. We've actually covered too many starting states. So what we care about is not actually all the mathematically theoretical possible states of a contract. We care only about those that we can actually reach uh by running the program and calling its functions. So a fuzzing cannot cover all the reachable states but for modification covers some states that are actually not at all reachable and that means that they're not interesting.

For example, if uh we will try to prove um the invariant I said before that an account should not lose money due to another account's actions. Um one of the counter example I can get is that there are just too many tokens. I am transfer I'm swapping tokens and then it overflows which doesn't make sense but the prover doesn't know that the amount of tokens has to be smaller than say the total supply so it will give me that example it had the freedom to choose it and I need to tell the tool don't do that so I constraint it let's say I did that I run the tool again now I have a counter example due to wrong internal accounting and that means that the variables inside the contract of the

exchange um do not correctly represent its assets. So I can assume that it does right and continue going on. But is it safe to do so? If I assume that the internal accounting is always right, I'm going to miss bugs, right? Potentially. So now I actually need to try and prove that like proving a lema before a theorem. And now I'm a bit in a rabbit hole and trying to to prove more and more things before I'm proving the thing I care about. And that's where bounded model checking comes in. Bounded model checking is an idea that we start from a specific initial state like we did before in fuzzing.

And now we call again all the external functions of the contract with symbolic inputs. Now I reach two different states. Again, not a single state. It's a symbolic state. It represents all the states that I can get to by one step of calling that function. and I do it again. So that means that whenever for each uh state that I go to by one function call now I call another function call and I do that again and again until I reach a certain depth of uh function call sequences.

So I'll briefly go into some technical details how would um a call sequence look like. At first I'll zero out the entire state. Then I call all the constructors. If they have inputs, they will be symbolic. Call the setup function like I do invariant fuz testing. I call four external functions of the contract with uh arbitrary inputs. Could be anything. And then I test the invariant. And I will have a sequence for every combination of four external functions in the contract.

Another analogy to understand it is that fuzzing goes deep. It's like uh DFS. I'm going straight ahead going 15 functions deep then starting all over again. That's not how bound model checking works. Boundary model checking first checks all the states that I can reach with one step then all the states that I can reach with two steps and so on and so forth. Baron knowledge checking has been used in the industry for many years but not yet in web 3 to our knowledge. It has been used in many different fields. It has been used to verify C programs um by Amazon. It's still being used. Um NASA developed a tool to u uh do bound

balling for Java programs and it's used all over the place for hardware by Intel, Nvidia and so on. So it's not a new idea but it's a new application and unfortunately it also has its own drawbacks. So the amount of different uh call sequences grows exponentially uh as we increase the depth because every time we have a choice of all the different external functions of the contract. So it's exponential growth. That means it doesn't really scale all that well. And that means that in future research we will try to focus on choosing paths that are more likely to lead to an exploit.

And that also means that we will try to ignore paths that we have maybe already covered or we think there is a very low chance of them leading to an exploit. Finally, let's compare all the three different technologies. First of all, we have input coverage. So for uh fuzzing, we saw it's pretty low. Um however, we use symbols. So formalification and bound model checking have perfect coverage. The state coverage of uh fuzzing is low as we as we saw before. It's perfect for for modification because we started from an arbitrary state and bounded model checking is somewhere in the middle. So we again we deal with symbolic states right we call these functions with symbolic inputs.

However um some states we will not find from the initial state maybe at all maybe not in the end steps that we've checked. So we don't cover everything anymore but we cover a whole lot more. So it's something in the middle. However, one of the advantages of bounded model checking is that now all the um all the alarms it gives um make sense. So we no longer run into the problem of unreachable states whenever we see a violation of the invariant. We know uh where exactly we've started, which functions did we took, which state did we pass through, and it's all diagnosable.

So uh I hope that today uh you've learned that we can use tools to increase the security of smart contracts. Um we can use fuzzing but it cannot take everything uh found everything. We can use qualification but it's hard and it's effort intensive and we can use bound model checking as a middle way between the two. If you're interested you can see our code in the GitHub here uh by scanning it. It's open source. Thank you. [Applause] Thanks guys. And that's all the time we have for today. Thanks.

Ask some questions here if you like.