Building Secure Contracts: How to Fuzz Like a Pro

Transcript

the next speaker please welcome Jocelyn from trail of pets who's going to be speaking about fuzzing building secure contracts how to fast like a pro welcome Jocelyn thank you thank you um okay hey everyone so this is going to be a workshop we are going to have a couple of exas we are going to go through if you already want to to take all the material you can take the career code or go through this website you will see you will see five exercise I'm not expecting us to go through all of them if we can go through maybe three of the exercise it's already good given

the time we have let's say if you want to you know yeah if you like challenge or if you already fast go for it we have two spare tickets for the security Summit so if you go through the five exercise and you don't have a ticket to the summit just let us know okay today we are going to talk about property-based testing but we have introduced in the previous talks and we are going to have an end zone in our approach on how to develop environment and how to use furthering to develop more secure contracts uh my name is Jason Feist with me um Natalie Chen and Justin Jacob from trail of Beach if you have any question about our company or about what we are doing

don't hesitate to let us know Natalie already introduced us this morning so I will keep this part so today we are going to focus on kind of trying to understand how to find bugs in a in a contract how to find vulnerabilities what are the different type of Technique we can use and we are going to focus on the specific technique which is property-based technique as of you guessed let's say you have this piece of code you have two function a function to buy token and a function that computes some parts and you want to find bugs in in this example don't try to look new too much there is a bug there but we will see it like later how can you find your normal Bridges

on a high level you really have four techniques that you can use the first one is unit test manual analysis fully automated tool and semi-automatic tool um unit test I'm hoping that you are all aware of you know what they are basically you create a concrete example and you are trying to you know test it with different platform other Foundry whatever you know works for you here um it's a good technique it works well because it's well understood by a developer but from a security standpoint it's not going to protect you against vulnerability we actually have data that highlights there is no correlation between having good unit test coverage or unit test you know development and

the likelihood of having critical vulnerabilities in the code base and so we run for that is that most of the time when you are going to develop any test you are going to use them to trigger a happy pass so things that should behave the way you know like you are intended to do while vulnerability usually usually relies on kind of edge case that's why you should still do unit tests but they're not going to be enough the second technique oh yeah just an example of unit test the second technique is manual version so this usually it requires specific set of skills specific mindset and specific expertise usually for manual review you're going to ask a security auditing team such as trailer base or you know any of our competitors to look at your code and you

know try to find the updates this uh some benefit you will be able to catch any type of vulnerability you will have like a large curve image but it does also some limitation the first one uh it's kind of done on a kind of on the stop shot of shortcut base uh it's time consuming it's worth of intensive next technique you can use you can use fully automated tool usually this type of techniques rely on static analysis or analysis like static analysis they are going to look for pattern for common vulnerability that are well known in the space and are going to try your ability to find vulnerability like that you might know Theta which is a static analyzer for solidity

if you don't know we are actually of a GitHub action which is called Street Direction where you can just add this to your CI every time you do peel request it's going to look for common vulnerability and it will help you know to trade as a result this is really powerful and it's open source and it's free the last kind of type of technique we call them semi-automated analysis because then you need a human interloop you need someone to help the tool to to know what you know they are looking for and one of the main known thickening Fallout but we kind of discussed in the previous talk is called property based technique base testing and we are going to see what it is and

how to do it with a Kindle like so as I mentioned um as a precursor in the previous talk um when we refer to fuzzing we're essentially stressing the program with random inputs which means at a high level it would be like a monkey on a keyboard or a cat on a keyboard and essentially throwing random inputs into your smart contracts and seeing how your system behaves it's fairly fuzzing in general is fairly well used in

traditional software security and you can see that through the use of like for example AFL and Gophers generally these um generally these platforms are testing for crashes so they're looking for are there opportunities in which malformed input can cause a program to crash and therefore cause unexpected Behavior that's not exactly what we're going to be testing with smart contracts because there are there is no concept of crashing um instead we're looking at property-based testing so this is when you take some of the assumptions that you've made on your code base and you apply it through property-based testing

by defining invariance the fuzzer is basically going to Generate random inputs call your smart contracts and check whether the output and the states are actually correct and whether there are deviations from what is expected in general fuzzing can also be considered as unit testing on steroids because you're not only limited by the input that you've specified but you have the the fuzzer comes with additional features to essentially generate different input so in terms of what is an invariant and what and how are we able to actually use fuzzing to integrate and invariant is

