Practical Symbolic Execution for EVM | Palina Tolmach, MakerDAO | ETHTaipei 2023

uh thank you very much thank you all for coming uh I'm Paulina I'm a PhD student at nanian Technological University in Singapore and I also worked with maker Dao on making symbolic execution more practical and that's what the talk is actually going to be about so we'll take a look at why do we need something like symbolic execution what it really is how does it work and how we can practically apply to the smart contracts that we are developing so why should we care about symbolic execution anyway and the short answer for that is because we want to eliminate bugs from our code and symbolic execution can help us with that because it's a very popular verification or a bug finding technique so the problem of smart contract verification looks something like this we usually have some smart contract source code we want to make sure that it's implemented securely and correctly and we can define a set of properties for it properties essentially are a specification it's a set of statements that describe how the smart contract should work what it should do what it should not do a popular type of property is the balance invariant you can see on the slide which states that the sum of user balances should be equal to the total supply of this token we can also Define a more general property stating for example that the contract should be free from particular vulnerability and so on so once we have defined the source code and a set of properties for it we can pass this information over to the verification tool that is going to use some mathematics in order to analyze the input and either it's going to tell us that all the properties hold and the implementation looks correct or it can also tell us that one of the properties is violated which indicates that there is a some issue with the implementation symbolic execution and formal verification in general belong to a wide range of techniques that can and should be used in order to perform the correctness and security Assurance of smart contracts with other approaches from this range including for example unit testing or fuzzing which are more lightweight techniques although very effective so they definitely should be a part of any smart contract development processes however symbolic execution and formal verification in general are often seen as a more comprehensive way to analyze the code and we'll see why so as I was looking for some example that can help me prove my point I came across this issue created in The Foundry repository um I hope they don't mind me using that um it's just a very illustrative example but I mean Foundry is a great tool anyway so this code here that you see on the slide contains this very specific if statement which requires that X should be equal to this very random constant X is derived from new number which is the input variable by subtracting one from it so what the issue is saying is that for the father that is used in Foundry it's very hard to randomly generate the input that would make this condition become true therefore allowing the exploration of the corresponding execution path just because it's so specific we'll talk a bit more about what fuzzin does um yeah but that's the issue and symbolic execution can actually help us with this particular case I slightly changed the change this code for the purpose of this talk we're going to use it throughout the talk as an example so what we have here is the function called backdoor that takes X as an input parameter as an argument then we initialize the variable number we set it to 99 that's just a random value we initialize Z which is x minus 1 where X is the input parameter and then in this code we have an if else statement what it means for us from the point of the analysis is that there are two possible ways in which the smart contract can be executed if Z is equal to 691 I slightly shortened this constant uh then we set number to zero and in the next line we have an assert statement that checks if number is not equal to zero what it means is that the assert is going to fail because we just set it to zero zero not being equal to zero evaluates to false which is the assert violation since asserts are commonly used in smart contracts to express conditions that should never evaluate to false uh if a line assert usually indicates a bug or basically any sort of issue so that's the problem in the smart contract we'll be looking for in this presentation we'll be trying to detect this particular issue if the else branch is taken number is set to 1 and then the assert is not going to fail because one indeed is not equal to zero at least using the arithmetics we consider in this case so the assert is not going to be violated in this Branch but will be if you know the true branch is taken so we know it contains a bug what techniques do we have that we can use in order to try to identify this issue well uh to start with we can just try executing this code by assuming that X has some concrete value for example four and that corresponds to testing so that could have been a unit test effects is four then Z is four minus 1 which is three three is not equal to 691 so we're taking the else branch number is one one is not equal to zero the third is not violated and the bug is not found even though we actually know that in the other Branch it would have been violated and that highlights the limitations of unit testing so obviously unit testing is extremely important every project should use that but it also provides us with limited information about different states in which smart contract can end up in however to increase the range of our analysis we can also instead of executing the code on one specific concrete input we can try to run it on a series of concrete inputs we can write it on 1501 very long numbers something else does more or less so if you weren't able uh to catch the workshop by not yesterday basically just runs the code on some randomized concrete inputs hoping to identify some edge cases however you know that's that's a very specific I mean sorry that's a very effective technique that can help us Identify some of the issues the potential problem is that is that we can keep executing the same execution path if in the interesting path we have this very very specific very random condition that is very hard to satisfy using randomized inputs and that's what the issue that I showed you before from The Foundry repository scene we can actually try it out ourselves to make sure that it doesn't work uh so here I hope the font is big enough uh that's the same smart contract that I've shown on the slide and I also have prepared a Foundry project with a test uh to try it out so here we have the test Vector function that calls this back door within this test X is the input variable so it's going to be fast by Foundry if you're on Forge test so let's try it out sorry um yeah so we were not able to identify this issue the test can pass even though we know there is a failing assert happening in it however I also told you that symbolic execution can help us with that and how does it do that the general idea behind symbolic execution is that instead of running the code on concrete inputs we assume that the input variable can be symbolic we can have a symbolic value a symbolic value means that it can potentially take any possible value but we'll be restricting this out of possible values that this variable can take in accordance with the conditions that can be observed in the execution path we are taken so we'll be narrowing down the possible set of values as we go through the contract and once we reach for example the final or interesting state where we want to check if the assert is violated we can take a look at all these collected constraints and see whether that's actually feasible or maybe the constraints are contradictory so we cannot really end up in this state so let's take a look at the example if x is symbolic then Z is symbolic value -1 which is still pretty much any value especially if we assume that an overflow sorry underflow can happen if Z is anything that it can be equal to 691 but it can also be equal to anything else which makes both of these branches feasible so both of them can happen now and both of them should be explored and then we'll finally be able to execute this identify this failure on the left however for this if true Branch to be taken Z should be equal to 691 and that's exactly the constraint or a condition that we need to record so for this execution path to be taken Z which is symbolic value minus one we also established the relation between these two different variables so these should be equal to 681 for for that Branch to be taken for this to happen then we also want to check if the assert can fail in this case so the feeling assert corresponds to the um for so we need the negation of what is enclosed in the assert to become true so the negation of number not being equal to zero should be true um so the number should be equal to zero that's what we express using this formula so number which is zero because we just set it to zero not being equal to zero in the negation of that should be true that's that corresponds to the failing assert if that is true then the assert is failed and we identified our issue at the same time we can also explore the else branch uh however the the opposite uh should be true so Z should not be equal to 691 and then in a very similar fashion we're also expressed in the field assert so number not equal to true the opposite of that should evaluate to true for the assert to be violated however that's one example of this contradictory you know statements that I've mentioned before because number is one uh one not being equal to zero evalu is to choose the opposite of that is false the assert can never be violated in this case and that's good so we're we want the asserts to not be violated so here we don't have an issue but we have one on the left um so what we did here we took the source code and translated it into a more formal or logical representation that we can formally reason about uh the input to a symbolic execution Tool uh usually is the source code or the byte code that we analyze assuming that the inputs or some other variables are symbolic and the output should look something like this so we want to see that the back door function can be called with 692 which is 691 plus one for the assert to be violated how do we get from this logical formulas to the concrete concrete output telling us the exact number with which we should call it for that we used the tool that is called smt solver that's a very sophisticated complex piece of software we'll just assume that it's it's a black box smt stands for satisfiability module of theories there are different types of SMG solvers you can see some of them on the slide what they do they take a formula that represents this this path conditions or constraints that we have collected and it checks if they are satisfiable and under what under what conditions so what value what concrete value should the symbolic variable take for this to become true so the conditions you see on the slide right now are they're corresponding to the failing assert so that actually can happen so if we set it over to the SMGs solver it will tell us that this set of constraints is satisfiable it can become true if x is 692 which is what we're looking for if we Supply a set of formulas that is not satisfiable that cannot become true such as 1 being equal to zero an essential solver should tell us that it's on Sat which is which means that it's not satisfiable no assignment to X which is a symbolic variable uh exists that we can make it become true the third possible option is uh I don't know as an essential solver can tell us that it doesn't know if it's satisfiable or not if it runs out of resources so in the previous slide We performed this manual translation from the source code to this logical representation another more automated way to do that is to just directly encode it into the language that an SMD solver understands so let's try doing that um these three is one of the popular SMD solvers developed by Microsoft research it has a python interface so in order to use it we can run a python shell I can probably make the font a bit bigger so what we need to do here we need to import everything from the Z3 library and then we can start encoding our program directly into this language so what do we have in our program we have a parameter called X which is a symbolic variable and what this statement is saying is that X corresponds to a symbol of type integer which is an acceptable simplification for the purpose of this talk uh what else do we have we have Z which is x minus one uh and then we set number 299 and then we get to our if statement so whatever if statement is basically saying is that the number is either zero or one depending on whether Z is equal to 691. um we can express that using the if construct in these three so we're saying if Z is equal to 691 then it's zero otherwise it's one uh all right so the only thing left is to check whether the failing assert can can actually can actually happen and for that we use the function called solve what we need to provide within this function is the expression we want to evaluate uh which in our case is the failing assert which means it's a negation of the condition enclosed in the assert which is a number not being equal to zero which is equivalent to the opposite of number being equal to zero and there we go so almost immediately the SMG solver tells us that it is indeed possible if x is equal to 692. so that's basically what symbolic execution tools do under the hood um right so what existing symbolic execution tools are how can we actually use it uh we have performed more or less comprehensive evaluation of existing symbolic execution tooling there are quite a lot of these tools it's a relatively popular way to perform vulnerability detection um they differ in implementation in the implementation language the essential solvers used in a lot of other aspects today I want to take a look at mistrial and ifbmc which are two tools out of well all that we evaluated uh so let's get back to our our concrete example and see how we can run it and whether that works in general so here is the code that I've also also showed on the slide so let's start with material that's a python based tool um in order to run it let's also time it we can run Miss and a which is a shorthand for analyze and then we also we only need to provide a pass to the smart contract we want to look at and in a couple of seconds 2.6 to be precise it actually outputs the result it tells us that the assert can be violated if the backdoor function is called with 692 which is exactly what we were looking for um another tool that we can also try is is BMC so sbmc is a rust-based tool um It's relatively fast however it doesn't take solidity files as input which is also common among verification tools for smart contracts so first of all we need to compile the runtime byte code for the smart contract which we can do using the compiler and providing the bin runtime flag then we also specify the path to this contract there we go so now we get to the runtime binary that we can copy paste to the configuration sorry configuration file of the that asbmc takes so it we have to copy paste the code here and we can also set up some other additional values such as the balance of the contract we're analyzing the nons we can set up the state here and specify the address of this contract that's going to be used once we've done that we can actually try running is BMC on that we'll also time it so we're saying isbmc and then we provide the pass to this to this configuration file and there we go uh so it outputs the results in 0.2 seconds which is extremely fast if you ask me it tells us that the assert can fail and then it also provides the cold data with which the smart contract should be called uh in order for the assert to fail however uh we also have to decode this ourselves so it does not tell us the exact function name and parameters but we just you know outputs this undecoded call data however you can trust me I checked that it's exactly the output we're looking for and this 2b4 is actually 692 in hexadecimal so that works and it's actually quite fast another thing we can try is to make the our example a bit more complicated so in a lot of cases it takes longer more than one transaction to get to some interesting Behavior or Identify some issue so we can make our code a bit more challenging by adding the variable life which is a Boolean variable to our contract that can be set using this set life function and this variable life should be set to true in order for the backdoor function to be executed successfully and reach the failing assert so in this case we'll be looking forward to to function calls in the country example we can run with material on it again and we'll see if it's going to uh show us some results it takes a bit longer but right so now it takes 4.

