Building secure contracts: Fuzzing like a pro

Transcript

foreign [Music] before we start I would recommend everyone to take a screenshot of this one so there's a link with all the material work we are going to go through today is a workshop so we are going to have a couple of exercise and ends on experience okay so today we are going to talk about how you can leverage a technique which is called Farthing to build a more secure smart contract we are going to see what is fuzzing we are going to have exercise on how to you know use a feather and we are going to you know see a couple of best practices on how to do that

so my name is rasna Feist with me is Natalie chin we are both working at tradovits if you don't know us we are a security company where we specialize in high hand security technology we have expertise in blockchain but we also work on different you know spectrum of security including cryptography or traditional absec one thing that kind of defer us I think from other companies is that we are research oriented and as always we spend a lot of our time trying to apply program analysis in our day-to-day you know activities and as always we have built a lot of Open Source tools you might know Slither which is a static analyzer for a smart contract a kid now that we're going to see today but we have a lot of you know additional tool for different altern and

so on so today we are going to as I mentioned we're going to focus on a specific technique which is called Feathering we are going to see what it is how you can leverage it and you know we are going to exercise for you to play a bit with it um the question like the first question that we're going to ask ourselves is how to find sorry how to find backs if I give you this piece of code these two function a function that is going to buy some token and a function that is going to compute uh some price to know if you are sending in a filter don't need to focus too much on this there is a bug but we will see that later if I give you this piece of code how can you know if it's good or if there is a

vulnerability in it you have basically four techniques the first one unit test I'm assuming everyone here you know knows what's a unit test you should do them uh you know we're valuable but in terms of security they might not provide as much value as you can think um one of uh of kind of evaluations that we have made internally that we were looking at uh how good our unit tests in the audits that we are doing and what's the likelihood to have a bug and actually there is no correlation and the reason for that is that most of the time when you are going to avoid you need test you are going to cover kind of the happy past things that should happen within the protocol while usually vulnerability are going to realize in

the edge case so you should do unit tests but they are not sufficient to prevent you know from vulnerability the second technique is manual analysis basically opens a contract go line by line trying to find vulnerabilities this requires specific set of skills you require a specific mindset and usually people go through a security firm to get an audit of bad context um as you know there are two additional techniques that you can use for your automated analysis and semi-automated Analysis by fully automated analysis I mean tool that you can just run on your card base they give you some Wizard and you have nothing else to do outside of creating the wizard one example of that is Twitter although it's a static analyzer it's

going to look for common command pattern and common vulnerability in your card base here an example of Street Direction so it's a GitHub action that you can connect to your GitHub and it's going to one Splitter on every pull request it's free it's open source and Setters demonstrated its capability to find vulnerability you know over time so I would highly recommend if you're not using it to you know integrate this in your RCI pipeline the second technique are like the fourth one the last it's semi-automated analysis what I mean by that is that you're talking to user tool but what is it

okay um sorry so the last technique is semi-automatic analysis you're going to use a tool but here you need to provide some input you need to provide some configuration or there's some manual intervention in comparison to slitter where you can just run in on your code base for some YouTube analysis you need to provide information in particular we're going to use on the specific technique which is called property based phasing with a Kindle foreign so that brings up the question of what is property-based testing and what are we actually looking for when we're defining invariance or what we're looking for when we write property tests at a very high level fuzzing is very

much like unit tests on steroids it's like a cat on a keyboard or a monkey on a keyboard and like pseudo-randomly generating random inputs for your functions and seeing how your functions work and whether your functions actually work in the correct way so fuzzing is fairly well used in traditional software you can see that in like AFL you can see that in lib fuzz and what they're looking for is slightly different than like what a smart contract would look for so typically for something like AFL it's not going to be looking for it's going to look for program crashes so it's going to say oh your code panics in this area and this is unexpected behavior

