Catching Weird Security Bugs in Solidity Smart Contracts with Invariant Checks

By Bernhard Mueller | Monday, April 6th, 2020

Contract invariants are properties of the program program state that are expected to always be true. In my previous article I discussed the use of Solidity assertions to check contract invariants. This article expands on the use of invariants and provides a couple of additional examples.

An interesting feature of invariant checking on the bytecode level is that it allows you to detect low-level issues, including issues caused by compiler optimisation or idiosyncrasies of the programming language, by defining high-level rules. For instance, in the last article we saw that a high-level rule “the contract should always remain unlocked” could be broken by exploiting Solidity memory addressing. Let’s look at some more examples for the effectiveness of contract invariants.

Example 1: Integer rounding

Integer divisions in Solidity round down to the nearest integer. Failure to consider the rounding behaviour can lead to bugs and vulnerabilities. Consider the example from Sigma Prime’s blog post which also has a great writeup on this bug class:

pragma solidity ^0.5.0;

contract FunWithNumbers {

    uint constant public tokensPerEth = 10;
    uint constant public weiPerEth = 1e18;

    mapping(address => uint) public balances;

    function buyTokens() public payable {
        uint tokens = msg.value/weiPerEth*tokensPerEth; // convert wei to eth, then multiply by token rate
        balances[msg.sender] += tokens;
    }

    function sellTokens(uint tokens) public {
        require(balances[msg.sender] >= tokens);
        uint eth = tokens/tokensPerEth;
        balances[msg.sender] -= tokens;
        msg.sender.transfer(eth*weiPerEth); 
    }
}

Let’s put on the auditor’s hat and come up with some meaningful properties to check. Amongst other things we could assert that, when comparing the contract account state at the beginning and end of a transaction, the following should always be true:

  1. The token balance of msg.sender increases when the contract account balance increases;
  2. The contract account balance increases when the token balance of msg.sender increases;
  3. The token balance of msg.sender decreases when the contract account balance decreases;
  4. The contract account balance decreases when the token balance of msg.sender decreases.

This could be generalised even more (e.g. the sum of all token balances increases if and only if the contract balance increases) and supplemented with additional checks (balance always increases by the right amount, …) to catch more possible bugs.

MythX supports standard Solidity assertions and the MythX AssertionFailed event which allows you to add a custom error message. One way of checking contract invariants is by creating a modifier to wrap all public and external functions. This ensures that the invariant holds at the end of all internal message calls and transactions. This approach has some limitations but let’s roll with it the meantime (support for inline specifications is coming to MythX soon™).

Typically we’ll create modifier along the following lines:

modifier checkInvariants {    

  // Save old state
  uint sender_balance_old = balances[msg.sender];    
  
  // Execute the function body
  _;

  // MythX AssertionFailed event    
   if (--- this should never occur ---) {
       emit AssertionFailed("Some error message");
    }

   // Solidity assertion    
   assert(--- this should always hold ---);
}

We’ll add the checks by creating a wrapper contract and overriding the public functions in FunWithNumbers:

contract VerifyFunWithNumbers is FunWithNumbers {

uint contract_balance_old;

constructor() public {
contract_balance_old = address(this).balance;
}

event AssertionFailed(string message);

modifier checkInvariants {
uint sender_balance_old = balances[msg.sender];

_;

if (address(this).balance > contract_balance_old && balances[msg.sender] <= sender_balance_old) {
emit AssertionFailed("Invariant violation: Sender token balance must increase when contract account balance increases");
}
if (balances[msg.sender] > sender_balance_old && contract_balance_old >= address(this).balance) {
emit AssertionFailed("Invariant violation: Contract account balance must increase when sender token balance increases");
}
if (address(this).balance < contract_balance_old && balances[msg.sender] >= sender_balance_old) {
emit AssertionFailed("Invariant violation: Sender token balance must decrease when contract account balance decreases");
}
if (balances[msg.sender] < sender_balance_old && address(this).balance >= contract_balance_old) {
emit AssertionFailed("Invariant violation: Contract account balance must decrease when sender token balance decreases");
}

contract_balance_old = address(this).balance;
}function buyTokens() public payable checkInvariants {
super.buyTokens();
}

function sellTokens(uint tokens) public checkInvariants {
super.sellTokens(tokens);
}
}