basically something that always has to be true it's something that regardless of what a user does with your code base and how your code base works this property is supposed to hold true within your code base for any state change so the easiest example would be for the erc20 token that a user's balance should never exceed total Supply if this property is violated then it means there's probably something as an error within like the mint function or maybe something with an arithmetic this property tells us that if there is a violation that there is an underlying bug in our code base

so this is where Echidna is used we use it fairly heavily in Audits and it's used very much in mature code bases it's basically used to generate those random inputs so that we can call Smart contracts and call those functions and see whether properties are intended to hold so from essentially the invariance that we create we're writing them into solidity into something that a kidney can understand and therefore run randomized inputs on to check whether there are potential invariant or property violations

so this is one example of smart contract code and this is just the typical this is just a standard token it's got total Supply it's got balances and it's got a transfer function so if we specify that the property invariant is essentially we are able to Define it as an Echidna function the Echidna test is going to Generate random inputs to see whether a property violation is possible um so in terms of what the property actually is um we were essentially we should be determining um what code to put within the Echidna invariant to determine whether total

Supply and the balances assumption assumptions actually hold if Echidna is able to break this then it means Echidna has essentially found a set of inputs that breaks those invariants pass it to Justin for exercises thank you okay um as I mentioned it's a end-on session so we are going to see a couple of exercises and we are going to you know help you to write invariant in solidity and to tell them in with the kidma before we go around for like the setup do you have any question regarding property-based testing regarding fuzzing

in general Okay so you can go on this website hi everyone customer question um do you know what's the difference between the property based testing and the mutation testing okay usually mutation testing um each refers to a technique where you are going to change the unit test so you have like you know a set of unit tests

and you are going to introduce changing in your test or in your function to see if the unit test pass or doesn't pass kind of like the idea of mutation testing usually is going to rely on trying to evaluate how good your unit tests are Hangouts different because here we are going to Define invariant and we're going to see using variant old or doesn't hold so mutation testing usually more used to test the quality of your unit test here it to test the environment of the system okay thanks we have a tool which is called Necessities that does mutation testing if you are curious okay

what time is it so let's take 15 minutes to go through this classical size so if you go here we can just follow the links okay until freedom and we are going to go you know oh yeah we're going to go over if you have any question with the setup or if anything is not working foreign

[Music] let's give it three additional minutes and we'll go through the answer okay so for the first exercise this was a Target and assuming you can see you know just by looking at the card that there is an abuse

bag here we are using uncheck Android operations so there is no other for protection otherwise what you can easily do like an underflow when you transfer the phones but how can you you know without even looking at the card how can you try to find this type of box and here um the property that we want to try to see if it's invariant that no one should have more than the total Supply if you deploy the contract and you say like the initial balance is 10 000 and there is no mean function the total Supply is 10 000.

and now uh the invariant property is exactly that the user should not have more than 10 000 as you can see here hunting which is really straightforward that you can Define the environment in solidity everything is in solidity it's just a function with like that we're doing a Boolean like a condition and this condition is our environment if you want again on that it's going to say yes I can I can break this invariance here is a sequence of transaction to trigger and to reach like this this condition and it's just a call to transfer with ten thousand and some number and yeah obviously it's because of the underflow here

is there any questions regarding the first exercise how many of you manage who have echina warning okay how many of you might have to finish the third exercise okay let's go to the second one here we are going to try to have a system where you can pose a system you drop the ownership and we're going to use the keynote to see if we can unpause the system so let's take yeah that's like 15 minutes again so 25.

then it will be also on YouTube so can you tell us a bit more about how Echidna Works uh underneath like does it just realize what the functions are and calls them in a random order with random inputs for example in this case with the pause and pause I guess you just write this invariant saying uh make sure the contract is not imposed and then it would just try out these pause and pause functions by itself so it's going to try out the function of the contract there are some heuristic for example we do construct constant extraction so we are going to use Theta to look at the code find some interesting variable and feed that to a keynote so that it's not

fully around them it's random with some realistic under the wood it does coverage so it's going to look at you know what are the different what are the different aware of the code that are reached by the transaction and it's going to use this information to determine which like mutation to apply so it's it's not fully random it's one done with some heuristics so for example for the previous situation with the transfer we only care about the balances and not the pause and pause mechanism there is a way to guide the kid not to say yes this is the only thing you should use try to break it with that yes there is a configuration file so you can say okay just call file function or just call this function like