and it's basically going to to tell you when your program crashes there's no concept of crashing per se and smart contracts so this concept doesn't really work in terms of like the evm and like ethereum space what we mean by property-based testing is from a user perspective they're going to Define invariance they're basically going to say these are assumptions that should hold true in a code base and the fuzzer is going to randomly generate inputs call a function and see whether there are violations of a certain property so generally we're looking for violations of a property and not necessarily crashes so this is what we'd mean by unit testing on steroids with

unit testing you're limited by the input range that you're specifying so you're basically if you set up like a unit test your the inputs that you're checking are limited by what you've defined whereas in fuzzing it's going to randomly generate those inputs to see whether violations are possible so that brings up the question of what is an invariant an invariant is basically something that should always hold true in a code Base by that we mean something that's probably affecting System state maybe as a end-to-end system Behavior as opposed to the behavior of like a certain function for example

foreign so one really good example and one that's easy to reason about is the concept of total Supply in erc20 tokens with these tokens there's a concept of like user balances and then total Supply and a system and variant that we can reason about is essentially that any user balance regardless of whether it's the owner or another address should never exceed total Supply if it does then we know something is wrong within the system we know that there's either like a bug or something wrong within the mint or some arithmetic so this is where Echidna comes into play

Echidna is our open source smart contract fuzzer and what that means is that we're basically going to feed Echidna in variants and Echidna is tasked with finding what inputs are possible to essentially break a specified invariant that were identifying the benefit is that it's very easy to use and we can generally or we can Define invariance within solidity so there's no context switching between different languages we have the ability to essentially write it in the same language that our source code is in um it's also available within a GitHub action similar to what we saw with slither and it works for all compilation

Frameworks so you're not necessarily dependent on a single framework so this diagram depicts a little bit more of how how to think about smart contract code and invariance so in the middle we have the smart contract code and this is basically just the stub of an erc20 token it identifies the total Supply it identifies balances and the fact that from a transfer function that there is the opportunity for these balances to change the property invariant we're going to get into in the first exercise but with Echidna we're essentially going

to identif or determine whether achidna can find a property violation of the property invariant pass it off sorry okay before we go into the exercise you have any question okay so as I mentioned this is a Amazon you know workshop and we have a couple of exercise you're going to find the first one at this URL um checkout on the etrcc branch and um Good Luck so we are going to take 10 minutes to do

this one nothing and myself were going through you know work I want if you have any questions regarding the setup or if you have any question regarding you know Hot Wheels I cannot just raise your hand and we will help yeah 10 minutes or up to 50. 50 okay

foreign foreign

or even echidna foreign

foreign foreign

okay wherever you want if you have any issue and you need like help on the installation um if anyone needs help with like

installing Echidna um feel free to raise your hand too thank you

okay let's see the solution so for this exercise we have this target we have this contract it's a token it has a transfer function uh most likely you can support the bug here there is a unchecked block and there is a subtraction so you can have an underflow okay the pointer is not working but at this line you can have an underflow so if you try to transfer more token than your actual balance uh this is going to renderflow and you're going to have like a really really big balance but when you look at this type of contract you don't actually need to look for a bug when you are trying to think about invariant you can just try to you

know determine what type of invariant you want to offer this function and Define it so here the environment that we would like to try is the one we just described during the slide such as you have a total Supply no user should have more balance of the total Supply if you have a total supply of 1 million and the user has 2 million uh something one is going on so to test this with a kidnap you are just going to renew it the token with another contract you deploy the system with an initial balance of 10 000 token any other invariant health invariant is simply a solidity function Boolean and the Boolean is a condition it's it's a invariant that we are

looking for and here the invariant is simply that the color the balance of the color is below or equal to ten thousand again this is an invariant like no one within the system should have more than 10 000 and you can describe it as a solidity function if you want this with a kidnap again ekina is going to tell you this value this invariant does not hold and to break this invariant it's going to give you an example of sequence of transaction it's only one transaction so it's one call to some address to transfer to transfer this amount so what is happening under the hood is that Akinator is going to take this contract is going to call all the functions of the contract um here you only have the transfer function but you can imagine

