Verifying smart contract security with Remix and MythX

By Bernhard Mueller | Tuesday, January 14th, 2020

Leveraging security tools for verification can help you increase confidence in the correctness of smart contract code. Examples are given here using the MythX plugin for Remix.

MythX logo on an airplane

Whether you are a smart contract developer or auditor you might wonder if there’s any value in using an automatic smart contract analysis tool. Assuming you know what you’re doing, will these tools tell you anything you don’t already know?

In this article I’ll describe how you can leverage security tools to increase confidence in the correctness of smart contract code and potentially detect issues that are not easily apparent.

Getting ready for takeoff

The first thing to keep in mind is that smart contracts are immutable once deployed to the blockchain (that’s the whole point). If a bug makes it into production, it’s “game over”, potentially resulting in vast financial losses.

Therefore, smart contract development should be approached with same care as developing and testing flight control systems:

  • Use a minimalist approach;
  • Use proven components whenever possible;
  • Be very specific about how the code is supposed to behave.

Smart contracts (if done right) are relatively small programs and many traditional program analysis techniques can be applied without running into path explosion issues typically encountered with more complex programs. Analysis techniques such as symbolic execution, SMT solving and input fuzzing can provide a high degree of confidence that the code behaves correctly no matter what.

MythX is a security testing service that applies static and dynamic methods analysis to search for generic bugs and verify assumptions about Solidity code. It does this by integrating static code analysis, symbolic analysis and a grey-box fuzzing into a unified API. When developing, testing, or auditing smart contracts, MythX helps you do the following things:

  • Get a quick overview of best practice violations and potential bugs in large codebases;
  • Verify assumptions about code that is hard to understand;
  • Gain confidence that the code behaves correctly with respect to functional specifications (with MythX you can prove correctness of some properties and achieve high certainty on others).

Running a basic scan

Remix comes with a built-in MythX security verification plugin which requires a couple of steps to set up. Once you have set up the MythX plugin you can submit contracts for analysis by clicking the “Analyze” button in the MythX tab.

MythX detects many generic security issues out-of-the-box. This includes both simple best practice violations (for example, set a specific compiler version, don’t do state writes after calls to untrusted addresses, and so on) and (mis-)behaviors that are very likely to constitute a vulnerability (for example, anyone can kill the contract).

Let’s try a basic analysis by running MythX against a couple of challenges from the OpenZeppelin Ethernaut wargame. Below is the source code of Level 2, “Fallout” (I flattened the code and updated it for compatibility with solc 5). Copy/paste the code into Remix to try this yourself.

/*
 * @source: https://ethernaut.openzeppelin.com/level/0x234094aac85628444a82dae0396c680974260be7
 * @author: Alejandro Santander (OpenZeppelin)
 * Modified by B. Mueller
 */

pragma solidity ^0.5.0;

contract Ownable {
    address payable public _owner;

    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);

    /**
     * @dev Initializes the contract setting the deployer as the initial owner.
     */
    constructor () internal {
        _owner = msg.sender;
        emit OwnershipTransferred(address(0), _owner);
    }

    /**
     * @dev Returns the address of the current owner.
     */
    function owner() public view returns (address) {
        return _owner;
    }

    /**
     * @dev Throws if called by any account other than the owner.
     */
    modifier onlyOwner() {
        require(isOwner(), "Ownable: caller is not the owner");
        _;
    }

    /**
     * @dev Returns true if the caller is the current owner.
     */
    function isOwner() public view returns (bool) {
        return msg.sender == _owner;
    }
}

library SafeMath {
    /**
     * @dev Returns the addition of two unsigned integers, reverting on
     * overflow.
     *
     * Counterpart to Solidity's `+` operator.
     *
     * Requirements:
     * - Addition cannot overflow.
     */
    function add(uint256 a, uint256 b) internal pure returns (uint256) {
        uint256 c = a + b;
        require(c >= a, "SafeMath: addition overflow");

        return c;
    }

    /**
     * @dev Returns the subtraction of two unsigned integers, reverting on
     * overflow (when the result is negative).
     *
     * Counterpart to Solidity's `-` operator.
     *
     * Requirements:
     * - Subtraction cannot overflow.
     */
    function sub(uint256 a, uint256 b) internal pure returns (uint256) {
        require(b <= a, "SafeMath: subtraction overflow");
        uint256 c = a - b;

        return c;
    }

    /**
     * @dev Returns the multiplication of two unsigned integers, reverting on
     * overflow.
     *
     * Counterpart to Solidity's `*` operator.
     *
     * Requirements:
     * - Multiplication cannot overflow.
     */
    function mul(uint256 a, uint256 b) internal pure returns (uint256) {
        // Gas optimization: this is cheaper than requiring 'a' not being zero, but the
        // benefit is lost if 'b' is also tested.
        // See: https://github.com/OpenZeppelin/openzeppelin-solidity/pull/522
        if (a == 0) {
            return 0;
        }

        uint256 c = a * b;
        require(c / a == b, "SafeMath: multiplication overflow");

        return c;
    }

    /**
     * @dev Returns the integer division of two unsigned integers. Reverts on
     * division by zero. The result is rounded towards zero.
     *
     * Counterpart to Solidity's `/` operator. Note: this function uses a
     * `revert` opcode (which leaves remaining gas untouched) while Solidity
     * uses an invalid opcode to revert (consuming all remaining gas).
     *
     * Requirements:
     * - The divisor cannot be zero.
     */
    function div(uint256 a, uint256 b) internal pure returns (uint256) {
        // Solidity only automatically asserts when dividing by 0
        require(b > 0, "SafeMath: division by zero");
        uint256 c = a / b;
        // assert(a == b * c + a % b); // There is no case in which this doesn't hold

        return c;
    }

    /**
     * @dev Returns the remainder of dividing two unsigned integers. (unsigned integer modulo),
     * Reverts when dividing by zero.
     *
     * Counterpart to Solidity's `%` operator. This function uses a `revert`
     * opcode (which leaves remaining gas untouched) while Solidity uses an
     * invalid opcode to revert (consuming all remaining gas).
     *
     * Requirements:
     * - The divisor cannot be zero.
     */
    function mod(uint256 a, uint256 b) internal pure returns (uint256) {
        require(b != 0, "SafeMath: modulo by zero");
        return a % b;
    }
}