if you have a really large you know code base and you want kind of an hour of the search you can do that with with a configuration file all right thank you any additional question thank you [Music]

[Music] okay just to get a quick overview of how many of you managed to finish like the second size oh way more on the first one congratulations okay so here we have a contract with multiple function we have a feature where the owner can pause and unpause the system and there is only under modifier and and so on so the question here is can we deploy the system in a way that the contract is paused you drop the ownership you put it to the other zero so there is no more

owner the system is paused can you unpause it and here again the properties and variants is going to be describing solidity it's simply this function so it's a function that we're doing a Boolean and the Boolean is a condition um is pause is equal to true yeah yeah so

um I thought we had to write a test that narrows it to you can't call resume essentially because in the test you're calling paused at the start and if you're saying it suppose is true is always true then it's not going to be true initially until paused is called and then ownership is right now so okay if I understand correctly I mean correct me if I'm wrong um you you mean that to check if regime can be called was well I just thought that was what the exercise was oh okay okay um because the test is not the contract that's like a user and the use you're

you're seeing the expected behaviors the user can deploy the contract call pause and then renounce ownership yeah um and you're testing that it can't be unpaused um but that test is saying is saying that it's always paused from the start but uh like so okay like here the scenario is that you deploy the contract you call pause so you pause the system yeah because I'm seeing this as like separate from like this test contract I'm seeing it separate from the token okay so there's a linear returns here so Tesla can inherits from token

so your inherit all the functionality more for like Foundry tests you you have like a setup and I was thinking the Constructor is like set up but you're actually saying like that's the Constructor of the token yes typically would have a setup function where you do like the initialization uh we do support uh this is kind of a let's create an API I have a couple of slides later on so you can also use setup function and do it that way that makes sense yeah yeah that makes sense okay um okay where I was yes so here the environment is just this solidity

function is always close if you run it on it it will call two different functions and it will break the invariants here just to remember we did not look at like the different function we don't maybe we don't even know there is like a resume function we just say I want to have this invariant and what's going to happen is that Akinator is going to deploy this contract is going to call all the different functions available in the contract transfer pause and pause whatever is going to try all of them and in between every curl is going to call the Echidna functions of the environment it's going to see if it's holding and here what it does is that it does two curl one call to honor one call to

resume and after that when it covers the invariance the invent is working why the environment is broken so this is kind of like a hold style of vulnerability where people were like in old version of solidity you are defining the Constructor with the name of the contract and here there's a typo the contract is called ownership and the function is called owner also owner is a function available for everyone anyone can become the owner and then everyone can unpause the system this type of vulnerability don't happen anymore but it's just to give you like a kind of a should not happen anymore but just to give you like an Insight of the type of invariant that require multiple

transaction to be broken do you have any question regarding the second exercise um so regarding the functions you call is it like brute force or do you have any strategy on doing this so as I mentioned previously it's random but with some realistic and one of the realistic is are using the coverage so it's going to look at you know like you make a new transaction with a different function are you covering new code yes now and

based on that there's kind of a feedback group to know you know where where to kind of prioritize but part of it is still London I think there is like a can you please go back to the previous slide I mean it's a related question to the previous one so in this case owner doesn't take a parameter but let's say let's say that you know owner would take an address yeah and the owner is said to the address in that case would I could not still be able to pass message or send it to the owner and still be able to find the bug yes um typically as I mentioned like you know it's going to try one family value for the parameter but in addition to that there are some heuristic and one of the

realistic for address for like the type address else is going to use all the address that are known description so you are now any contracts that you deploy or things like that and what about interactions where uh you know a specific function needs to be called a few times and another function and a little complex interaction so uh I mean does akina try those also or yes it's like here um here there is two transactions but you can go over like further five six seven um something that can happen also is that you call 20 transaction you break the invariant as a strategy where it's going to try to reduce the the call so that it's a bit

easier to debug so you might break it the first time by calling 20 function but that link is going to try to say okay maybe I just need to call 10 of them and I'll leave this process okay thank you okay now the question um that is sometimes difficult in order to have a good insight and and and to go to go behind is how to define green variants like the example we just saw the environment was pretty straightforward and you know they were simple but when you are like in front of a code base the environment might be more complex so how how can you kind of Define and how can you understand them and