you can have like you know 10 or 20 different function with different input it's just going to stress test the contract after every code it's also going to check the environment by calling it and if this invariant return false you'll find the bags and here it is called transfer and it did transfer with 1093 again you are going to trigger the underflow the thing which is interesting here is that you define an invariance about like the kind of the behavior of the contract but you don't need to even look at the transfer function itself to Define this type of invariant any question how many of you manage to find a

solution for the first exercise oh nice okay let's go over the second one um let's take 10 minutes ish to go through this one foreign

thank you foreign

foreign foreign

and then foreign

foreign leadership

foreign foreign

foreign okay how many persons managed to serve

this one oh nice we're making progress okay so for this one we have this target so we have this contract it has some you know ownership features with some access control and it's a possible system so you have a pause function and a wisdom function and here what we want to test is that we want to test a situation where because it's a portable system you say okay I'm going to pull the system I'm going to drop ownership so that there is no owner anymore can an attacker and pause the system so can you uh can you kind of prevent as an attacker can you resume the execution of the contract to do that within the within our test we are going to use a

Constructor to pull the system and Set uh honor to zero so we lose ownership there is no more there is no no user that can call the only or no function or at least should not be able to and now we're going to add a property and here the property is simply again a Boolean function that would lose a Boolean and the Boolean is is equal to true so the process system you pause the system you drop on your ship can you unpause the system can you can you kind of work this invariant and echina is going to say yes and to trigger that Akinator is going to tell you that they can break the invariant by

calling two function owner and resume now if we take a closer look at the ownership contract you will realize that there is a function called honor in ownership contract and basically anyone can become the owner like this is a bug this type of vulnerable is a bit old it was more common while the Constructor and solidity was not called Constructor but it did happen more than once the thing which is again interesting here is that we were not looking at the ownership contract we were not looking at the different function we were just looking at the possibility of the system and it can now kind of on its own managed to find a path to break like our or mitigation

any question regarding this exercise Okay so one thing that can be kind of difficult is to find invariants to you know like here in these two examples it was kind of straightforward small piece of code if you have like a couple of invariants that are easy to kind of Define but now if you you know if you take like a protocol which is larger if you are building something which is more complex it might be difficult to come up with invariant and having good invariant is actually the most important part of what we are doing here because if your invariant is just one is always equal to one sure you have an invariant but it's not going to be valuable uh you know for the safety of your contract

and the best approach is actually really Simple Start small try to create an invariant that you know is not complex and is really straightforward the first time you're watching an invariant should not break like the first invent you are going to come up with with your system should not lead to a bug otherwise either your code base is in a really bad shape or you know you are thinking too too far don't try to avoid the environment in solidity right away just thinking like think about them think in English like uh create a magnum file uh text file whatever works for you and start by dumping idea what you know what should be the kind of behavior of your system what it should be doing what it should not be doing and then once you

have like a couple of maybe five or ten idea go on salinity write them and run the further if an invariant breaks as are you from the back or your environment was first and this is something that is actually pretty common when you start you know building a variant you might have assumption on how the system is supposed to work but actually it's a bit more complex so it's a niterative process start small start with English then solidity when the further iterates based on the on the result um and it's really like you know a process of you know thinking about everything that can happen in your system and or should not happen to give you some example to be a bit more concrete let's say you have a now with magic Library so if you think about

arithmetic though of invariants are usually odd for any type of arithmetics commutative identity invert this is like standard arithmetic operation if you have you know more complex system we saw like a couple of examples with erc20 uh the balance of a user should not be above the total Supply you can also start thinking about individual function if you have a transfer function what should be the behavior of a transfer here you can think about two things the first one the balance of the center through decrease and the balance of the receiver trading quiz that makes sense right actually if you write rows invariant

