Detecting Ownership Takeovers Using Mythril

September 22, 2020 by Joran Honig

Mythril is an analysis tool which uses symbolic execution to find vulnerabilities in smart contracts. Mythril even generates exploits for the vulnerabilities that it finds 🚀. In a previous article, I wrote about Mythril internals and symbolic execution. In this article, I’ll show how I use Mythril to detect Ownership takeover vulnerabilities. I’ll also use Mythril’s new plugin system install and release plugins with ease!

Introduction

Out of the box, Mythril comes with several zero-setup detection modules. These pre-built detection modules look for weaknesses and vulnerabilities. For example, our ether thief module simulates how an attacker might steal ether from a contract.

Awesome, right?

However, ether is not the only thing that holds value on the blockchain. There are a variety of different tokens and smart contracts, and they all work slightly different. Some vulnerabilities are particular to the business logic of a smart contract, which makes it difficult to find using generic detectors. Fortunately, we can build custom detection modules to look for these non-generic vulnerabilities!

In this article, I’m going to have a look at the smart contract ownership pattern. Check out this knowledge base article from OpenZeppelin. This page describes access control and the ownership pattern. As you can imagine, ownership will likely be used to protect sensitive functionality. So we want to be sure that nobody can just take over ownership.

Luckily we can use Mythril to find whether an attacker can take over ownership!

To do so, we’ll follow the following steps:

🚧 First, I’ll set up the scaffolding for a plugin project.
☕ Then we take a look at ownership, determine what Mythril should look for, and encode it in SMT constraints.
🚀 Finally, we set up setup.py to install our plugin and enable it within Mythril.

💡 Let us know if you end up building a nice detector after reading this article; we’d love to include it in Mythril to #MakeEthereumSafer.

Setting up a Mythril Plugin Project

Before we get started with building our detection module, we’ll first need to set up our plugin project & dependencies.

Installation

You will want to have a few packages installed to build a Mythril plugin.

The first dependency is python3 (preferably >=3.6), which you can install using your favourite package manager.

In this article, we’ll also be using virtualenv to install all further python dependencies in isolation.

# You can use the following command to install virtualenv:
python -m pip install --user virtualenv

Laying down the groundwork

Now that our environment is set up, we can get started with our Mythril plugin project!

The following commands will set up the base file structure for a Mythril plugin:

# Create a directory for the project
mkdir ownable_detector

# The following two commands set up a python virtual environment
virtualenv ./venv
source ./venv/bin/activate

# Set up the project files
mkdir myth_ownable_detector
touch setup.py
touch requirements.txt
touch myth_ownable_detector/__init__.py
touch myth_ownable_detector/detector.py

After running these commands, you should end up with the following directory structure:

ownable_detector/
- setup.py :: we’ll use this to handle the installation of the plugin
- requirements.txt :: contains plugin dependencies
- myth_ownable_detector/
  - __init__.py :: the entry point of the plugin package
  - detector.py :: the container for the detector