I think the best process is driven iterative approach start really small the first invention that you are going to describe for your contract should not break like the first invariant should be something really straightforward that should not work it should be something just to kind of uh get used to the cut base and get used to like the the system you should first they find the invariant in English don't try directly to write them in solidity you know open a markdown open a text editor whatever works for you and start to you know think about them in plain English like what the system is supposed to do then vitamins validity and iterate your nakina does it work is does it not work if it works either you

found a bug or maybe your invariant is wrong maybe like you know you made assumption about the code base and there are sometimes that you add was not correct so as far you need this iterative approach and that's why trying small is usually better because you will move complexity as I mentioned you know start early on even even before it's kind of like a powering shift even before starting to curd like if you're a developer before even starting to record your your contract you can you can think about what the system is supposed to do and this will help you you know like down the line um so it's really like a process of thinking about what the system is supposed to do just to give you some example if you have now with Matrix Library if you have

like you know a fixed Point arithmetic or something like that then you can think about 1 000 arithmetic properties that you should have commutative identity inverse and so on so you have like a couple of math related environment should offer most of the properties then you are something that can be more complex with a supply which you know we already saw then you can start thinking about some function for example transfer what the transfer is supposed to do uh the transfer is supposed to decrease your amount right and it's supposed to increase the amount of the receiver if you go and you define an invariant that does that you will realize that this is

actually false because one of the HKS is that if you do a self-transfer if you do reception sir you don't decrease your balance your balance is going to stay constant now this is just an example of invent that might seem straightforward but actually there are a lot of educated and things to consider when you are building on this type of things something to consider also a situation where the system should reveal so our bottom false so it's also important to you know create environment on things that should not happen in that way so if you have a transfer and you don't have enough funds as well you should revert our own faults depending of your implementation they are kind of two categories of

invalent you are going to have function leveling variant so those are going to be invariant related to the execution of a specific function most of the time not all but most of the time they can be stateless invariants or you don't manipulate the state and those are usually the simplest to test because you can just look at the specific function and you can just focus on that then you have system level invariance so in variants that must be true for any function within the contract the balance Supply the balance of the user not not being greater than the total Supply is one of these examples so it's not just with respect to specific function but it's it's respect to the system as a word

now how to do that in practice for function level in variance a simple and simple technique is just you anyway the target you name it the function you create a function that you want to test and you can use for example assertion to to check so you can say here you test the commutative INB and you test it is equal to BNA system leveling variant might have more complexity in the sense that you might need a complex initialization maybe you're going to try something that requires five different contracts and then we need to deploy the five different contracts for that as well you can do everything in solidity or you can also leverage your unit test to do that we have an additional tool which is

called etheno it's just going to reply you in the test and help the fell off a lot okay if we go back to the example at the beginning of the presentation if you remember we have this contract we have two function a buy function which is going to check if you have enough money and means some token and a valid buy function that is stateless and just going to try to see if you provide enough token and enough ether to byte here you have to function by which is stateful valid by which is stateless here again start with the simplest one valid by start with the stateless what environment can we have here

one simple one we like simple is that if you send zero uh ether you should not be able to have any token out of it so you can Define this as a session so you call the you call the function you say I'm sending more than one you call valid by this should never be twitch like this should always fail because you are trying to buy something with zero if you want this with a kid now it's going to tell you actually you can do it with one and the reason for that is if you look a bit more closely to the formula here you have a division and then multiplication

if the number of token is below 10 the division is going through it on zero because it is going to run down so the amount of ETA that you have to send is going to be to you so for any token from one to nine you can basically buy that for free does that make sense any question I have hinted a bit the session mode so in echina we have what we call Api so we have three way to define invariant we have the Boolean properties that we saw with the first exercise we are the

assertion that we quickly saw sorry we quickly saw with like the previous slide and we also supported up front real API the adapt Foundry is mostly the same as a Boolean property but you have this setup function and so on yeah Boolean properties where we deserve them assertion you just add additional answer to the code base and up Foundry that you you are aware of so for the next exercise we are going to go on exercise four we are not going to do the exercise 3 today and here we are going to use our session mode so we're going to try a property where instead of