they are going to break and the reason for that is that there is an edge case here either destination is a sender the balance is just going to stay the same so this is an example where you can think about invariant that are straightforward but actually the kind of expected behavior of the function is slightly more tricky that's why this iterative approach is really important something to consider also case in the example of transfer if you're not having enough funds if you don't have enough money the transverse with our tone fault depending on how you implement the token they are basically two type of invariants you're going to find functional leveling variants or system

level invariant functioning variant as a name kind of suggest are going to be relying on the behavior of an individual function the arithmetic one that we describe commutative and this type of things are usually function level they can be stateless not always but usually they are stateless then you have the system level invariant the invariants that are going to be true across any you know function in any call the total balance is one of example of this system level invariance it's usually better to start with function level in variant just to get like a better sense of you know where you are at and what you are trying to Define functional level environment might take a bit more time to to get them wise simple techniques it's just to inherit

the contract create a functions that call you know what you are trying to call and use assertion we are going to see in a couple of slides a different mode of echinap the first one that you use was to create a properties function but we also support assertion within the code the second one for system maneuver environment might be more complex and one of the difficulty can be to initialize the system if you are looking for invariants that are going through all over three or four contracts then you need to deploy three of our contract and you know initialization can be complex we have an additional tool is called ethino that is going to replay your unit test so typically if you have a really complex you know initialization setup you can use this tool just to see

the canal so that it's a bit easier to set up any question okay as I've kind of entered we have different API foreign so the API are going to be the way you define the invariant property brilliant property assertion and um dub Foundry so the Boolean property are the one you already manipulated pretty straightforward you have a function within a Boolean the environment is a Boolean this is nice because it's easy to use it's also easy for like system level environment it might be a bit easier and you don't have side effects

you are not messing up with a card so you know you can keep something a bit more clear and cleaner the assertions or using assets as a couple of Advantage because you can add you know assert in different place of the code but it has also a couple of kind of risk for example if you start adding assert everywhere in your code maybe your assertion as a bug maybe like you know like you add complexity so you have to be careful where you are going to to put the assertion and the last one is uh the dub or no Foundry kind of API it's kind of similar to the Boolean properties but there is like this setup function and like the property itself it doesn't work on like a Boolean but it's mostly it's fairly

similar to the Boolean properties okay for the next exercise we are going to see an example with a session so here you are going to instead of using the Boolean property you need to use an assertion to test the code any question okay let's take let's take 10 minutes for this one like I think at one point solidity was shipping with with like formal verification thing that was

checking assertions how is that coming along because I mean so yeah yeah so the question so the question is about Cersei and the smt Checker which is within Celsius and they're working on it so the smt Checker is going to work using formal verification it's slightly different in serving in the Sun that is going to use like a mathematical representation of the card to check the invariance for more experience the main difference and spoiler I have a couple of style on this but the main difference is that you are going to be way more efficient with furthering that with formal

verification from the moment you're going to try for my verification you might need to change the code base to make it amandable for for your your formal method you might need to create mocks so like it might not be able to analyze external curl and it's just usually more complex to use while if you check invent with a further from our experience you are just going to be away faster if you spend let's say two weeks writing on invariant you are going to go way you know deeper and broader using a further and using like a formal method-based tool for the smt Checker itself in Celsius I think it's still a work in progress I'm not aware of any kind of flashcard base using it and for the reason I just mentioned excuse me just to add some information

uh at runtime verification we are generating uh the K Foundry integration so that it will write Foundry tests you don't need to know thermal proofs you just write solidity and you generate proofs so that might be but yeah from kind of experience this is going to work for simple invariant if you have like an event within the function but from the moment you try to like you know test more complex invariants you need to add additional you know helper for for the formal method so this like you know adding a like a support for like Foundry or Aquino and everything is going to get you okay for simple environment but for anything more complex uh it's not it's

probably not going to work as easily from our experience foreign

