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. — 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. Mythril The first key step we usually recommend to new users is . 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 ). installing Mythril Discord support channel After successful installation the command line tool will be available on your system. Make sure you have version 0.19.7 or higher: myth $ 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; the code to explore all possible program states over transactions, whereby defaults to two but can be set to an arbitrary number; Symbolically execute n n 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 can kill the contract“). anybody 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 should one be so inclined. crafting exploits Basic Usage With that out of the way, let’s try Mythril on a smart contract exploitation challenge from . 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: CaptureTheEther TokenSale 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 and run the following command: tokensale.sol $ myth -mether_thief -x tokensale.sol Note the use of the argument which accepts a comma-separated list of to execute. Let’s have a closer look at a particularly useful module called . -m analysis modules Ether Thief Looting that precious ETH As its name subtly foreshadows, the module checks for transaction sequences that extract ETH from the contract. Specifically, it looks for states that fulfill the following conditions: Ether Thief A non-zero amount of ETH can be withdrawn from the contract; The sender withdrawing the ETH is the contract creator; not 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 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 flag: buy() --verbose-report $ 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 section contains the two transactions computed by . A look at the fields shows that no ETH is transferred the contract by the sender. Let’s have a closer look at the calldata: DEBUGGING INFORMATION Ether Thief call_value to The first transaction contains the first four bytes of the function signature hash of as well as an innocent-looking extra byte — — which represents the leftmost byte of (the remaining zeroes don’t have to be sent explicitly as the EVM will interpret uninitialized calldata as ). The value passed to works out to: buy(uint256 num_tokens) 0x20 uint256 num_tokens 0x00 num_tokens buy(0x2000000000000000000000000000000000000000000000000000000000000000) Let’s look at the effect this input has on the statement on line 16: require require(msg.value == numTokens * 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 results in an integer overflow. More specifically, the result of the binary multiplication is zero — note that there are other input values that could be used here. PRICE_PER_TOKEN numTokens uint256(1e18) * uint256(numTokens) The statement therefore passes and a large amount of tokens is credited on the sender’s account even though they’re not sending any ETH. require In transaction two, the illegitimate tokens are then sold in return for ETH (call to ). Because Mythril represents the contract balance symbolically it outputs a large random value for . In reality, the attacker would use a lower value corresponding to the actual number of ETH in the account. sell(uint256) numTokens If you haven’t done so already, now is the time to fire up and . Metamask give the challenge a shot Configuring transaction count An important concept to know when using Mythril is . 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 discover bugs that need three or more transactions to reach. transaction count not 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 . 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: Suicide $ 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 call to become the owner, and finally call to trigger the suicide. activatePassword(bytes11 password), pwnContract() kill() Let’s see what happens if we increase the number of transactions executed using the argument: -t / --transaction-count $ 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 and modules detect security bugs that allow attackers to steal from, and even kill, poor innocent smart contracts. When the flag is added, Mythril will output the input transaction(s) needed to trigger each bug detected. Increasing helps Mythril detect more bugs but also increases execution time exponentially. Ether Thief Suicide --verbose-report transaction count About Mythril and MythX is a free and open-source smart contract security analyzer. It uses symbolic execution to detect a variety of security vulnerabilities. Mythril 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. MythX