using 18 something something function we are going to use a session and let's take 10 minutes ish for this one any question this one would you mind going to yeah the example test thank you this one okay the slide also in the GitHub if you actually need them

do you have any questions regarding this one okay just okay I have a question yeah so you mentioned system level assertions and let's assume in the case with the balances you write the test and just make a transfer and make sure the balance is either increase or decrease is there a way to do this subsequently like many more times do these transfers away outside of just running a for Loop and just doing a bunch of like does that make sense I want

basically to do a lot of transfers but the state is maintained after each of them so it's what was already happening here um like you are going to Define an invariant where like you know like the after of the execution like the stage should be which like this environment should be true Aquino is going to try multiple call if you remember on the previous example on angular size 2 akina was calling two function it was calling owner and then resume I think so here I cannot could also called if you have a transfer function you cannot might call transfer one time two times three times ten times it's just going to randomly try different combination okay perfect so let's say in a case like

a landing protocol and so on it would just just try a like a random number of iterations of random number of things and it would just see if at some point reaches an inconsistency that's correct um there's a notion if you look at the configuration of a sequence length basically it's a number of curl before the state is related to the beginning like for example if you say the sequence length is 1000 it's just going to try one thousand call and at some point you just reset the system to like the initial state okay thank you and is there a way to kind of uh Target its inputs to something for example like it's in uh

Forge I think you basically can limit the inputs in some ranges so the best way to do that is to do input filtering and solidity we have some tutorial in Secure contract about that and we have some helper in a repo which is called properties basically you use module so you know like if you want to kind of uh narrow the input from an integer to like 100 to 1000 you can use module operation you take like the uint use modular operation so that otherwise you it just can create between the scrunch and so that the further doesn't waste time you can also use require you can just say you know like require this input to

be that number which require which will waste uh like results from the further because transactions okay yeah thank you Okay so here's a goal was to use a session and we were trying to you know break the transfer function so here we inhibit from the token we call CPL transfer to call like the function we want to test and we Define on variant using assertion

so here's our session is that uh you know it does it has increased um and yeah if you end up with a kid now it's going to break even variants uh because of the back I'm going to go a bit quickly because we are running out of time uh one thing you can also notice when you use a session is that you can keep that session in your code if you want uh additional you know unchain Safeguard this will allow you to have like invariant and post condition within your contract it's going to co to you know cause more gas and it can be complex enough bugs so keeping your contract only a session that you have a strong confidence in it and four things that are not too complex

quickly there is a notion of multiple contract and composibility or the example we are mostly on one contract but you may be like your system is using five or six different contracts for that you can use a specific flag which is all contract if you do that instead of focusing on Closing one contract ekina is actually going to call all the function of all the different contract if you are looking for composer ability bug that's very useful a couple of additional exercise I'm not going to go through uh but you know feel free to go through and after this day um there are many additional tool and technique that you can do to check invariants uh there are other like Bernie dark Foundry they might be easier

to use but in practice it might not be as powerful we have been using a kid now for more than five years in a different audit and we spend a lot of time making it efficient um the other technique based on formal methods such as formal verification the technique are useful they are powerful but they have a lot of drawback they are complex to use they are time consuming there is this quote from the runtime verification CEO basically saying that you need almost 10 times oh nine time uh the resource to do formal verification on your code base versus what you need for development so it's really intensive in comparison to heading that you can as you as you saw use pretty quickly a lot of advantage that I did not cover

we have some functionality where for example you can try to look for transactions attacking we're going to consume more gas if you are looking for you know complex Loop or things like that you can do differential fuzzing where you try to apply on two different uh implementation of the same logic you can do unchain phasing so you can provide an address and an FPC node and the keynote is going to try to First based on a state which is existing unchain and so on and so on it's free and open source obviously Just for information we are actually writing we are rewriting Akin and go it's called Medusa it's not as much as the keynote it's kind of on an MVP phase but if you are curious and you like to experiment with new tool feel free to go

through it yeah I hope that you enjoyed this session to learn more about our environments and property based technique you can go to secure contract we have the properties repo where we have defined existing invariants for different protocol but you can already reuse and just Import in your contract you know you should start thinking about invariant starting English and then try in solidity out of curiosity who here is going to try again on his next project perfect and if you have any questions feel free to let me know foreign