contract Fallout is Ownable {
  
  using SafeMath for uint256;
  mapping (address => uint) allocations;

  /* constructor */
  function Fal1out() public payable {
    _owner = msg.sender;
    allocations[_owner] = msg.value;
  }

  function allocate() public payable { 
    allocations[msg.sender] = allocations[msg.sender].add(msg.value);
  }

  function sendAllocation(address payable allocator) public {
    require(allocations[allocator] > 0);
    allocator.transfer(allocations[allocator]);
  }

  function collectAllocations() public onlyOwner {
    msg.sender.transfer(address(this).balance);
  }

  function allocatorBalance(address allocator) public view returns (uint) {
    return allocations[allocator];
  }
}

Make sure the code complies and then hit the “Analyze” button in the MythX tab. This submits the code to the MythX service for an analysis in Quick Mode, the fastest and least comprehensive setting available in the free version of MythX.

After at most a couple of minutes the results should show up in the “Report” tab.

MythX report in Remix
MythX report in Remix

The report shows a critical issue in this contract: Anyone can become the contract owner and withdraw Ether from the account. Clicking the issue title highlights the location of the issue in the code, while clicking on the little arrow to the left expands the description.

Most importantly, this includes the list of function calls for reproducing the issue:

  1. Call Fal1out()
  2. Call collectAllocations()

This is especially useful when trying to understand issues when the root cause isn’t that obvious (or in this case for solving the challenge).

Custom tests

Besides running the built-in detectors, you can also use MythX to check specific properties. Let’s have a look at a basic example to illustrate the concept.

We’ll solve level 17 of the Ethernaut wargame. The goal of this challenge is to “unlock” a registrar smart contract by setting a Boolean state variable to true. A brief look at the code doesn’t show any obvious ways of achieving this:

pragma solidity ^0.4.23; 

// A Locked Name Registrar
contract Locked {

    bool public unlocked = false;  // registrar locked, no name updates
    
    struct NameRecord { // map hashes to addresses
        bytes32 name; // 
        address mappedAddress;
    }

    mapping(address => NameRecord) public registeredNameRecord; // records who registered names 
    mapping(bytes32 => address) public resolve; // resolves hashes to addresses
    
    function register(bytes32 _name, address _mappedAddress) public {
        // set up the new NameRecord
        NameRecord newRecord;
        newRecord.name = _name;
        newRecord.mappedAddress = _mappedAddress; 

        resolve[_name] = _mappedAddress;
        registeredNameRecord[msg.sender] = newRecord; 

        require(unlocked); // only allow registrations if contract is unlocked
    }
}

Let’s think about this challenge from the perspective of a security auditor who wants to ensure that, once deployed, the contract remains locked forever. To verify that this assumption holds, they can add an assertion to the code that checks the statement “the Boolean variable unlocked must never become true” (this type of property is called an invariant).

Copy/paste the challenge code into Remix and add the following function to the contract class:

function getSolution() public {
    assert(!unlocked);
}

MythX automatically searches for counter-examples to assertions contained in the submitted code. In our case, it uses SMT solving and fuzzing identify ways of setting the variable unlocked to true. When the MythX analysis is done you should see an assert violation listed in the report:

MythX report in Remix with an assert violation
MythX report in Remix with an assert violation

Expand the issue to find the example produced by MythX (“decoded calldata” in transaction 2). The function call is rather long – copy the line into a text editor to view it. If you reformat the output a bit you can run the example in Remix and verify that it actually sets unlocked to true:

register(0x0000000000000000000000000000000000000000000000000000000000000006,0x0000000000000000000000000000000000000000)

What’s happening here? It turns out that the function register writes to a user-supplied value to an uninitialized struct that points to storage. In that case, this results in a write to storage slot 0 which happens to contain the value we want to change.

This is a simple example but in principle you can use assertions to check arbitrarily complex properties (more on this in the next article).

Analysis modes

When you submit smart contract code to MythX the analysis engine runs fuzzing and symbolic execution in parallel with certain bounds on analysis time, loops, transaction depth, and other parameters. We offer thee modes named “quick”, “standard” and “deep”:

  • In quick mode analysis time is limited to 120 seconds. In addition to the overall timeout, the following constraints apply:
    • The fuzzer will return in less than 120 seconds if the probability of detecting further issues falls below a certain threshold (coverage-based early termination).
    • Symbolic execution terminates early if all states within a depth of two transactions have been explored.
  • In standard and deep mode each tool runs for a full 15 and 45 minutes, respectively. This allows the tools to explore achieve higher path coverage and lowers the residual risk of false negatives.

TL;DR

In this article I showed how to run a basic scan with MythX for Remix and how to check a simple custom property using a Solidity assertion. Check out the following Medium posts for more examples:

Sign up for a free MythX account today, and get started with your own basic scans.

Share this post:
Category: