Building a Mental Model of a Smart Contract | Uri Kirstein - Certora

[Music] hello everyone my name is URI and today we will discuss a mental model that will help you find bugs in smart contracts the outline of today's talk uh we will Define the mental model then we will focus on different types of properties that one can think about and we'll see some examples where we have found we have prevented bugs on real code of Sor clients using these different types of properties a defi system can be very complex the code has many branches and edge cases and it depends on external libraries and you have to take into account its interaction with other protocols in the ecosystem and Game Theory and economic theory and so on and that makes them very complex and hard for us to think about and reason about if we want to find logical errors a solution to that are mental models which help us as humans understand a simpler more abstract problem and the mental model that I will present to you today is to break down the smart contract and instead of looking into it as lines of code or machine instructions than a collection of defining properties a defining property is something that describes how the the system should behave what is something that should be always true about it and if it's not that that means that something seriously bad has happened a bug and why specifically this model of properties and not a different mental model uh that is because we have the ability to feed these properties into a computer software and let the software check the code for us and ensure that these properties are correct and describe its Behavior so there are two different types of technologies that allow us to check properties of smart contracts the first are invariant fuzz testers fuz testers invoke random external functions in your code and try them with many different inputs as long as we give it time and they do so intelligently and they try to cover as many branches in the code there are a few different fers in the market there is Forge by Foundry Akida by trail of bits and Medusa by critic and many more in contrast to that there is a different technology called formal ification which takes the property and takes her code transforms it into a logical formula and then tries to prove things on it using mathematical methods and also there are a few formal verification tools out there there is hm by dap tools there is the prover by Cur and there is hos by a16z in our talk today we will not focus about these Technologies or how to use them and that is because even if you are an expert and know how to use them perfectly their effectiveness in finding bugs will still be limited by the quality of the properties that you gave them and we know from practical experience in Cur with our clients that thinking about good properties is is a difficult task so how does one start this intimidating task of identifying interesting properties for the mental model so we don't start from the code we start from the documentation and that is because we want to understand what was the intended Behavior rather than the implemented Behavior we want to be able to tell hey this is wrong this is actually a bug later on we do read the code we look at the variables and so on but we try very hard not to repeat the same logic when we write properties here on the screen you see a list of properties written by Badger da and you see that these properties are written in plain language in English hopefully it's easy for us to look at them and think whether they make sense or not and right next to each description we see that there is a category which will be the focus on the rest of this talk so in Cur we cataloged six different types of properties and today we're going to talk about the first four listed here function test consistent state state transition and risk assessment due to lack of time this is not a scientific categorization this is just a helpful tool for us to understand if we written enough varied types of properties so that we can have a higher confidence about the security of our code and that means that the property can have more than one type let's start the first type of properties that we will discuss today are function test properties these properties like their name look at a specific function and ask questions about it what is its expected output how does it change the state how does it behave in relation to different parameters different values and also what are its revert conditions let's look at uh at an example to understand this better this example was taken from openc the nft market Place uh in the version of the code that was not yet deployed it contained a function called verify order status and to understand the bug that I'm going to show you you don't actually need to know what this function is doing it's enough to look at its signature and actually not even at the whole signature just the last parameter the Boolean revert on invalid from its name we can infer that if revert un invalid is false the function should not revert throughout uh the rest of this talk you will sometimes see Snippets of code in CVL CVL is the input language for sora's formal verification prover I'm not going to explain the code Snippets because this is not our Focus today it's only here to give you an impression on how something like that would look like so this property prevented a bug in the code the function verify order status actually could revert despite that revert oninvalid was false and that could happen if a different parameter called only allow unused was true so what did we learn first of all a word about coverage in terms of the amount of input the coverage will depend on the technology that you use to verify this property if you use the fuzer you will have tens of thousands hundreds of thousands of different inputs uh depending on how long you let it run if you use formal verification you can uh get up to a full coverage of all the possible different inputs and back to this specific type of property it checks only a single function so it has lower coverage but it's also easier to debug because we know exactly in which function the problems lie moving on to the next type of property that we'll cover today they are consistent State Properties a consistent state is when we have different variables in our contract that describe related things and they all agree with each other they're consistent if they don't agree then we don't know which one of them is true the system is corrupted and from now on we don't really know how it will behave all hell broke loose let's look at an example here as well this one is from compound the learning protocol the code before deployment included two different types of variables one is a bit Vector 16 bits long called Assets in and each bit in the vector corresponded to a specific asset type and if it was on it means that for that user this asset type was given as collateral and if zero it was not in addition to that we had a mapping in the code that took the address of the user and the address of the token asset type and gave us back the number of tokens that were used as collateral so as we understand these two variables should agree right if the bid is on in the bit Vector we expect to see a positive number of tokens in the mapping as well and vice versa so this is the consistency property so why did the code even have this bit Vector um this is because bewise operations are more efficient so it saves gas and this is actually where the problem lied before deployment uh due to an incorrect bitwise operation we only looked at the lower eight bits which means that only eight type of collateral assets were accounted for and the other a types were disregarded obviously this is a a major bug in the code and compound fixed it and they check the property again and we prevented a different problem this time when a user was liquidated meaning all its collateral was taken away all the collateral was zeroed out in the mapping but the bit Vector was not zeroed out so now again the bit vector and the mapping do not agree anymore and the state is no longer consistent so this is a good example how one property can cover many different functions in the code and find several bugs the next type of property we'll discuss are State transitions and in state transitions we look at the system or a specific part of it as a state machine this is a model that some of you may know if you've learned computer science but we have an example here on the screen so these black circles represent States so we have owner not owner and pending owner States and the arrows represent transitions between states with the boxes no the different names of functions one needs to invoke so right after the Constructor the system is in the owner State and it will stay in the owner state for as long as you don't go over the arrow meaning for as long as you don't call the function set new owner and if we did the state will now be not owner so this diagram represent the transfer of the owner address so this is a subset of the system the state transition properties look that our code actually behaves uh like the diagram so we will check that if we're in the owner State we can either stay in the owner state or if we call the specific function in the arrow set new owner we'll move to the corresponding State not owner let's look at an example where' prevented a bug using this type of property this one is from A's governance version three which handles uh proposal voting and execution in the code a proposal was implemented as a state machine we even have an enum that tells us what is the state of the proposal The Proposal can be created cued executed and so on a very basic property for the proposal is that eventually it reaches the end end of its life cycle once the proposal is cancelled it's cancelled forever that's it there is no next step to go to so this means that this is the final State and there are a few of these here executed failed cancelled and expired if we look at it more formally we say that if the state is greater than three then it cannot change anymore so we look look at the test version of uh A's governance V3 and we've found a problem in the code it was actually possible to go from an expired state to the queued State because the executor could increase the delay and the grace period and this was not intended they should never had this power and we were able to uncover it by looking at the state machine and uh trying the property that described it moving on to the last type of property that we will discuss today these are risk assessment properties for these properties uh we should take on a pessimistic look and think what will be the absolute worst that can happen to the stakeholders how can they lose money lose privileges what are some known attack vectors or exploits and then we say not in our code let's look at an example this one is from a Dodge auction contract from Sushi swap a Dodge auction is an auction between two types of tokens where the price actually drops with time so a buyer can chip in they can wait longer because the price will drop but then they run the risk of someone else buying before them after the auction is completed all the buyers can go and claim uh all the tokens they bid on what would be a devastating thing that can happen in a Dodge auction contract one of them will be the ability to double claim right to pay for one token and after the auction is complete actually take more than what you've paid for this obviously comes at the expense of the other buyers that didn't claim their tokens yet uh technical detail since the claim can happen during multiple transactions we say that the amount of claimable tokens that um the user has must decrease after every claim in the Dodge auction version of the code before deployment this was not the case if we look at the function tokens claimable we see that the amount of claimable tokens was reduced but for the wrong address it reduced it for message sender and not for the user and that means that the user could do a double triple quarle claim this is obviously uh really critical vulnerability but let's remember that's how we constructed the property so risk assessment properties we look at some bad things that can happen know at at vectors and say uh we don't want them to ever happen Okay a recap of this talk I hope that I was able to convince you that going through the effort of thinking about the properties and the behavior of your system as a mental mod model is a useful exercise that can help you find bugs it can help you understand your system better it helps you when you look manually at your code looking for your next vulnerability as an auditor and you can even do better if you actually use an appropriate computer software to test out these properties and ensure that your smart contract always behaves correctly however writing these specifications is not an easy task especially not if we're trying to reach a high coverage of possible bugs and that's why we've developed some methodologies that can help us do that and gather all the interesting behaviors and one of the key weapons in our Arsenal is to try and make sure that we have enough properties of enough varied types that will increase the confidence we have in the security of our defi system thank you