means I was looking four years ago I was thinking of verification is a specifically like to find it so useful like the workers

I mean you know Things Are but if analysis there is really about

technique is foreign

okay how many of you managed to serve this one okay so here we are modest in the same situation where you know we have a we have a token and we want to check the transfer function however here we are going to use a session so instead of having like this property as a Boolean we are going to just have a assertion and here the assertions are made at the end of the transfer and you just check that the balance of uh you know like the color liquid and the other one increase um something which is interesting here but you have to be careful with is that if you use assertion you can keep the assertion in the code if you find a way

to express you know uh like like the invariant you might be able to just keep it as a nonsensive girl I'm thinking you have to be careful because first it's going to be more costly on gas but which can be okay if that you know additional Safeguard but writing invariant can be complex and you might introduce a bug so you want to be very careful to not have an invariant that is just going to break your system if you are the assertion but it might still be like it's a kind of a trade-off that you have to consider okay um there are a couple of additional things to consider for example composability if you look at you know modern systems not just one contract you might have five of six different

contracts you might interact with you know third party so we have a specific mode in Echidna which is called all contracts it's just a flag to activate a config file to set to true if you've said that instead of having a specific contract a kennel is going to call all the contracts so if you are looking for composability bug this is really important we have a couple of additional exercise we are not going to go through them but it's on GitHub so I would recommend you to you know try them and in particular they are from the damn venerable defy CTF and it's how to solve this challenge with the kingdom I'm just going to skip them okay some of the questions that you know

like we receive and you might you know ask yourself is a comparison between a k9 other tool the first things to know that nowadays there are a lot of further you have one in dub tool you have one in Bernie and one in in Foundry and you know probably other it might be slightly easier to use on the when you first use it for example uh the one in front of is really straightforward to use if you are already using Foundry for testing however Econo is usually more powerful we have additional features we have you know we have been using echina in our audit for more than five years so it's a bit more robust and we believe that the performance are also higher there was a question about formal verification from our experience while formal

verification might be appealing it's not as efficient as fuzzing in practice we like the most important part of all this work is not actually using a specific tool it's really for you to think about the environment really to sit down and you know consider them if you do that you have done 80 of the work how you are going to test them for my metal phasing whatever is only the 20 you know it's a women in work so you can try formal method but for more experience it's just going to be way more you know investment for you there is this um quote from this here or front-end verification is basically saying that you need nine times the resource to formally verify a contract versus the one you use for for

development while with a further as you saw it's pretty straightforward to use as I mentioned we have a couple of Advantage things that we did not go through during this Workshop but for example echina can Target high consumption as gas consumption function so if you are looking you know for gas performance you can just run a kinem this model is going to tell you which function consumes the most and this is going to be done with Felding so it's kind of more powerful than testing we have differential phasing where you have two implementation and you try to see if there is a Divergence between both and yeah we have a lot of additional things for example we have this optimization mode where for example you found a wounding issue and you want to know how

far the one thing can go you can ask Akin now to try to maximize the amount of of precision loss for the rounding so this type of things are only available in Echidna as far as we know and it's free on open source so information we are we're writing echinner so echina is in ascal it has been like a long discussion with the community because no one managed to contribute to Haskell so we are rewriting anything go with Medusa it's already open source it's experimental it's not as much as as a cleaner but yeah I wanted you to to know about it okay so as conclusion I would really recommend you know you as developer or security researcher to start building this kind of uh process of writing

invariant thinking about invariant and you know going through this iterative approach we have a couple of additional repo so we have securecontract.com which contain additional exercise we have properties which contain inbuilt-in variant for example we have open source invariants or irc20 erc4626 and so on um and yeah how many of you want to try and keynote on the next project oh nice and thank you [Applause] I'm not sure we have time for a question no no we have them okay we have time for a question perfect is there any question

if you have like any question feel free to you know find Natalie or myself [Music] [Laughter] [Music]