Towards Adoption of Symbolic Execution for DeFi Security

Transcript

foreign thank you all for coming I'm Paulina I'm a verification engineer at runtime verification before that I was a PhD student and I also worked with maker Dao on improving the adoption of symbolic execution tools for a smart contract and defy security and that's what the talk is going to be about so let's start with why do we need something like symbolic execution and the short answer to that is because we want to eliminate bugs from our code base and symbolic execution can help us with that because it's one of the formal verification techniques and there is of course more to formal verification than just bug finding but let's focus on this application in this talk let's see how it works here I have a small smart contract example we'll use

in this talk so here we have a function it's called backdoor it takes an input parameter X and in this function we declare a variable y that is set by zero set to Zero by default and then we also have an if statement what it means from the point of program analysis is that there are two possible ways in which which this function execution can take so there are two execution paths one if this if condition is true the condition says that X Plus 1 is equal to 1024 x here is the input parameter which means that if x is 1023 then we'll be taking this execution path in this execution path we set y to 42 and then at the end we have an insert

checking if Y is not equal to 42. what it means is going to fail this condition is going to be violated since asserts are commonly used in smart contracts to express conditions that should never evaluate to false it means that there is a bug in this contract and that's what we'll be trying to detect using the techniques we consider in this talk alternatively if we take the else Branch nothing happens y remains 0 0 is not equal to 42 so the assert is not going to fail in this execution path um so what techniques do we have that can help us um deduct identify this issue here well one of the techniques the most simple one probably is unit testing so in a unit test usually we assume that X has some concrete concrete value for

example we can assume that X is 5. if x is five the if statement this condition does not evaluate to true we're taking the else Branch Y 0 not 42 the third doesn't fail which means that we haven't identified the bug even though we know it's there and that illustrates the insufficiency of relying on unit tests solely for security and correctness Assurance in smart contracts because it provides us with limited information about the smart contract behaviors that'd be inside of course it's it's very useful technique and I'm pretty sure that every project should use them uh besides that unit testing are usually used to analyze happy path and there might be challenging to use in order to identify some unknown issues so in order to increase coverage we can

do fuzzing as well that means that instead of just running our code on a single concrete input we'll be running it on a sequence of randomly generated concrete inputs fuzzing is is very efficient I highly recommend using that as well the problem with it is that all these random inputs can still drive the execution towards the same execution path which means that we'll be exploring it over and over again and we won't be able to identify the bug because it can be challenging for the fuzzer to randomly generate the value that will satisfy this very specific condition that we have here and that is in fact what happens I run foundry's father on this example 65 Southern times I think and it doesn't identify this filter but you can also trade yourself um but I also said that symbolic

execution can help us identify this issue and here is how so the basic main idea behind symbolic execution is that we don't restrict the value of x to some specific concrete input but instead we assume that it can take any possible value and that's what we call symbolic variable then we'll go down every possible execution path and we'll further narrow down the set of values that acts and other variables can take based on the conditions that we encounter in this execution path so the conditions comes come from things like if statements Loops assert requires statements any conditional statement um here since X can take any values it might as well be 1023 so we'll finally get to execute this true branch of the if statement on the left where the

answer it fails the formula on the slide represents the state where the assert is failing um so we'll finally detect it because that evaluates to True indicating that the assert can fail here the input to a symbolic execution tool usually looks something like this normally it's the source code or the bytecode that we are going to symbolically execute the output we want it to look something like this so we wanted to tell us the tool to tell us that the vector function should be called with this particular concrete input for the assert to be violated symbolic execution is commonly seen as a way to generalize testing because it allows us to reason about such of inputs that would be impractical to reason about using for example a test Suite we wouldn't be able to cover as much

besides that symbolic execution can also be viewed as this translation from the source code or byte code to this more formal logical representation such as this formula we can see on the slide and we can reason about this formula but the question now is how do we get from all this logical formulas to the output that tells us with what specific values we should run this code for the assert to be violated and that is what symbolic execution tools use SMD solvers for that's a very sophisticated piece of software smt stands for satisfiability module of theories there are several of them some of them are on the slide but essentially what they do they take a formula this logical formula representing for example the state where the assert is failing in our example it

runs some analysis on it and based on the analysis it tells us either that this formula is satisfiable which means that it can evaluate to true if our symbolic variable takes some particular value such as the one we expect if the formula contains some contradictory Clauses which means that it can never evaluate to true it's going to tell us that it's unsat or unsatisfiable the third type of input sorry of output is I don't know so if you find out of resources it cannot really answer our question here on the slide I have an example of the manual encoding that I have performed of this solidity code that we had in the previous slide that's the translation to the python API of these three smt solver

