A stroll down the security tools zoo by Uri Kirstein (@KirsteinUri)

Transcript

welcome everyone I am Ori and we're going to take a stroll together down the security tools Zoo if you look at the world of security tools that help you find bugs in smart contracts before you deploy your code we can see that there are many different Technologies and each of them has a very intimidating title that sounds very scientific and foreign to most people like static analysis or formal verification invariant testing seems like you need to have a PhD just to understand these terms so today we are going to demystify them and explain what they actually do and

we'll briefly go over how they're implemented but will only scratch the surface what we will dwell on is how they're actually used in practice what you should be mindful of what you should try or not try to do what are the limitations and so on and after we do that we'll also learn how can we measure the effectiveness of our tool usage um and obviously we'll also see some cute animals along the way at first we'll start by explaining what tests are it's just to set up the discussion tests are the first line of defense that you have against bugs in your smart contract code

in this presentation we'll take as an example a transfer function that gets three different parameters two addresses and an amount and that amount should be transferred from the first address to the second so a test could look for example like this in Forge written in solidity so here we have a test that we transfer one token from the address called Alice to an address called Bob and then we check that Bob's new balance is equal to exactly one token so one common theme among all tests is that they all check for a specific input two specific addresses Alice and Bob and a specific amount of one token that we

try to transfer we're also checking for a specific scenario a specific combination of specific functions in this case only the single function transfer what people sometimes tend to miss is that tests usually only look at one specific starting state one what we usually do say in Forge is that we have a setup function where we tell it what are the two addresses that we are going to care about and we were minting tokens so we were actually setting a specific balance for the tokens for those addresses so a test is a combination of very specific things

examples for unit tests that you you're probably pretty familiar with this is that we'll probably try to transfer zero tokens transfers the max you win 256 amount of tokens transferred the entire balance of of Alice to Bob try to transfer to the zero address and and so on and if tests were animal there were a mole because a mole is blind a test checks only the specific thing it was set up to do tests are cheap to ride they're fast and their largest Advantage is that it's easy to understand relatively what weren't wrong when they failed because you wrote the test um hopefully you wrote some

documentation of it and you're looking at a very specific thing so it's relatively easy to trace back and see what went wrong and again as we said they have low coverage specific starting State input and scenario if we want to scale it up and and check more inputs then we would should look into fuzzing and there are several fuzzing Tools in existence one of them is echidna by trail of bits and there is Foundry and there is a tool by um by consensus diligence and there are many others fuzzing in the process of generating many many different inputs automatically and testing all of them

when do we stop so we allocate some limit to the computation usually it's either a limit on the amount of iterations the amount of different inputs that we put or just the amount of time try as many inputs as you can in 10 minutes obviously the more resources we allocate to the fuzzing and we don't get an error the greater will be our confidence that we don't have a bug in the function that we test so obviously there are some examples here on the screen it's just inputs that may look completely random to a human however in practice they rarely are truly random

fathers are always smart to some degree the inputs are not truly random fathers try to optimize for for example coverage many fathers will try to cover as many branches as possible in your code some fuzzers are even smarter than that and we'll check for some storage values in your contract and try to use them as different inputs and so on and so forth this is the difference between the different fuzzing products that there are some fuzzers are actually even smarter than that and can take a different type of test we call an invariant an invariant is something that is always

true about your system even as it goes through Transformations and there are many invariants in D5 one of them you can see on the screen this is a simple token invariant we say that the total supplier of the token is equal to the sum of the balances of all the different addresses which should always be true it doesn't matter which function we're calling that's why it's an invariant another type of invert you can think about is what we call solvency and that could be say a property of a volt and that's basically the opposite of what happened to the svb bank we always have enough assets to cover all our liabilities and so on and so forth and how fuzzers can actually check these

invariants is that they call random functions and usually a series of calls to random functions but eventually it's all the same thing under the hood there is a theorem called the infinite monkey theorem it says that if we'll give a monkey a typewriter and an infinite amount of time the monkey will eventually type the entire works of William Shakespeare and fathers kind of work the same way it's sort of a Brute Force approach in which we're trying many many different inputs in Hope of finding that rare bug which is like the works of William Shakespeare so a father is a monkey

fuzzers are cheap and they are easy to set up usually you can just reuse the tests that you already have set up before we can see that with Foundry and in practice they are very good at catching some classes of bugs which are relatively common meaning that they occur on many different inputs however they still don't cover all the states or all the inputs or all the starting scenarios it can only check some subset of them can we do better I'll give you some motivation for it make her Dao have a stable coin called a multi-collateral die

