Latest news about Bitcoin and all cryptocurrencies. Your daily crypto news habit.
In this series I explain how to use 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 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 Classic. 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 Classic 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“).
This type of analysis has a couple of advantages:
- Vulnerabilities are reliably detected irrespective of their cause(s) (which could, for example, involve uninitialized state variables, integer overflows or exposed initialization functions) provided they are reachable within n transactions.
- We can compute the input transactions required to reach the vulnerable states detected. This is useful not only to to determine the root cause of an issue, but also for auto-creating exploit transactions should one be so inclined.
Basic Usage
With that out of the way, let’s try Mythril Classic on a smart contract exploitation challenge from CaptureTheEther. TokenSale is a simple smart contract that allows users to buy and sell tokens for the 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 fornumTokensresults 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 some large value for numTokens. In reality, the attacker would pass 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 Classic 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” in it that allows anyone knowing the secret password to take it over (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 Classic 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 Suicide 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)s
--------------------
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 Classic’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.
Up Next
Part 2 is probably coming soon. Join our growing Discord community to stay up-to-date, get support and discuss things related to Ethereum security.
Practical Smart Contract Security Analysis and Exploitation— Part 1 was originally published in Hacker Noon on Medium, where people are continuing the conversation by highlighting and responding to this story.
Disclaimer
The views and opinions expressed in this article are solely those of the authors and do not reflect the views of Bitcoin Insider. Every investment and trading move involves risk - this is especially true for cryptocurrencies given their volatility. We strongly advise our readers to conduct their own research when making a decision.