Mythril 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.
One of the main design goals in Mythril 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. Bernhard Mueller has written several posts showing how you can use Mythril to up your security game.
This 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, ultimately providing enough information to start rolling your own custom analysis modules.
To explain how Mythril works we will need to start with symbolic execution, the core technique used in Mythril. If you are already comfortable with the general idea of symbolic execution, then this post will recap already familiar concepts.
I 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.
Our 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.
Before we start with actual symbolic execution let’s first look at concrete execution. We can execute the function
execute(uint256) with multiple different inputs. Take for example the input 4, which will result in the following execution trace for the function
execute (I've added the memory state for each step):
Initial state (function entry):
- currently executing: line 1
- input = 4
- currently executing: line 2
- input = 4
- result = uninitialized
- currently executing: line 3
- input = 4
- result = 0
- currently executing: line 6:
- input = 4
- result = 0
And here is a graphical representation of the same trace:
We can keep trying different inputs until we find an input that makes the function return 10. This approach is called fuzzing, and Valentin Wüstholz has done an awesome writeup 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.
Finally, 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
x. The symbol
x can take on any valid value that a
uint256 could possibly have. Now, we’ll execute the program again.
Executing the first two steps is still rather straightforward:
This is where it gets interesting. At line 3 the input is compared to a number
10, but the input is
x, so it could take on any concrete value. Therefore, both options
x > 10 and
x <= 10 are possible. If this happens, we branch out and create two new states. One where
x > 10 must hold, and one where
x <= 10 must hold. We'll also keep track of these constraints in our states. We do this so we can determine what inputs would follow specific paths.
Let's extend the state graph with the next steps of the execution:
These 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.
If 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.
For the analysis of state 3, the function
is_possible(result_constraint and state.constraints) will return false, because for this state
result = 0.
Looking at state 5, we’ll see something more interesting. Let's look at the two constraints that are considered here:
result == 10 and
x > 10. It's easy to see that the first constraint must be satisfied, because for this state
result = 10. We can also easily determine that
x > 10 can be satisfied; take for example the input
11. I just manually found a value that satisfies the constraints. In Mythril itself, actually checking if it is possible to satisfy these constraints is handled by an SMT solver (Z3 in our case). It uses black magic and tells us if it is possible to satisfy the constraints.
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.
As a conclusion to the analysis of the function
execute, we were able to say that
- It is possible that the output of the program is 10
- To get the output of the program to be 10, you could use the input 11
In this post, we saw how we can apply symbolic execution to a small example function and saw how to write a trivial analysis module.
While 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.