6 seconds versus the previous 2.6 seconds but it shows us the output we were looking for as well so first it calls the satellite function with the value true and then it calls the vector function in a similar way as we did before um for consistency we can also try that once again with the with sbmc let's recompile the code that we copy paste the runtime binary which became a bit bigger since the last time and let's run it again uh okay it's still extremely fast so it still takes less than half a second this time it outputs two transactions uh the first one being live this one here corresponds to the value true in the cold data and uh well the other equal is same as before but you know we still have to decode it manually an important thing that I forgot to mention we had to add the assertion failure detection ourselves so in order to detect failed desserts you should run our own maker dials for coffee with BMC but it does detect some other vulnerabilities by default um so was this um we can see that missile actually has a very usable user-friendly interface um it takes the solidity files as input and it's it's very easy to run and it shows you the decoded output sbmc is extremely fast um but it also requires a bit of additional work on the ux side so that's one example of the trade-offs that are made in the existing symbolic execution tools and there are some others so um well there are always some aspects to evaluate with the existing tooling one way to make a symbolic execution more usable and practical that I think is a recently uh developing rapidly developing trend is to perform so-called symbolic testing so instead of running our symbolic execution tool directly on the smart contract and trying to analyze all possible function calls and all possible sequences of function calls until we find a vulnerability what we can do is we can just symbolically execute the test itself so in a similar way as we first this test backdoor function before with Foundry which was not able to identify the issue we can also try to symbolically execute this call so we'll assume that X here is a symbolic variable and you know we'll just execute whatever is included in the test uh one very recent tool that has been recently released is helmets I think helmish is a right way to pronounce it um by a16z which is also very easy to run we can just let's also time it we can just type uh how much in the in the command line and in three seconds it tells us again that we should call this function with this argument uh in order for you know for the SR to fail um one thing that we have personally experimented with at maker dough is the integration of with BMC that we have just seen with Foundry in order to you know make it a bit easier to use and also facilitate this symbolic testing so with esbmc we can write a function that starts with the keyword proof because we need to distinguish between tasks that are going to be fast and the ones that are going to be symbolically analyzed so the functions that start with proof are going to be symbolically analyzed if we say if we run the Forge test command but for that I'm also running my uh my Fork of both Foundry and ewmc but if you run Forge test uh there we go here is the result um it outputs again pretty fast it shows us the the decoded output that says that we should call this proof backdriver test with the argument 692. uh so we'll here we leverage the capabilities of Foundry to do the compilation uh and and they the decoding uh of the output result uh which I don't know I hope it makes it a bit more useful and user friendly uh you can try it out yourself uh we have here's a link to the blog post which describes more in more detail it describes our experience of running all these tools um and well basically everything we had to do to uh to analyze them and also we have prepared the docker containers for all the tools we analyzed in detail so that you can also try them out relatively quickly uh with that I would like to conclude my presentation thank you all very much once again and I'd be happy to take any questions [Applause] any questions sorry I came a little bit late is this meant for developers developing their own contracts because how does that compare with this code coverage or Branch coverage you know it seems to do the same or is it mostly used to analyze other people's contracts well um so ideally I personally would love to see that being integrated in the development process and that's also what we wanted to achieve with this project in maker Dao so ideally the developer with the symbolic test center I have just shown uh ideally the developers should be able to run it himself in a similar way as he does unit tests or first tests but but isn't but isn't unit testing with code coverage um probably easier it is it is it is easier for sure it's less resource intensive but this in this way you can get a slightly better a more comprehensive analysis more comprehensive results they are more exhaustive they cover all possible input States ideally but of course that's subject to some constraint limitations that we have uh but yes so if you look at um some of the academic tools a lot of the tools that I have shown on the website on this slide with the like the existing symbolic execution tooling a lot of them are academic tools that are made specifically for vulnerability detection and they're just being run on basically the side of smart contracts on other people's contracts on other people's contracts yeah so you just scroll them from Israel scan and then you run it and you identify a few thousand vulnerable smart contracts but yeah I mean ideally I would prefer uh that uh some some of these symbolic execution would happen on the developer site at least you know as a slightly more comprehensive way to uh to do for example fuzzing in unit testing which is like in-house quality assurance cool thanks uh any more questions by the way I think it's the one of the most smooth live demo I've ever seen like it's 100 perfect oh thank you thanks any more questions yes uh okay yeah go uh so you said it's more resource intensive I mean now on this simple example it was very fast I assume that it's like I don't know exponentially more resource intensive but what's the what is like the the input variable that makes it is it the size of the contract that you're testing is it the number of variable like uh how how can I decide what what would be a realistic scenario to use uh symbolic execution over I don't know something like fuzzing or normal unit test uh thank you so much for this question I really wanted to to talk about that um so yes unfortunately um you're right it as this more the size of the smart contract grows as we try to consider for example more users interacting with the smart contract um the number of states we have to analyze increases exponentially that's the state state explosion problem uh what makes it complicated so we have this in the previous slide I think I had it linked to the to the post we evaluated on a bit more realistic source code you can try it out yourself on some of the uh well some of the smart contracts to see if it works what makes it complicated is basically a few things so the size of the smart contract itself um the type of variables I guess matters more than just the number of variables because hashing is challenging so the main the main bottleneck with symbolic execution is traditionally associated with this possessing dissolvers so SMG solver struggle with uh they are very sophisticated basis of software they contain like Decades of optimizations but still they struggle with with particular Primitives such as for example hashing so hashing is challenging first into solvers and of course uh evm like storage layout relies on hashan so you have to either over approximate that or well you have to implement some strategies that help you deal with that um so you know reasoning about uh large bit factors is also hard and solidity also I guess a lot of solidity smart contracts use unsight integers of 236 bits which are relatively large so that's that also makes it a bit complicated um the number of you know conditional statements you have to analyze so basically anything that makes the the formulas were sent into essential solvers bigger um you know it involves some overhead and plus just some you know some particular Primitives that are used in evm of course that's a very simple example that I just chose for the purpose of this talk you can do more uh more realistic things but I mean at the current stage there is a chance that you'll probably run into some scalability issues uh but you know a lot of very smart people are working on that so I mean hopefully we'll probably get some symbolic execution tool that works very fast sometime soon one more question thank you um can you also uh like search over for a different like environment variables like the block hash or the timestamp or is it only functional arguments that can be uh you can do pretty much anything I mean that you can treat these environmental variables in any way you want basically I think ubmc probably assumes that like block timestamp and block number are symbolic or you can do this you can do this yourself so there is nothing stopping you from doing that but that's just some additional thing you have to reason about so that potentially might also induce some overhead on the analysis but yeah that's definitely doable and I think that's actually been done basically some of the tools okay I think we can take the last question if there's anyone interested I'll give you five seconds all right thank you Felina thank you so much [Applause]