and quite recently they have found out that something that they thought should always be true about their token is wrong it was called the fundamental equation of die that should tell you what is the ratio between the depth and the amount of tokens that there are I'm not even going to explain what that equation is the interesting thing to see is that this is the minimal example to recreate this bug right so it's a combination of calling eight different calls in a specific order with a specific relation between the different inputs so obviously you can put in between them

some irrelevant calls and the inputs are not specific just the relationship but the chances of us uncovering this with fuzzing are pretty low so what can we do if we'll go back to school for a moment we have all learned the Pythagorean theorem the Pythagorean theorem was proven to us and we know that it's true for every um right angle rectangle and we know this without actually checking all the different rectangles in existence which is basically what we're trying to do with fuzzing and we were able to prove it using mathematical theorems

and this is essentially what we're going to do with the following technology called formal verification form of verification takes her code and transforms it to math and then tries to prove that math equation the downside is that if you transform your code into math you should also transform your tests into math and we call those math tests specification or even formal specification because it's as formal as a mathematical equation there are different types of formal verification the two that we're going to

discuss are symbolic execution and Theorem proving first let's look at an example for a specification this example is written in the sortora verification language which is uh at the input language for formal verification tool by Sir Torah if we look at it we see that it's actually not that different from the test that we saw earlier for the transfer function so we check the balance of Bob before the transfer we transfer some amount from Alice to Bob and we check that the balance of Bob grew exactly by the amount that Alice has sent

what are the differences between this and the test that we saw before well here we don't know what the balance of Bob was before the transfer it's no longer necessarily zero we also didn't set up the addresses of Alice and Bob and more interestingly we didn't set a specific amount you can think of it like an X symbol in math checking for every amount the first type of formal verification that we will discuss is called symbolic execution there are several tools on the market that do this um there is a sartora tool that we've discussed before there is mandicore by trail of bits and there is mithril by consensus diligence and others

the basic idea of symbolic execution is that we give the specification which is the math test and we give the code and we get one out of three possible outcomes either we get a proof which is a mathematical proof that our code behaves as we've wanted to as we've defined in our specification or our tests and that's great it gives us some confidence greater confidence than just trying some subset of inputs another possible outcome is a violation and when we get a violation we get a specific set off a starting state in inputs which violates what we wrote in the

specification and this is an unexpected Behavior which oftentimes is a bug the third option is that the tool cannot decide and just times out symbolic execution is a turtle it gives us the maximal amount of protection see this covers so much and again the big difference between this method and the previous ones is that we have some mathematical proof for the absence of specific bugs and I also want to mention that just the process of writing what we call the formal specification is oftentimes enough to uncover bugs in

the design or the implementation just by itself however as a turtle formalification is slow for verification at its core theoretically tries to solve what we call an undecidable problem which means in practice that first we have to bound what we're trying to do for example we're not proving anything for an infinite amount of iterations in Loops what does it mean if for example we have a function that runs over an array with a variable length we will limit it to say free iterations eight

iterations or some limit what it also means is that it doesn't matter what we will always have some programs and sound specifications at which we will fail fail miserably meaning we will time out no matter how much time we're gonna give form verification will be as useless as a turtle flipped in its on its back and this is unavoidable it will sometimes happen this is inherent to the technology however we see that in practice this is not the limiting factor the limiting factor is the need to write those math tests those specifications which is hard

to do it's not natural for many programmers and there is a problem of what happens when the specification is not good enough if the specification doesn't actually mean what you wanted to prove or there are some Key properties of your code missing from the specification then it's not going to cover you from Bugs it's the same as tests if you didn't write the test that can catch the bug you will not see it and formerification is exactly the same in this regard there is a different verification called theorem proving it's mostly used by runtime verification

with the K framework I'm not going to delve into all the details as this one is a bit more complicated but the basic idea is that they use an even higher abstraction we have a model a mathematical model of the evm and it's already written you don't need to write it again what you do you check the specification against the combination of the code and that evm model so two different mathematical entities and what K is trying to do is to prove that they are actually the same what we say they are equivalent in math and this is a very hard problem sometimes

