{"tags":["mythril","symbolic-execution","security","smart-contracts"],"id":"36e41e821089493b9e8997c251d68ef2_2","article_id":"36e41e821089493b9e8997c251d68ef2","article_version":2,"title":"Introduction to Mythril Classic and Symbolic Execution","content":"{\"markdown\":\" \\n[Mythril Classic](https://github.com/ConsenSys/mythril-classic)\\n is a cool symbolic execution tool that comes pre-loaded with several detection modules that check for bugs like integer overflows and reentrancy vulnerabilities. I’m one of the core team members of the MythX platform team; maintaining, improving, and buidling Mythril Classic.\\nOne of the main design goals in Mythril Classic is to make the interaction with the analysis tool simple and effortless. In other words, you don’t have to get a PhD in computer science in order to start using and benefiting from formal methods like symbolic analysis. \\n[Bernhard Mueller](https://medium.com/@muellerberndt)\\n has written \\n[several posts](https://hackernoon.com/practical-smart-contract-security-analysis-and-exploitation-part-1-6c2f2320b0c)\\n showing how you can use Mythril Classic to up your security game.\\nThis specific post aims to reveal some of the magic happening behind the scenes, later articles will go more in-depth on the detection module system of Mythril Classic, ultimately providing enough information to start rolling your own custom analysis modules.\\n\\n## Symbolic execution\\n\\nTo explain how Mythril works we will need to start with symbolic execution, the core technique used in Mythril Classic. If you are already comfortable with the general idea of symbolic execution, then this post will recap already familiar concepts.\\nI think the easiest way to explain symbolic execution is by applying it and graphically showing what happens during execution. To help with that, we’ll be using the following solidity function as a target of our analysis.\\n\\n```solidity\\nfunction execute(uint256 input) public (uint256){\\n uint memory result = 0;\\n if (input > 10) {\\n result += 10;\\n }\\n return result;\\n}\\n```\\n\\nOur goal will be to see if we can use symbolic analysis to show that it is possible to get the result of the function to be 10.\\n\\n### Concrete Example\\n\\nBefore we start with actual symbolic execution let’s first look at concrete execution. We can execute the function \\n`execute(uint256)`\\n with multiple different inputs. Take for example the input 4, which will result in the following execution trace for the function \\n`execute`\\n (I've added the memory state for each step):\\n\\n```\\nInitial state (function entry): \\n- currently executing: line 1 \\n- input = 4 \\nstep1: \\n- currently executing: line 2 \\n- input = 4 \\n- result = uninitialized \\nstep2: \\n- currently executing: line 3 \\n- input = 4 \\n- result = 0 \\nstep3: \\n- currently executing: line 6: \\n- input = 4 \\n- result = 0\\n```\\n\\n\\nAnd here is a graphical representation of the same trace:\\n\\n![](https://api.kauri.io:443/ipfs/QmYeLC1q25DRQd9KzandsuBRRyPW6nFav8Sz6Gc7nmSHbi)\\n\\nWe can keep trying different inputs until we find an input that makes the function return 10. This approach is called fuzzing, and \\n[Valentin Wüstholz](https://medium.com/@wuestholz)\\n has done \\n[an awesome writeup](https://medium.com/consensys-diligence/finding-vulnerabilities-in-smart-contracts-175c56affe2)\\n of how Harvey, a state-of-the-art fuzzer, works and is used in the MythX-platform. In this case, however, we are looking at how symbolic execution can be used to solve the problem.\\n\\n### Symbolic Example\\nFinally, we’re at the part where we’ll be executing the program symbolically. This means that instead of executing the program with the input 4 we’ll execute the program with a symbol, let's call that symbol \\n`x`\\n . The symbol \\n`x`\\n can take on any valid value that a \\n`uint256`\\n could possibly have. Now, we’ll execute the program again.\\nExecuting the first two steps is still rather straightforward:\\n\\n![](https://api.kauri.io:443/ipfs/QmanKdLDQRikZ8pjsKGTFqevnNstx1D2WBPCpEjtit1DpK)\\n\\nThis is where it gets interesting. At line 3 the input is compared to a number \\n`10`\\n , but the input is \\n`x`\\n , so it could take on any concrete value. Therefore, both options \\n`x > 10`\\n and \\n`x <= 10`\\n are possible. If this happens, we \\n_branch_\\n \\n_out_\\n and create two new states. One where \\n`x > 10`\\n must hold, and one where \\n`x <= 10`\\n must hold. We'll also keep track of these \\n_constraints_\\n in our states. We do this so we can determine what inputs would follow specific paths.\\nLet's extend the state graph with the next steps of the execution:\\n\\n![](https://api.kauri.io:443/ipfs/QmbqXxgTazypUnrnMRafPk5vC5QTJe7Gv6ctxXhKnqAsMc)\\n\\nThese are the states generated by symbolically executing the function. Given these symbolic states, we can write a simple program that tries to find an input for which the function will return 10.\\n\\n```python\\nfor state in states:\\n # Let's filter all the states that are not return statements\\n if state.currently_executing != 6:\\n continue\\n # We want the result to be 10, let's formulate that as a constraint\\n result_constraint = (state.result == 10)\\n \\n # If it is possible to satisfy both the path constraints (these are the constraints collected on each branch)\\n # and the result constraint then there must be an input that makes the function return 10\\n if is_possible(result_constraint and state.constraints):\\n # Using SMT solving we can get an input that will satisfy all the constraints and make the function return 10\\n print(give_satisfying_input(result_constraints and state.constraints))\\n```\\n\\nIf we look at the execution of this piece of code then we can clearly see that it will only consider state 3 and state 5.\\nFor the analysis of state 3, the function \\n`is_possible(result_constraint and state.constraints)`\\n will return false, because for this state \\n`result = 0`\\n .\\nLooking at state 5, we’ll see something more interesting. Let's look at the two constraints that are considered here: \\n`result == 10`\\n and \\n`x > 10`\\n . It's easy to see that the first constraint must be satisfied, because for this state \\n`result = 10`\\n . We can also easily determine that \\n`x > 10`\\n can be satisfied; take for example the input \\n`11`\\n . I just manually found a value that satisfies the constraints. In Mythril Classic itself, actually checking if it is possible to satisfy these constraints is handled by an SMT solver (Z3 in our case). It uses \\n[black magic](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)\\n and tells us if it is possible to satisfy the constraints. \\n But Z3's magic doesn't stop there. It can even give you an example that satisfies the constraints; this will allow us to construct a concrete input that will make the function return 10.\\nAs a conclusion to the analysis of the function \\n`execute`\\n , we were able to say that\\n\\n\\n\\n * It is possible that the output of the program is 10\\n\\n * To get the output of the program to be 10, you could use the input 11\\n\\n## What next?\\nIn this post, we saw how we can apply symbolic execution to a small example function and saw how to write a trivial analysis module.\\nWhile this is already cool, in further posts we’ll look at more interesting properties and bugs. For example, we can search for states where we can force the value of a send call to be 10 ether. Something you might not want your contract to allow.\\nThanks to \\n[Valentin Wüstholz](https://medium.com/@wuestholz)\\n and \\n[Dominik Muhs](https://medium.com/@dmuhs)\\n for feedback on a draft version of this article.\\n\"}","author":"dea4103810fbf9967e69eb3b10507660c92ab74b","timestamp":1554207347040,"attributes":{"origin_name":"medium","origin_url":"https://medium.com/@joran.honig/introduction-to-mythril-classic-and-symbolic-execution-ef59339f259b"}}