- venv/* :: all the virtual environment files

Installing necessary python packages

Our detection module will be using a single package: mythril; this is what we’re building our plugin for 😃. We’ll write this into the requirements.txt file:

mythril

Now, you can use the following command to install the dependencies written in requirements.txt (there is only one for this example plugin):

pip install -r requirements.txt

Set Up Complete

👍The set up is all done! Now we can get started with our detection module.

Writing the Detection Module

As we know, it is common for smart contracts to implement some form of access control, such as ownership (Check out: access control).

Smart contracts with ownership will frequently have a state variable public address owner which holds the address of the owner/administrator of the smart contract. Contracts with an owner will usually have an onlyOwner modifier, which protects sensitive functions by verifying that the sender of a transaction is the owner.

You can imagine that it wouldn’t be good if anyone could take over ownership of a contract. Let’s write a plugin for Mythril that finds whether an attacker can take over ownership.

Check out this repo to follow along with the plugin implementation: https://github.com/ConsenSys/mythril-example-plugin/blob/master/example_detector/ It contains the finished plugin, as well as a simple vulnerable contract ownable_example.sol.

Detection

Before we get started, we need to figure some things out. First, we should determine what it is that our detector should be checking. Second, Mythril works on the EVM bytecode, so we need to figure out how ownership works on the EVM level.

What should Mythril look for? The owner of the contract has a lot of power, so we want to know if an attacker can potentially take over ownership. More formally, Mythril should be on the lookout for:

Situations where an attacker can change the owner of a contract to themselves.

Diving into the EVM

There are two principal variables for ownership takeovers: msg.sender: the sender of a transaction owner: the owner variable

The EVM keeps track of the msg.sender in its Execution Environment. The yellow paper explains that this variable tracks: the sender address of the transaction that originated this execution. In Mythril, we can locate the sender for a global state as follows: global_state.environment.sender.

owner is a solidity storage variable, which means that it will be somewhere in the storage of the contract. We can use solc to figure out where in storage the compiler puts this variable (check out the official Solidity docs here: https://solidity.readthedocs.io/en/v0.6.8/internals/layout_in_storage.html#json-output).

💡 The owner variable might be at a different location in storage depending on the contract.

I ran the following command to find where Solidity allocates the owner variable for ownable_example.sol:

$ solc --combined-json storage-layout ownable_example.sol
...
"label": "owner",
"offset":0,
"slot": 0,
"numberOfBytes": 20,
...

This output tells us that solc put owner at offset 0 in storage slot 0, and that it uses 20 bytes. Nice!

Writing a detector

Above, we’ve looked at what our detection module should check & what the relevant variables look like on the EVM level. With this information, we can formulate a detection rule:

If an attacker can change the first twenty bytes of storage slot 0 from someone else’s address to their address, then there is a vulnerability.

Mythril uses symbolic execution to explore all possible executions of a smart contract, and this rule describes what Mythril should be searching for. In writing a detection module, we extend Mythril to check for circumstances where our detection rule applies. To achieve this detection modules introduce hooks into Mythril’s exploration engine so that Mythril executes the plugin at relevant points during the execution. For example, we’ll want to introduce a hook at all SSTORE operations, as these operations can modify the owner variable. On each hook, a detection module will check whether the smart contract is vulnerable using constraints and the SMT-solver.

The constraints are a conditional expression indicating if there is a vulnerability, and the SMT-solver allows us to see whether the constraints are satisfiable (i.e. if they are possible).

In our case, the constraints (i.e. the conditions which imply a vulnerability) follow from the formalized detection rule: If an attacker can change the first twenty bytes of storage slot 0 from someone else's address to their address, then there is a vulnerability.

Concretely, there is a vulnerability, whenever Mythril encounters a transaction where:

An attacker is sending the transaction.
There is a value written owner (the first 20 bytes of storage address 0).
The value written to owner is the attacker’s address (i.e. the first 20 bytes of the value written must be equal to the attacker’s address).
The value of owner must not have been the attacker before (i.e. the first 20 bytes of storage at address 0 is not equal to the address of the attacker before the write).

The following snippet shows how we describe these conditions using python:

# In the following array we'll describe all the conditions that need to hold for a take over of ownership
vulnerable_conditions = [
 # Lets check that we're writing to address 0 (where the owner variable is located
 address == target_slot,
 # There is only a vulnerability if before the writing to the owner variable: owner != attacker
 Extract(
     20*8 + target_offset,
     0 + target_offset,
     state.environment.active_account.storage[symbol_factory.BitVecVal(0, 256)]
 ) != ACTORS.attacker,

 # There IS a vulnerability if the value being written to owner is the attacker address
 Extract(
     20*8 + target_offset,
     0 + target_offset,
 ) == ACTORS.attacker,
 # Lets only look for cases where the attacker makes themselves the owner by saying that the attacker
 # is the sender of this transaction
 state.environment.sender == ACTORS.attacker,
]

The Weeds

Now we have everything to start writing our plugin in detector.py.

💡 For the full plugin implementation, check out: https://github.com/ConsenSys/mythril-example-plugin/blob/master/example_detector/myth_example_detector/detector.py.

In detector.py, we create a new class OwnershipDetector which inherits from DetectionModule. We’ll also add hooks into Mythril’s symbolic execution by setting the class variable pre_hooks= ["SSTORE"]. This hook will make Mythril execute the detector’s function _execute(global_state) whenever it encounters a state that executes a SSTORE operation.

On each hook we’ll perform three steps:

Construct vulnerability_conditions.
Check if vulnerability_conditions can be satisfied.
Report an Issue if the vulnerability_conditions can be satisfied.

🤖 Check out https://github.com/ConsenSys/mythril-example-plugin/blob/master/example_detector/myth_example_detector/detector.py#L55 to see how I implemented these steps.

Registering the Plugin

To make the detector a full-fledged plugin we’ll need to make some additions: Make the detector expose the MythrilPlugin interface Add a setup.py which can install and register our plugin with Mythril (optionally) Install the plugin using python setup.py install.

MythrilPlugin interface

Step 1 is easy. First, we make the detector OwnershipDetector inherit from MythrilPlugin. Then we add some fields with meta-information on the plugin (for example the author, license and version of the plugin).

class OwnershipDetector(DetectionModule, MythrilPlugin):
 """This module checks for ownership vulnerabilities"""
 # The following fields add some metadata to the plugin
 author = "Joran Honig"
 plugin_license = "MIT"
 plugin_type = "Detection Module"
 plugin_version = "0.0.1 "
 plugin_description = \
   "This is an example detection module plugin which finds ownership takeover vulnerabilities.\n" \
   "This is largely copy of the reachable exceptions module already present in Mythril."
   default_enabled = True

Installation and Plugin Registration

For step 2 we’ll need to add some contents to setup.py to detail how our python package should be installed (check out the docs for more info). The following is the setup.py that I will be using for this module:

import setuptools

with open("README.md", "r") as fh:
    long_description = fh.read()

setuptools.setup(
    name="myth_ownable_detector",
    version="0.0.1",
    author="Joran Honig",
    author_email="[email protected]",
    description="An example mythril plugin",
    long_description=long_description,
    long_description_content_type="text/markdown",
    url="https://github.com/ConsenSys/mythril-ownable-detector",
    packages=[
        "myth_ownable_detector"
    ],
    classifiers=[
        "Programming Language :: Python :: 3",
        "License :: OSI Approved :: MIT License",
        "Operating System :: OS Independent",
    ],
    # ===========================================
    # The entry_points field is used to register the plugin with mythril
    #
    # Right now we register only one plugin for the "mythril.plugins" entry point,
    # note that you can add multiple plugins.
    # ===========================================
    entry_points={
        "mythril.plugins": [
            "myth_example_detector = myth_ownable_detector:OwnableDetector",
        ],
    },
    python_requires='>=3.6',
)

At the very end, you can see I used the entry_points parameter; this is used by Mythril to find python packages that expose a Mythril plugin.

When developing new Mythril plugins, you can change mythx_example_detector = myth_ownable_detector:OwnableDetector to point to your own plugin.

tldr;

In this article, we took a look at:

Mythril detection module design.
How to make Mythril discover ownership takeover vulnerabilities.
How to create a setup.py to install custom detection plugins.

Fin

Thanks for reading through this article; I hope you enjoyed it!

We ❤️ Smart Contract Security, and we’d want to hear if you built a detection module! Reach out to us on twitter at @mythx_platform.

Thinking about smart contract security? We can provide training, ongoing advice, and smart contract auditing. Contact us.

All posts