so we've encode this example and ask if the assert can fail it almost instantly tells us that it is possible if x takes this value that we expected it to show us all together with type in this took me 33 seconds but if you type faster than me you can do even better uh so obviously it's a very simple example but I personally think that it illustrates that symbolic execution is a very powerful tool and technique and personally I think that a year from now it's going to have a very big presence in the smart contract development processes so maybe now is a good time to start adding it to belt um in general there are many symbolic execution tools for smart contracts and as part of our effort to improve and increase the adoption of this technique we have selected an examined some open

source tools the best open source tools for symbolically analyzing evm bytecode so these four tools here made it to the top of our list for usability versatility and being stable in general so the tools are misreal by consensus Manticore by trail of bits hevm originally part of the adaptools framework currently developed by theorem foundation and ivmc which is the only academic tool that made it to our list that's developed by a group at true University at bochum so let's get back to our resample contract and as powerful as all these tools are only two of them detect this fail assert out of the box missile and hevm so all these tools are rapidly changing and evolving but at the moment to use them efficiently and

effectively you might have to tweak their behaviors quite a bit or slightly change the way the analysis is performed so here I'm also going to show some Landmark tips on how to use the symbolic execution Tools in practice uh for example anti-core out of the box doesn't report this assert failure even though it's there however if we'll look into what happens it turns out that multi-core only detects and reports failed a certain solidity versions prior to 0.8 uh when the EDM representation of a failure had changed so even if we say something trivial like assert Falls it will not be able to report that either however if we don't grade solidity version to 0.7 it's going to detect this filter in less than two seconds and we

also similarly added the detection of filters to epmc ourselves so that brings us to the advice number one if the tool doesn't report any issues make sure that it actually reports something add something trivial like a third false and see if it fails because there are a lot of reasons for the tool not to report anything other than Beyond just the code being perfect and correct one other aspect that we're considering is the support of several SMG solvers it matters because the performance of different doesn't dissolvers may vary and for example here the timing all the timings are based on the same Essentials over D3 but if we use a different one in this BMC we'll get an almost 20 times better timing uh here's another example of a tool

reporting that everything is fine over a more complex contract so that is a simplified contract from the makerdale code base that contains a real bug that of course has been fixed it has a function that's called country example that deterministically fails an assertion expressed in an important invariant after the execution of four function calls so the contract is called minivat however if you run mithril on it it will finish the analysis in four minutes but it would still it would not report any issues however if we anticipate that there might be some essential related issues which we should and that's the device number two we might think that maybe the SMD solver is quietly failing due to the timeout in the background and in fact that's what happens and if You observe

some inconsistent behaviors in the symbolic execution tool if it performs inconsistently between different runs there is a chance that there is also some smts over timeout happening if we increase this over timeout missile will run way past this for minutes does it help no it doesn't uh that happens because there are actually a lot of aspects that affect the performance of the symbolic execution tool and in general symbolic execution traverses all possible states of a smart contract so the number of states grows exponentially with the contract size so one of the biggest impact on performance comes from limiting the scope of the analysis and also you can otherwise you can optimize the interactions with the smt solver for

example we're acquiring it less frequently so all this might be achieved by the options that are present in the symbolic execution tools that you're using for example in the end we managed to make missile find this issue in less than two minutes that's the advice number three know your options know the options present in the symbolic execution tool you're running and use them to limit the scope and optimize the performance otherwise for example you can focus on the detection of only some specific vulnerabilities not reasoning about gas and so on overall Miss Roland montic word to python-based tools are flexible and easier to use in general the timings on the chart represent the best most optimized run of these tools to detect the issue that I have seen shown in the

contract on the previous slide um each of payment is BMC the originally has killed and rust respectively are on average faster than the other two so it might seem that the usability versus performance is a trade-off in the existing symbolic execution tools but a lot of efforts are currently being put by the respective teams to improve the situation and one example of that is symbolic testing so that's one of the emerging Trends which allows developers to apply symbolic execution to existing tests that already exist in the project that makes it easier to introduce symbolic execution to the development processes it also limits the scope of the analysis because the analysis will be restricted only to these things that are being executed within the test and in general I think it dramatically

