# Introduction to fuzzing - Josselin Feist | Trail of Bits

- Speakers: [Josselin Feist](https://streameth.org/speakers/josselin-feist)
- Channel: [ETH Belgrade Community](https://streameth.org/eth-belgrade-community)
- Date: 2024-10-07
- Duration: 30:32
- Topics: People & Blogs
- Watch: https://streameth.org/watch/yt-wW-RhVJs8KM
- YouTube: https://www.youtube.com/watch?v=wW-RhVJs8KM

## Transcript

[Applause] hey everyone so let's wait for the slide perfect okay um I just want to start by saying thanks to the organizer like this week is really cool and it's my first time in Serbia so thanks for our our all of this organization um but today I want to talk about fing and I want to do an introduction to fing um before we start how many of you have used a f a fether um in their life oh okay so more than usual which is pretty good um okay first things first who am I my name is Jan Fe I'm the engineering director of the blockchain team at TR of bits if you don't know us we are a security company where we specialize in highand security technology we work on blockchain but we also work on traditional application security cryptography machine learning and so on one thing that I think defer us from a lot of our competitor that we are research oriented and as a result we publish a lot of academic paper blog and also tools and we have published a lot of Open Source tools such as slitter Aina Medusa caracal and so on that you might know but today we are going to focus on fuzzing and we are going to see why we are using fuzzing what it is how to use it and how you can kind of use this type of technique on your day-to-day you know activity as as a developer or security researcher the question we are going to try to answer here and the things we're going to focus is how to find bugs so if you have like this piece of code okay it's working if you have this piece of code U it's like 10 line of code you have two function it's a function to buy some token based on some price and you have a one uh to 10 ratio when you send 10 one you receive 10 tokens how do you know if there is a bug how do you know like if there is something going wrong here there is not a lot of code but you know it can have some impact usually you have four techniques to find bugs as a developer or security researcher the first one the first technique which is I'm hoping uh used by everyone and everyone is aware of it is unit test basically you call the function with a specific input and you try to see what's the outcome of this this is really kind of well known in traditional software development and also in a blockchain with toolkit like art or Foundry the thing is that from experience unit test are not going to prevent having vulnerability in your code base and the reason for that is but most of the case when you are going to write unit test you're going to test for the happy path you're going to test the program to see if it behave the way it's supposed to be in kind of like the expected PA U the think that most of the vulnerability are going to lie in the edge case in the kind of small detail or in the situation where you did not think about the code base we actually have have done a couple of research on that and we were looking to see if there was any correlation between the quality of unit test and the likelihood to have critical bugs in a v in a code base based on on our security overview and we could not find a strong collation between both which means uh from from our from our empirical experience there is no direct correlation between quality of unit test and likelihood of having bugs let's say you have other technique that you can use the second one is manual analysis basically you go line by line you read the code U when you go to a security provider when you go to a bug contest or a bug buy most of the people are going to do that they're going to sit in front of their screen and just look at the different line of code and try to manually understand what can happen it's really powerful but it's time consuming it's expensive and uh every time you change a card you might impact what you are building so it's not something that is necessarily robust over time then there are two categories that I'm going to do a bit more of a deep dive which relies on tool fully automated analysis and semi-automated Analysis by fully a automated analysis I mean uh tool and technique that are kind of oneclick buttom something where you just run a tool it give some result you you tri the result you know if there is a bug or not uh a common example is slitter which is our static analyzer you can see on the screen or GitHub integration where you can One S it's going to look for common vulnerability reury lack of Access Control this type of things and is going to try to find common bugs it's really good at finding common pattern however uh it's not going to find more complex vulnerability it's not going to find things that are a bit more related to your own business logic in addition to that it might create fce alarm so it's not because this type of tools and technique find a b that BG that there is a bug you need to triage let's say from our experience triaging this type of result will take you like half of an hour one hour so it's something we definitely recommends to do the next technique and the one we're going to focus today is on the category of semi-automated analysis so here you also going to use a tool but instead of being a click buttom one click buttom something you just one and you don't have any configuration or anything to do you need to provide some information you need to provide some configuration it does require what we call human in the loop so you need a bit more expertise to use and in particular we are going to focus on one technique which is called property based testing uh with a fuzzer which we have built which is called a so I've been mentioning fuzzing a bit I've been mentioning property based testing what does it mean on a really really high level fuzzing is just a tech technique to generate input to your program if you want to think of the most basic way of doing fuzzing uh um you know from from a user perspective you open your application and you go crazy on your keyboard and you look what's going to happen to your application is it going to crash is it going to reach something which is a bit real is it going to trigger a path that you did not consider uh so it's really a technique you Generate random more or less randomly input to your program it's a it's a technique and it's a it's a type of tool that is really well established in traditional security and traditional software engineering with further like AFL um leap further go f and so on now property based testing is a specific variant of fuzzing where traditionally fuzzing is applied to find memory corruption like segmentation fault buffer overflow if you have worked with more traditional language here what we are trying to look on Smart contract we are to trying to look for business logic issue we are trying to find um problem in kind of like the specification of the code base trying to find problem that are related to the specific logic of of the of the contract of the code base how we do that first we define properties we Define invariant um then we use a further to Generate random input to the contract and we use a tool to check if the property or the invariant is still true no matter of the of the of the input the way you can think about that if that on a really high level when you do a unit test you call a function with an input 10 you do the same with further but instead of calling the function with 10 the further is going to call the function with arbitrary value 10 20 1 million 100 so it's kind of a way to do unit testing but on steroid like you try the same kind of philosophy but you do it with way more input I've been talking about invariance I've been talking about property I'm using the same um I'm using both term but it's the same terminology basically an invariant or a property is something that should remain true over your code base um for example if you have an nc20 token and you have a total supply of 1 million one invariant is that no user should have more than 1 million right if you have a total supply of 1 million and a user has 2 million token probably something is wrong right so this is an example of simple invariant you can Define over Val your Cod base okay a now so Aina is our open source and free smart contract further um we have been working on it for probably five to six years now uh it's a it's a it's a it's a further that we have been eily used in most of our Audits and also by by some of our clients you can see a couple of oh can still see it okay sorry um yeah so it's um it has been used also by many by many clients directly on their code base you can see a couple of name here thank you um how does it work on a high level you have your smart contract code you define your invariant in solidity and you just run the further and the further K is going to try to break this invariant if we take as an example A near C20 token again a really simple contract but here we have um someone who are trying to kind of optimize gas and they are using uncheck operation for arithmetic if you have a bit of experience with solidity you can def you can directly spot that here there is a bug you are using uncheck arithmetic operation to update the balance which means that there is no check and if you send uh if you transfer an amount of token which is greater than your balance there going to be an underflow and it's probably going to be bad here how can you define an invariant so here an invariant will simply be that the user so balance you see yeah um the balance of the user is below the total Supply which is which you define to be 10,000 so you define the total supply of the contract to be 10,000 you write an invariant which is three line of code and you run the further if you run the further on this invariant is going to tell you it failed so it did find a way to break this invariant by calling the contract under the wood the further is going to call all the function of the contract with arbitrary value and is going to try to see if this in variant total supply of the balance uh user balance is below the total Supply is still true here it says he managed to find one by calling the transfer function where the destination is zero and sending 10,093 token if we go back on the example this is a vulnerability I was hinting there is an underflow in this contract so if you transfer more asset that you have in your balance you you you can actually do that and you receive more token than expected the thing which is interesting here is that we were defining an invariance over the total Supply over the balance but we were not thinking about the transfer function we are just defining the general invariant of the pro of the protocol and the further by exploring randomly all the function by exploring randomly all the kind of possibility of the contract did find a bug in a place we were not looking for and this is really I think as as an intuition it's a really good way to find bugs because you are not going to look at the function themselves you just Define in variant and the further does a job for you now the question that you might ask is how you define inv variant because like the lc20 was a bit of a simple one and how we can do it for more complex protocol how we can do it for things that are a bit more difficult to understand here there is no magic solution the way we approach defining invariant and property with our client and in in the Cod base we are reviewing is that we have an iterative approach we start small we start simple and we go more and more complex over time if the first invariant that you are writing leads to a bug most likely there is something really wrong in the way you are you are developing software uh so start simple don't try to write solidity in variant from the scratch start with English you open can open a markdown file you can open a text file or you can write on a whiteboard whatever works for you and start to think about what are the property of your code base what are the specification what should be uh the different Behavior of of your contract and iterate so you start with the English specification you write the solidity code you run the further either it pass and then you can start and go back on the on the English definition or it breaks and if it breaks either you found a bug which is great or your invariant was false and uh from practices when you start writing invariant it is likely that some of the invariance that you are going to write are actually not correct you might have assumption about the behavior of your program but this might be false to give you kind of a couple of traditional example of invariant to give you some some insight if you have an arithmetic Library if you have a math Library U you can use some of the common property that you have seen you know when you were you were kind of learning about about arithmetic I guess commutative identity inverse now if we think about a bit more complex system we have the erc20 total Supply example that I use at the beginning the balance of a user should not be greater than the Supply but is straightforward if we go a bit more deeper and if we we think about the transfer function and if we think what's the behavior of a transfer so if I'm sending 10 token to to someone else and I think about what's going to impact the balance my balance should decrease by the amount and the receiver should increase by the amount right I'm sending 10 token I have less I have 10 token less here has 10 token more well if you write this as an invariant and you run the further it's actually going to tell you that it's wrong and the reason for that there is a specific Edge case if the destination is yourself the balance doesn't move like the balance doesn't change if I send 10 token to myself the balance is the same this example is just to highlight that sometimes you're going to think about an invariant in a way that it seems straightforward it seems like okay you you understand how the system is behaving but actually it can be more tricky that's why like an iterative approach starting starting small as simple and moving into complexity over time uh is what we we use something to consider also is to consider reverting we on FS to consider um that when the the function is not supposed to be able to be executed it's not actually executed like for example if you don't have enough funds the transfers should revert or R false depending on your uh behavior on a on a high level we usually categorize invariant into uh two categories the first one are function level invariant so think of invariant where you just Define with respect to like a specific function arithmetic associativity or like the transfer of function level invariant most of the time they are stateless in the s that they don't require to change a state I'm saying most of the time because sometimes you have a function and you need to consider the state um they are usually a bit more simple to test and they are simpler to start with then we have system level invariance so system level invariant are really invariant that are not dependent of a specific function and should remain true across like the entire system the total Supply versus balance of the user is an example of system level inv variance there are more powerful but also more tricky to to Define so start with function level inv variance um here kind of a simple strategy is that you just inherit from the target you create a wrapper on on the function you want to call and you just check whatever property you wants to check so in this example we just take uh we check that a plus b is equal to B plus a and we use an ass for that for system level inv variant as I mentioned it's a bit more complex usually you need to set up like the system you might need to deplo multiply contract you might need to kind of set some parameter U you might want to get to a point where you first or you have enance into specific state of your of your system if you think about a landing protocol you might either want to have system invariance that are going to Target opening a position closing a position liquidating a position maybe you want to narrow it down and you want to say okay I'm going going to have a concrete example where I open a position and I'm just going to f what can happen after OPP position is open this is depending on what inance you want to test this is depending on the complexity of the system if we go back on this example so again there is two function here buy which is just a stateful function receive some token receive some ether means some token and valid by which is going to check that you are sending enough token and again here we have like a a conversion of 1 to 10 one is equal 10 token where to start here we have two function and if we if we go back to our discussion where to start we have a state full function by and we have a stat less function valid by so let's start with valid by it's a it's a simple function just take some parameter and revert when you don't provide enough amount so what invariant we can think of here um the most simple I think one of the most simple invar we can think of this is a function that takes some amount of token and take and take how much haer you sent one thing you can say is that if the amount of haer you sent is zero you should not be able to receive token if I'm if if I'm sending zero iter I should not be able to meet any token um so here is how you can Define the invariance with a caveat because I updated the slide yesterday there a bit of a typo here it should be assert desire amount is equal zero um this is why you don't update the slide the day before the presentation but yeah basically the idea is that you call the function and you check that the invariance so you cannot like if you send zero token if you send zero it should be zero token if you run this with a kidner it's going to say it did manage to find a bag it did manag to find a way to break this invariance why is that if we go back to to to the code and we look a bit more deeper the way we do the arithmetic here is that we take the number of token divide by 10 and multiply by decimal and the further told us that it did manage to mean some token for free with an amount of one here because you have a division by 10 if you send any if you try to meet any number of token between one to to nine up to 10 the division is going to run toward zero and basically like this was the equation is going to be zero this is an example where due to the lack of precision of integral arithmetic you can basically get any token for free if you me between one to nine this is again an interesting example in the sense that we were not necessarily looking at the formula like the formula here is simple but you can imagine more complex formula in defi we were not looking at the formula we were looking at the output of the formula and by defining an invariant over the output of the formula the further found a bug in the arithmetic self okay so Aina is not the only tool that works you know that way and and and can find bgs based on on invariance there are many other further out there um from D B fundry I believe fundry is right now probably the one which is the most used by by developer um all this additional further I think they are probably easier to use like it's the first if it's the first time you are writing an invariant if the first time you are using a further probably it makes sense to start with with a Foundry one just because it's going to be simpler that say uh they do require specific compilation framework Foundry you need Foundry and if for example if you if you use hard that you might have trouble with that uh and there also from our experience they are not as advanced as a Kina as I mentioned we have been working on Aina for five to six years now a lot of kind of like the optimization and like the fine tuning on the value generation on all that stuff have been really kind of pushed toward our usage and push thanks to all the Cod review we have done there is an additional category of techniques and tool that you can use to check in variant and this technique are based on formal method a further is just going to randomly generate input over your program and try like some some some of the path a formal method pays tool is going to on a high level create a mathematical representation of your code and of your invariant and is going to try to check if this mathematical representation um is valid or not they are powerful in the sense that you can have proof like it's mathematical representation you can have a proof of what you do that's say from experience and and I've been working on on symbolic execution and on further for for a couple of years they are significantly more difficult to use there is a lot of HK there is a lot of inside knowledge that you need to know about how this tool and techniques works so just if you want to apply formal method on your code base it is going to require a lot of time while with a further within a day you will be able to start so formal method are a good tool like you know KVM C and from from one time verification and from C they are good but we would not recommend to start with that if you have thinking about inv variance um in comparison like you can yeah you can start much more easier and faster with the further a couple of additional things that I did not mention here but we have a lot of additional options a lot of additional featur with Kina we have for example a mod where we can Target high consumption uh gas transaction if you want to know is there is if there is some risk of Daniel of services we can do differential phing we can work with any compilation framework and so on and so on um and yeah it's free and open source you might have heard of Medusa so Medusa is our second SM contract further tldr we are taking all the lesson learn that we have you know acquired by building a k and we are rewriting our further Ino um it's still experimental it's still not up to it's a bit behind A9 some of the feature but in a couple of months um we will be able to do the switch if you like to try you know beta version if you like to try experimental software please you know try it and and give us feedback we are trying to uh you know make it as usable and as performant as we can okay so I hope that the kind of T of what you can take from this presentation is that thinking about invariant is a really powerful way to to find vulnerability and to build better software from our experience it's not necessarily about even using a further or even using formal method but just thinking about invariant you know go go over like a markdown file whiteboard or what you wants to use and defining what the system is supposed to do is going to help you you might directly find bugs just because you're writing the specification the our client that have a specification that have some form invariant Oro specification they have more mature software they have more mature code base and you can see directly from the quality of of their code when they have this type of approach when they follow this Paradigm um if you want to start keep in mind start simple start with the most common invariance start withun function level invariant and iterate over time iterate over complexity it iterate over size finally um as I mentioned we have been using further for like a really long time and we recently launched a Services which is called invariant development of the services where we help our customer understanding what are the envirment of the system how to integrate further in their you know Ci or integrate like a further in their development process how to deploy the further in the cloud and so on if you are interested to learn about about this the services um there's a CER card for that um thank you for our attention and if you have any question um now is the time [Applause] yeah thanks for the presentation um I just want to I I just wondering about one topic that had just come out from the Twitter recently have you ever heard about GPU based fuzzing and how you can accelerate uh fuzzing capabilities uh using like gpus like h00 or something really good question um I don't have yet a clear answer on the GPU based further because I haven't seen practice some of the Challenge from dpu G GPU based feing solve in practice uh typically I'm thinking about storage like how do you manage storage when you you first over the GPU U maybe there are some technique that some of this team have you know find the solution for uh there is some you know discussion over Twitter I'm waiting to see the final result to get an opinion but it is it is an interesting topic and actually at TR bits a couple of years ago we were exploring GPU fing but for traditional application not for smart contract so maybe we will see a speed up at dbd does that answer your question do we have any more questions yes what has been the best case scenario for a client providing information to help make the creation of the invariance easy uh is I know specification also implies better code but is a specification best and if so in what format okay that's a really good question I don't think there is a specific format um we can be you know we can adapt whatever they provide but I think if they have some form of specification or Pudo specification doesn't me doesn't need to be like fully formal um it helps helps a lot and also to demonstrate which one what's the status of which one because sometimes you have like you know they know about 20 variants they have check three of them manually they have checked one of them with formal method two of them with phing it gives us some insight into into what they have done uh something it's also useful for us is to know what they want to cover but they could not uh because sometimes you know like they're going to focus on writing in variant for like I don't know like a math Library it's it's it's a common theme but maybe they did not consider like the integration with protocol or things like that so it's really about understanding um what they want what they are at and where we can get them for the next step yeah I have a like two questions about one thing first about uh when should you think like uh people need to do f in like should they cover everything or just very specific uh uh code that had a lot of complex math it's a person one that's a really good question um for the invariant definition as soon as possible like from the invariance standpoint like defining what what function should be should be doing should be done as soon as possible using the further might depend on on how you you build a software um I think for example if you are writing an arithmetic Library you should probably use a fuzzer from the beginning because it's going to help you to understand better how how it works if you want to fuzz like more complex integration um you probably want to start with unit test like you want at least to have like a unit test being able to you know test whatever uh process or whatever behavior of the system and then you can move into fuzzing uh but I think for anything which is stand alone in that sense like a library or something like that you can probably start with fing for something that is a bit more complex complex start with unit test and then move toward phasing for the inant definition I think as soon as possible thank you and the second question about you mentioned also formal verification of course it's quite hard and complex thing but can you just find the boundaries when you can just limit with the fing and when you can go to the formal verification MH that's that's a good question so when to switch from fing to formal verification um the first question I think to answer for for yourself is resource how much effort and how much time you can spend into that area because at the end of the day security is a budget question how much you know effort are you going to invest there if you have unlimited budget then you can probably do fing and formal verification on a large part of the code base then if you have limited budget and let's say you want to spend one month internally doing some formal method over you know like over your code um if you haven't started with fing it's probably going to be way more costly for you to get anywhere so start with feing once you have like a good definition of the feather and you want to apply formal method identify the components that are going to be the most amendable for formal method and that are going to have the highest impact with respect to your code base uh for example um if if you want to apply formal methods on composability is probably going to be tricky because you might need to write a mock of like whatever contract you interacting with you might need to write like additional wrapper you might need to write some stuff with respect to the underlying formal method tool you are using so this might not be easier for you and you might anyway work on a model and not on the actual representation of the code so here instead you might want to focus on yeah arithmetic access control all these type of things um some place where it makes also sense that if you are trying to write an optimized version of a code base you you write like your code in assembly like let's say you go full you know full assembly on your contract maybe write a version in solidity do differential phasing to compare both implementation if it pass use formal method to do like an equivalence check over the two model so like this is a good example where it makes sense I time unfortunately we don't have I'll ask after the the talk yes feel free to to chat after the the talk and please give one round of applause