In this article I explain how to use Mythril to find and exploit security bugs in Ethereum smart contracts. The articles will cover basic principles and advanced techniques, such as testing security properties, proving invariants, analyzing multi-contract systems and auto-looting ETH from vulnerable contracts on the Ethereum network.
Mythril — also known as the “Swiss army knife of smart contract security” — has lots of bells and whistles, but to use it effectively you need a basic understanding of the analysis techniques used. This article provides an overview of the most important concepts.
The first key step we usually recommend to new users is installing Mythril. You should do this also in case you to want follow the examples in this article (if run into trouble installing, you can ask for help in our Discord support channel).
After successful installation the myth command line tool will be available on your system. Make sure you have version 0.19.7 or higher:
$ myth -V
Mythril version v0.19.7
The basic command for executing security analysis is -x / --fire-lasers:
$ myth -x <Solidity file> $ myth --rpc RPC_OPTION -xa <contract address>
This command runs a generic analysis that works reasonably well in most situations. Before we get ahead of ourselves though, let’s have a look at what is going on behind the scenes.
Multi-Transactional Symbolic Execution
Mythril checks for security issues by running a custom implementation of the Ethereum Virtual Machine. The analysis process involves the following steps:
- Obtain the contract bytecode by compiling a Solidity file or loading it from an Ethereum node;
- Initialize the contract account state either by running the creation bytecode (if source code was provided) or by retrieving data from an Ethereum node on-demand;
- Symbolically execute the code to explore all possible program states over n transactions, whereby n defaults to two but can be set to an arbitrary number;
- Whenever an undesirable states is encountered (such as “the contract kills itself”), logically prove or disprove the reachability of those states given certain assumptions (e.g. “given the right inputs anybody can kill the contract“).
When find a vulnerable state, we can compute the input transactions required to reach that state. This is useful not only to to determine the root cause of an issue, but also for crafting exploits should one be so inclined.
Basic Usage
With that out of the way, let’s try Mythril on a smart contract exploitation challenge from CaptureTheEther. TokenSale is a simple smart contract that allows users to buy and sell tokens for the once-in-a-lifetime bargain price of 1 ETH. Here is the source code:
Working with code is easier than working with on-chain contract instances because that way Mythril can show you the the code responsible for each bug it finds. Copy/paste the code into a file called tokensale.sol and run the following command:
$ myth -mether_thief -x tokensale.sol
Note the use of the -m argument which accepts a comma-separated list of analysis modules to execute. Let’s have a closer look at a particularly useful module called Ether Thief.
Looting that precious ETH
As its name subtly foreshadows, the Ether Thief module checks for transaction sequences that extract ETH from the contract. Specifically, it looks for states that fulfill the following conditions:
- A non-zero amount of ETH can be withdrawn from the contract;
- The sender withdrawing the ETH is not the contract creator;
- The amount of ETH withdrawn can be greater than the total amount previously paid into the contract by the same sender.
This is a pretty low-false-positive way of of spotting contracts that “leak” ETH to anonymous attackers. Let’s now unleash this module on the TokenSale contract:
$ myth -mether_thief -x tokensale.sol
==== Ether thief ====SWC ID: 105Type: WarningContract: TokenSaleChallengeFunction name: sell(uint256)PC address: 693
Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.
--------------------
In file: tokensale.sol:25msg.sender.transfer(numTokens * PRICE_PER_TOKEN)
--------------------
Myhril claims that to have found an issue in the withdrawal function but the root cause is not immediately apparent. If you haven’t spotted the bug yet, take another good look at the code and try to figure out the attack.
Concretizing Transactions (a.k.a. Auto-Exploit-Generator)
As you have probably deduced there’s an integer overflow issue at play here. To exploit the issue you need to pass a very specific value to the buy() function. Don’t fire up your calculator just yet though, there’s some good news: Mythril can compute the correct input transactions for you automagically. All you need to do is add the --verbose-report flag:
$ myth -mether_thief -x tokensale.sol --verbose-report
==== Ether thief ====SWC ID: 105Type: WarningContract: TokenSaleChallengeFunction name: sell(uint256)PC address: 693
Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.
--------------------
In file: tokensale.sol:25msg.sender.transfer(numTokens * PRICE_PER_TOKEN)
--------------------DEBUGGING INFORMATION:
Transaction Sequence:
Transaction Sequence: {'2': {'calldata': '0xd96a094a20', 'call_value': '0x0', 'caller': '0xaaaaaaaabbbbbbbbbcccccccddddddddeeeeeeee'},'5': {'calldata': '0xe4849b32084031', 'call_value': '0x0', 'caller': '0xaaaaaaaabbbbbbbbbcccccccddddddddeeeeeeee'}}
The DEBUGGING INFORMATION section contains the two transactions computed by Ether Thief. A look at the call_value fields shows that no ETH is transferred to the contract by the sender. Let’s have a closer look at the calldata:
The first transaction contains the first four bytes of the function signature hash of buy(uint256 num_tokens) as well as an innocent-looking extra byte — 0x20 — which represents the leftmost byte of uint256 num_tokens (the remaining zeroes don’t have to be sent explicitly as the EVM will interpret uninitialized calldata as 0x00). The value passed to num_tokens works out to:
buy(0x2000000000000000000000000000000000000000000000000000000000000000)
Let’s look at the effect this input has on the require statement on line 16:
require(msg.value == numTokens * PRICE_PER_TOKEN);
PRICE_PER_TOKEN is set to 1 Ether which corresponds to 1e18 wei. As it turns out, multiplying this amount with the value Mythril has computed for numTokens results in an integer overflow. More specifically, the result of the binary multiplication uint256(1e18) * uint256(numTokens) is zero — note that there are other input values that could be used here.
The require statement therefore passes and a large amount of tokens is credited on the sender’s account even though they’re not sending any ETH.
In transaction two, the illegitimate tokens are then sold in return for ETH (call to sell(uint256)). Because Mythril represents the contract balance symbolically it outputs a large random value for numTokens. In reality, the attacker would use a lower value corresponding to the actual number of ETH in the account.
If you haven’t done so already, now is the time to fire up Metamask and give the challenge a shot.
Configuring transaction count
An important concept to know when using Mythril is transaction count. This variable specifies the number of transactions to be executed symbolically. The default value of two is sufficient for detecting many common bugs such as the integer overflows, uninitialized storage variables and misnamed constructors. However, a search that goes two transactions deep will not discover bugs that need three or more transactions to reach.
Unfortunately, because each transaction can have multiple valid final states, the space of states to explore grows exponentially with the number of transactions. Symbolically executing three transactions therefore takes significantly longer than executing two (we’re currently working on a way of optimizing the number of transactions executed within a predefined timeframe — I’ll update this article as soon as this becomes available).
To demonstrate this let’s have a look at another example. See if you can spot the security issue (beware of spoilers in the contract name):
This contract has a “backdoor” that allows anyone knowing the secret password to become the owner (but as we know, private state variables aren’t really secret — the only difference is that the solc doesn’t generate an accessor function for them).
Another popular Mythril module is Suicide. This module checks for transactions that, if sent by anyone other than the contract creator, will “accidentally” kill the contract. Running the S_uicide_ module on the code above returns the following output:
$ myth -msuicide -x killme.sol
The analysis was completed successfully. No issues were detected.
Mythril appears to overlook the vulnerability. The reason for this is that a minimum of three transactions is needed to kill the contract: The sender must provide the correct password to activatePassword(bytes11 password), call pwnContract() to become the owner, and finally call kill() to trigger the suicide.
Let’s see what happens if we increase the number of transactions executed using the -t / --transaction-count argument:
$ myth -t3 -msuicide --verbose-report -x killme.sol
==== Unchecked SUICIDE ====SWC ID: 106Type: WarningContract: KillmeFunction name: kill()PC address: 422Estimated Gas Usage: 630 - 1055
A reachable SUICIDE instruction was detected. The remaining Ether is sent to the caller's address.
--------------------
In file: killme.sol:21
selfdestruct(msg.sender);
--------------------
DEBUGGING INFORMATION:
Transaction Sequence: {'2': {'calldata': '0xa6e0e35e63727970746f6b69747479', 'call_value': '0x0', 'caller': '0x0000000000000000000000000000000000000001'},'3': {'calldata': '0x2eb00c1b', 'call_value': '0x0', 'caller': '0x0000000000000000000000000000000000000001'},'4': {'calldata': '0x41c0e1b5', 'call_value': '0x0', 'caller': '0x0000000000000000000000000000000000000001'}}
This time the issue was detected and we get a sequence of three transactions. Inspecting the calldata more closely reveals the names and arguments of the functions being called:
TL;DR
Mythril’s Ether Thief and Suicide modules detect security bugs that allow attackers to steal from, and even kill, poor innocent smart contracts. When the --verbose-report flag is added, Mythril will output the input transaction(s) needed to trigger each bug detected. Increasing transaction count helps Mythril detect more bugs but also increases execution time exponentially.
About Mythril and MythX
Mythril is a free and open-source smart contract security analyzer. It uses symbolic execution to detect a variety of security vulnerabilities.
MythX is a cloud-based smart contract security service that seamlessly integrates into smart contract development environments and build pipelines. It bundles multiple bleeding-edge security analysis processes into an easy-to-use API that allows anyone to create purpose-built smart contract security tools. MythX is compatible with Ethereum, Tron, Vechain, Quorum, Roostock and other EVM-based platforms.