Running this contract through the MythX Remix plugin detects two invariant violations. Let’s have a closer look at the reported issues.

User buys tokens for 6 Wei. 6/10 hets rounded to zero so no tokens are added to the user’s balance.

The first counterexample produced by MythX shows a user attempting to buy tokens with a very low call value of 6 Wei. In this case, the 6 Wei get added to the contract balance but the balance of the user does not increase.

Taking another look at the code, we can see that if less than 1 Ether is sent when calling buyTokens(), the result of the division msg.value/weiPerEth will be rounded down to 0 and the subsequent multiplication with tokensPerEth will likewise return 0.

The second counterexample shows a user first buying one Ether (1000000000000000000 Wei) worth of tokens (transaction 2), then selling 6 tokens (transaction 3). This deducts 6 tokens from the user’s balance but does not transfer any Ether to the user due to the rounding error in sellTokens(uint tokens) : uint eth = tokens/tokensPerEth will be rounded down to 0 if tokens is lower than 10 or to the nearest multiple of 10 otherwise.

Example 2: Arbitrary storage writes via large-sized arrays

A couple of years ago I wrote about proving security properties using the open-source tool Mythril. By checking contract invariants with MythX you can achieve similar results. It is however important to point out the difference between the two methods:

  • The method shown previously was based on under-constrained symbolic execution of the runtime bytecode (using an older version of Mythril) whereby storage variables were initialised as symbolic variables. This method detects all instances of a bug but also returns false positives.
  • MythX combines symbolic execution and input fuzzing after partially initialising the contract account state with the concrete values. By doing this it avoids false positives but there’s a residual risk of false negatives. The risk of missing bugs declines the longer the tools are allowed to run.

With that said, let’s revisit the example shown in the old article which was based on Doug Hoyte’s classic USCC submission. This smart contract contains a hidden method of overwriting the owner state variable:

pragma solidity ^0.5.0;

contract Pwnable {
    address public owner;
    uint[] private bonusCodes;
    
    constructor() public {
        bonusCodes = new uint[](0);
        owner = msg.sender;
    }
    
    function PushBonusCode(uint c) public {
        bonusCodes.push(c);
    }
    
    function PopBonusCode() public {
        require(0 <= bonusCodes.length);
        bonusCodes.length--;
    }
    
    function UpdateBonusCodeAt(uint idx, uint c) public {
        require(idx < bonusCodes.length);
        bonusCodes[idx] = c;
    }
}

To catch improper modifications of the owner variable we can informally define the property:

  • The owner must not change in the course of the transaction unless the transaction sender matches the existing owner.

Which translates to the following Solidity assertion:

assert(owner == old_owner || msg.sender == old_owner);

Using the aforementioned method of creating a wrapper around the Pwnable contract, we get:

contract VerifyPwnable is Pwnable {   

  modifier checkInvariants {
        address old_owner = owner;       
        _;        
        assert(msg.sender == old_owner || owner == old_owner);
     }
    
     function PushBonusCode(uint c) public checkInvariants {
         super.PushBonusCode(c);
     }    

    function PopBonusCode() public checkInvariants {
        super.PopBonusCode();
    }   

    function UpdateBonusCodeAt(uint idx, uint c) public checkInvariants {
        super.UpdateBonusCodeAt(idx, c);
    }}

This time MythX detects one assert violation in the code:

Apparently there is a way to change the contract owner even though the state variable owner is not explicitly accessed anywhere in the code. This happens due to the way dynamically sized arrays are laid out in storage:

  • The length of the array uint[] bonusCodesis stored at storage slot 1;
  • Accessing array element n points to storage address keccak(1) + n.

The state variable owner lives at storage slot 0. To access it, one must first underflow the unsigned integer variable bonusCodes.length which happens in the first function call:

  • PopBonusCode()