improves the usability of such such tooling so symbolic testing is supported by our old friend hvm we added the supportive symbolic test into his BMC by integrating AWS Foundry ourselves but that's probably a different story there is how much by a16z that appeared quite recently and also there is KVM by runtime verification on the slide we also have the same minivan smart contract but now we have the test instead of the country example function but it encodes essentially the same thing and we'll use it for benchmarking these tools as well right so since symbolic testing is quite easy to use we'll be evaluating this tooling based on their completeness which we Define as the support of complete evm semantics and uh cheat codes that Foundry uses to tweak their analysis KVM is by far the most

complete one because it supports the complete evm semantics and in fact it also passes all tests from the ethereum conformance test suite for ethereum clients it also provides extensive cheat code support and a lot of work is currently being put to make the performance better for example when I run KVM on the same example back in April it took 32 minutes to finish the analysis and identify the issue on a powerful server and now it finishes less than in three minutes on my laptop also take few minutes to finish the analysis but they are a bit less complete and hvm takes just 1.5 seconds it's blazing fast I don't have any other comments here the concluding advice here is that I recommend you find in your tool and

learning how to use it efficiently so with the security guarantees that are inherent to symbolic execution that might give you an ad chain save smart contract development auditing bug bounties probably and all these tools get better and better and easier to use day by day because the teams are developing them very actively this talk is Loosely based on the two blog posts that describe the evaluation of symbolic execution tooling that we have performed and one of them is available on this link on the slide and in addition we have also prepared some Docker containers with this toolsfully set up so that you can try to run them seamlessly and that actually completes my presentation thank you so much and I'd be happy to answer any questions

so in your slide looking at the the usability and the performance how much impact does the usability have on your performance as the person who's actually setting the thing up to run it thank you so much yeah I actually wanted to wanted to say something about it so I have to say that missile and Manchester um rank them as more usable so one of the reasons why we do that is because they provide a lot of options so you can they're quite flexible you can turn off an accessory detectors you can basically do a lot of things to optimize their performance and that's why actually monticore and mystery in the most optimized runs don't perform much worse than usbmc or hvm that are faster on average but are less flexible so

them being usable and and providing more options to adjust the the analysis um well first make them more performant it's easier to extend them so we have added similar functionality to multi-coordinate BMC and it took considerably more effort to do this in ewbmc well it might have something to do with my personal skills because one of is written in Python the Azure is in Rust but it's easier to expand it's easier to add some additional vulnerability detectors and so on so I'd say that it has a great impact but still well so there is a limit to how fast Mysteryland multi-core can be and for example neither of them can complete the analysis in 1.5 seconds as a gvm because they take I think two or three seconds just to start

but in general well I would say it's extremely important um well I hope I answered your questions sort of so what so what I'm trying to get at is you know if I go and pay someone to do this work you doing the setup and the thinking and setting the options that's expensive time right and and that's real time the difference between two seconds and 12 seconds and you know 112 seconds for a report doesn't make any difference it's like by the time you send that to me in an email that that difference is completely irrelevant right and unless there's a really really big difference right well to be fair

that's a simple example and that's why the difference is insignificant and uh in theory more performant tools and for example tools that support several SMG solvers other than one that might struggle with some particular thing we have in the smart contract and we have a lot of those might be able to do something in the end so there are a lot of at the moment there are some scalability issues that are being addressed but the question is essentially whether you can get some results with the tool you're using and it's easier to get these results from the tool that is easier to to tweak uh but in general at the same time if they're not if they're like incorrectly not performant if they want to use one smt solver that does not perform well on

for example what we have there like non-linear arithmetics for example or larger beat factors and we have a lot of those in smart contracts then you won't really be able to get any results even though it might work you know better on something for example so I guess the bottom line is that it take some work to find the tool that works best for you and yeah that's pretty much it the question is whether you're you'll be able to get some results You're Expecting especially if you're talking about a relatively large chord base which might be challenging thanks thanks for the talk um so you showed a small example where the fuzzer couldn't find the bug but the symbolic execution engine could um and what I was thinking there is that

a lot of coverage based filters may be able to easily find that bug because they're going to be um coverage directed right so could you just elaborate a little bit more on the advantages of using symbolic execution over a coverage guided buzzer sure well I'm to be very less familiar with coverage based funding I think the question is still whether it would work in some very with some very sophisticated smart contract that contains a lot of for example nasty conditions if you have to very carefully devise what input variables should be in order to pass all these checks in general yes so I agree that definitely I think the fact that it doesn't identify these issues in the smart contract just characterizes the fathers that I have

used as you know having limited ability to reason because if you simplify it they'll be able to find it but in general yeah I would say that symbolic execution is probably is generally considered more useful when it comes to some conditions that are constructed in a way that is very hard to bypass them without some automated mathematical reasoning about what value should it take thanks thank you