the prover will need some help we'll need some hints from the user hence why it's interactive there will be some problems that it will say I don't know if it's true or not and the user will need to provide some extra information so that means that we have three different outcomes but not the same ones as the ones we get in formal in symbolic execution one is a proof and that's actually the same if we have a proof then we're happy there are no bugs in the code at least like in this specific instance that we've checked um we can also get a violation however that violation doesn't come with a counter example and now if if we time out it basically just means that we need to give another

hint if we do this enough times we'll eventually should be able to prove almost anything so to sum it up Theory improving is like an elephant it can carry great weights in practice it was used to prove very complex system much more complex than smart contracts it was used to prove airplane software or submarine software and it's also unbounded like I said before we don't need to limit the number of Loops or any other things like that however it takes a while to tame an elephant and that's somewhat true too for if you're improving you need some expertise to know which hints to give to the prover which is is not trivial at

all and there is low explainability meaning again you don't have that counter example so if the proof fails you you need to try and figure out on your own what went wrong and how and that's not easy so we see that writing specifications is um is a drag it's not easy it's hard it takes time it costs money can we enjoy some of the benefits without writing specifications so one thing that basically all formal verification provers come out of the box with is the ability to check that some bad reverting your code don't happen this could be reversed due to assertions in the code division by zero index out

of bounds and all kinds of other things which is nice but very very limited and that's where static analysis comes in and there are several static analysis tools in the market there is slither by trail of Bits And there are tools by Veritas and consensus diligence static analysis is the process of looking at your code and examining it without running it hence why it's static and how it's done static analysis tools have a set of detectors

that are looking for specific pretty fine bugs in your code what does it mean let's look at this example this was taken from very dice's website so we can see that they check for re-entrancy or check for access to uninitialized State variables and so on and so forth there is a list however um while we're trying to have a one-size fetal tool we know that in some design patterns we actually use reentrancy and sometimes we actually do access uninitialized variables in order to for example save gas so not necessarily the things that static analysis will complain about will

be actual bugs in your code static analysis is like a goldfish it's cheap and it's easy to maintain usually you just plug and play put it give it as an input your source code and it will tell you all the problems that its detectors we find it's also very pretty it tells you exactly what was the thing it was designed to find and we'll explain to you the attack show you previous exploits and you can have loads of documentation on every detector pretty like a goldfish however like a goldfish it's confined to its aquarium meaning it will never be

able to find a bug that it was not programmed to if there is no detector for something then the static analysis tool will never find it and also from a practical point of view these false alarms are a real problem there are plenty of fish in the sea this for example is me running slither on one of uh the simple smart contract codes we use insertora for testing and there are several Pages worth of warnings or alarms in this specific case none of them are actually relevant or interesting none of

them are real bug so what you gain in Simplicity of use you somewhat lose in that you need to spend some time in weeding out those counter examples to sum this part of the presentation up in practice each company uses a combination of Technologies it's not a single animal it's it's a it's a hybrid animal so Torah uses static analysis to improve formal verification consensus uses static analysis to improve fuzzing and very dice uses fuzzing to improve static analysis and there are many more

examples so keep that in mind Okay so we've seen all the different animals and now it's time for zookeeping how do we know that um we we treat these animals right how do we know that we are using our tools effectively to find a box one way is to have a human inspect them meaning you have a person an engineer look at your tests at your formal specifications and so on and check if there is something missing if there is something wrong another option is that many tools will report what is the code coverage that they have and you're probably familiar

with this from testing also from traditional software you we have different types of coverage Branch coverage and line coverage and many many others however there is another type which is somewhat less known which is called mutation testing and the idea is that we're trying to test our tests we take the source code and introduce some random faults in it the code with a random fault is a mutant and we expect that Newton to fail at least one tool or one test in our test suit

I'll show an example um this is a code of the transfer function that we saw before it contains no bugs and therefore it should pass all our tests however we've created a random mutant of it in this example we can see that the first line has been omitted has been commented out okay and we expect that this wrong function that doesn't make any sense should fail our tests and if the mutant is not failing any of our tests then we know we have a problem

we know we have missed something we have missed something in the test in the specification or something like that has a mutation testing tool called Gambit and it's actually open source you can go and use it with whichever other tool you want what are the takeaways from this talk different tools different Technologies are like different animals they behave differently they have different limitations different strengths different restrictions and different costs we can see that there is no tool that is strictly better than the others each tool has its own disadvantages and costs and the keys to Security is to try and

combine several different Technologies to cover the drawbacks of each other and find as many bugs as possible to secure our code thank you