In the second call we write to the array index that equals(MAX_UINT — keccak(1)). This will result in a write to the storage address keccak(1)+(MAX_UINT — keccak(1)) which overflows into 0:

  • UpdateBonusCodeAt(35707666377435648211887908874984608119992236509074197713628505308453184860938, 0)

Voila! The owner is now set to the zero address (to set it to any other address, convert it to an unsigned integer and pass it with the second argument). You can try this out with the Remix JavaScript VM or Ganache to verify that it works.

It’s worth pointing out that even without the assertion, MythX automatically detects the two individual flaws that make the owner overwrite possible. The first issue is the integer overflow caused by decreasing bonusCodes.length. Note that this is not possible anymore with solc 6.0 or higher which makes the array length read-only.

Additionally, MythX reports that a writes to an arbitrary storage location are possible following the length underflow:

TL;DR

By checking high-level invariants using symbolic execution and input fuzzing you can verify assumptions about how your code behaves. This can uncover unexpected bugs caused by peculiarities of the Solidity programming language, such as rounding errors, unsafe integer arithmetics and addressing of elements in storage.

By the way, all examples in this article can be reproduced using the free version of MythX. You should try it out!

Share this post:

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:

MythX Tech: Behind the Scenes of Smart Contract Security Analysis

By Bernhard Mueller | Tuesday, December 17th, 2019

The tech behind MythX smart contract analysis, including the microservices Maru, Harvey, and Mythril, and how they work together.

When I first introduced Mythril in 2017, I didn’t expect it to be very useful to smart contract developers. It was a simple symbolic analyzer for Ethereum bytecode with tacked-on Solidity support. Mythril was OK for detecting some security issues and solving CTFs, but it wasn’t written with the needs of developers in mind.

As soon as you want to use Mythril, or any other open source smart contract security tool for that matter, on an actual real-world project, things fall apart very quickly. Mythril takes ages to install and has 30+ command line flags. Running it consumes a lot of computing power. It reports only a limited subset of what’s in the SWC Registry. It doesn’t integrate well with development tools. And most frustratingly, when dealing with large projects, something always breaks. TL;DR: Mythril sucks for developers.

Yet, there seemed to be demand for a tool like Mythril and people actually started using it, building it into their own software, and posting hundreds of issues on Github. As of today, Mythril has been downloaded 470,000 times.

It was always clear to me that whatever we did, Mythril-the-Python-tool could never reach the usability and reliability required to be truly helpful to smart contract developers in their day-to-day job. Then, in early 2018, the “INFURA of smart contract security idea” lightbulb went on: What if one could submit your contracts to a simple API and get back a a security analysis report? Voilà, MythX was born (well actually, Mythril Platform was born, but that had to be renamed due to legal threats from the Tolkien troll army).

The MythX project started in early 2018 with funding from ConsenSys and two developers. Since then, the MythX team has grown to 18 heads and we have built a lot of awesome tech to pack into our security analysis engine. We also built an API that’s scalable and won’t break down even when people throw gigantic Truffle projects at it (I’m looking at you Aragon).

Our mission statement was to provide comprehensive smart contract security analysis at the click of a button.

Continue…
Share this post:
Category:

MythX Pro Security Analysis Explained

By Bernhard Mueller | Tuesday, November 19th, 2019

MythX recently went live with a new Pro upgrade that offers more powerful analysis features than the free version. In this article I’ll explain how the new “full” analysis mode affects the performance of MythX.

MythX is a smart contract security service that integrates multiple analysis techniques. The MythX Pro plan comes with a new analysis mode called Full mode. In this mode, submitted contracts are subjected to a thorough fuzzing campaign and deep inspection using symbolic analysis. It discovers complex security issues and can be used for checking the correctness of smart contracts.

Background

When you submit a smart contract to MythX, the analysis service spawns a number of workers that perform various analysis tasks in parallel. Each worker is given a maximum time budget it may spend on testing the code. The more computing time is available, the higher the coverage achieved by the analysis engine (at the cost of having to wait longer for the results).

Continue…
Share this post: