Advanced smart contract security verification in Remix

The Remix development environment provides users with a convenient and powerful way of checking the correctness of smart contracts via the MythX plugin. In this article, I’ll explain the basics and provide several examples including security tests of real-world smart contracts.

Smart contracts are immutable (or at least supposedly so) and ensuring program correctness before deploying a contract to the mainnet is absolutely essential. Security audits and a comprehensive test suite help ensure that the code is bug-free. When it comes to automated testing, writing comprehensive unit tests is a great start, but such tests don’t ensure that the code behaves correctly under all circumstances. This is where program analysis techniques such as symbolic analysis and input fuzzing can provide additional confidence.

Using the “MythX” tab in Remix you can check assertions in your code using grey-box fuzzing and symbolic analysis. In other words, the MythX security analyzer fires on all cylinders to break your assumptions about the code and alert you about unexpected bugs.

Let’s start with a basic example to illustrate how this works. By adding an assertion to the code you assert that some expression always evaluates to “true” when that particular program location is reached. Consider the following code:

pragma solidity ^0.5.0;
contract Primality {
    
    uint256 public largePrime = 973013;
    
    uint256 x;
    uint256 y;
    
    function setX(uint256 _x) external {
        x = _x;
    }
 
    function setY(uint256 _y) external {
        y = _y;
    }
    
    function checkSomething() external view {
        require(x > 1 && x < largePrime);
        require(y > 1 && y < largePrime);
        assert(x*y != largePrime);
    }
}

In checkSomething() we assert that uint256 largePrime is prime (i.e. it can only be divided by 1 and itself). We express this as:

• There exists no pair of numbers x, y that are greater than 1 and lower than largePrime and whose product matches the value of largePrime.

MythX can be used to check whether the above assertion is correct. It does so using two approaches: It tries many possible inputs to determine if the exception can be triggered (fuzzing) and checks if execution paths that reach the failure state are feasible using an SMT solver (symbolic analysis).

Fire up the MythX tab in Remix, copy/paste the above code into a new file and click the “analyze” button. After a couple of minutes the result should show up in the “Report” tab including an issue titled “assert violation”.

You can highlight the affected line of code by clicking on the issue title. Clicking on the arrow left to the title shows a more detailed description and, most importantly, the example found by MythX that violates our assertion.

In this case, a sequence of function calls is displayed that triggers an assert violation in line 21:

1. Contract creation
2. setY(953)
3. setX(1021)
4. checkSomething()

To verify that the example provided by MythX is correct you can deploy the contract to the JavaScript VM and execute the function calls in the same order which should trigger an exception.

You don’t need to know exactly how MythX works in order to use it but there are a few facts about the analysis service that are important to know:

• Starting with the initial state set by the constructor, MythX explores sequences of transactions (call function setY() followed by function setX() and so forth).
• In the above example MythX factorised a number. This won’t work for very large numbers. The compute available for solving complex math and logic problems depends on which analysis mode is used.
• MythX produces up to two examples for each assertion violation it detects but additional cases might exist, so you should always re-run MythX after applying a fix.

Writing correctness checks

Assert statements can be used to discover subtle vulnerabilities. A great way to try this out is by cheating on smart contract wargames. Most Solidity hacking challenges define a specific goal the player needs to reach. If you copy/paste the code into MythX and assert the negation of the goal this will motivate MythX to find the solution to the challenge.

To demonstrate this we’ll solve level 17 of the Ethernaut wargame using MythX. 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 (unless you’re somewhat experienced in auditing Solidity code).

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
    }
}

Think about this challenge from the perspective of a security auditor who wants to ensure that, once deployed, the contract remains locked forever. The auditor could assert the following:

• The value of the boolean variable “unlocked” must always be false.

We can check this easily by adding a new function to the contract which asserts unlocked == false. Copy the challenge code into Remix and add the following function to the contract class:

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

Run a quick MythX analysis. When the analysis is done you should see an issue titled “assertion violation” listed in the report tab. Expand the issue to find the example produced by MythX (“decoded calldata” in transaction 2).

The function arguments are rather long and will get cut off at the right. Copy the whole line into a text editor to view it. With some reformatting of the output you can run the example in Remix and verify that unlocked is indeed set totrue:

register(0x0000000000000000000000000000000000000000000000000000000000000006,0x0000000000000000000000000000000000000000)

Why does this work? It turns out that the function register writes a user-supplied value to an uninitialized struct that points to storage. This results in a write to storage slot 0 which happens to contain the boolean value we want to change (replay this in the Remix JavaScript VM to verify the solution).

It’s important to note that assert violations may have various root causes, including integer overflows and underflows, write to unexpected memory locations, forgotten modifiers, and many more. As long as there is some way to break the assertion MythX will likely find it and display the steps it took to get there.

Function preconditions and postconditions

The previous example showed assertion that checked a particular type of property known as a contract invariant (more on this below). Besides checking the validity of global invariants, it is often desirable to check the behavior of a specific function in which case function preconditions and postconditions are used.

During a recent security audit of the 0x smart contracts with ConsenSys Diligence we tested a library that implemented arithmetic operations on fixed-point signed integers. Amongst other things, we wanted to ensure that the arithmetic functions were safe from overflows und underflows.

Here is the original version of the_add() function which takes two signed integers arguments and returns the sum, supposedly reverting on overflow.

contract FixedMath {
/// @dev Adds two numbers, reverting on overflow.
    function _add(int256 a, int256 b) public pure returns (int256 c) {
        c = a + b;
        if (c > 0 && a < 0 && b < 0) {
            revert();
        }
        if (c < 0 && a > 0 && b > 0) {
            revert();
        }
    }    
}

It’s a little difficult to see whether this function actually catches all possible overflows and underflows so this is a good candidate for “cheating” with MythX. We can define the following two properties:

• The sum a ≥ 0, b >0 must always be a positive number;
• The sum of a≤ 0, b < 0 must always be a negative number.

In order not to touch the original contract we create a wrapper contract that inherits from our FixedMath and override the target function to insert checks. The above properties are translated into assertions as follows:

contract VerifyFixedMath is FixedMath {
    // The sum of two positive numbers or zero and a positive number must be a positive number
    function EnsureAddNoOverflow(int256 a, int256 b) public pure returns (int256) {
   
        // Preconditions
        require(a >= 0);
        require(b > 0);
        // Postcondition
        assert(_add(a, b) > 0);
    }
    // The sum of two negative numbers or zero and a negative number must be a negative number
    function EnsureAddNoUnderflow(int256 a, int256 b) public pure returns (int256) {
        // Preconditions
        require(a <= 0);
        require(b < 0);
        // Postcondition
        assert(_add(a, b) < 0);
    }
}

Running a quick MythX check uncovers one case of integer underflow:

Again, to view the function arguments copy the decoded calldata from the MythX tab into a text editor. You should get the following:

EnsureAddNoUnderflow(-57896044618658097711785492504343953926634992332820282019728792003956564819968, -57896044618658097711785492504343953926634992332820282019728792003956564819968)

As it turns out, summing the smallest negative number with itself results in an underflow and the result is zero (the issue was fixed in the course of the audit).

Contract invariants

An contract (or global) invariant is an assertion that should always hold. For example, you might want to ensure that:

• The value of the “owner” state variable never changes;
• The total token supply is constant (in a non-mintable token);
• The sum of all balances of an ERC20 token always matches the total supply.

Checks on simple invariants can unearth quite interesting and counter-intuitive bugs. An article by Vera Bogdanich Espina of OpenZeppelin contains a great example. The article discusses how a critical vulnerability in the MakerDAO contract (also discovered by OpenZeppelin) could have been caught by an automated verifier.

The bug itself is not trivial and I recommend reading OpenZeppelin’s detailed writeup if you want to fully understand what’s going on. In short, the vulnerability allows an attacker to remove votes from proposals of their choice and indefinitely lock other users’ MKR tokens. In her blog post, Vera provides a simplified version of the vulnerable contract:

contract SimpleDSChief {
    mapping(bytes32=>address) public slates;
    mapping(address=>bytes32) public votes;
    mapping(address=>uint256) public approvals;
    mapping(address=>uint256) public deposits;
function lock(uint wad) public {
        deposits[msg.sender] = add(deposits[msg.sender], wad);
        addWeight(wad, votes[msg.sender]);
    }
function free(uint wad) public {
        deposits[msg.sender] = sub(deposits[msg.sender], wad);
        subWeight(wad, votes[msg.sender]);
    }
function voteYays(address yay) public returns (bytes32){
        bytes32 slate = etch(yay);
        voteSlate(slate);
        return slate;
    }
function etch(address yay) public returns (bytes32 slate) {
        bytes32 hash = keccak256(abi.encodePacked(yay));
        slates[hash] = yay;
        return hash;
    }
    
    function voteSlate(bytes32 slate) public {
        uint weight = deposits[msg.sender];
        subWeight(weight, votes[msg.sender]);
        votes[msg.sender] = slate;
        addWeight(weight, votes[msg.sender]);
    }
function addWeight(uint weight, bytes32 slate) internal {
        address yay = slates[slate];
        approvals[yay] = add(approvals[yay], weight);
    }
function subWeight(uint weight, bytes32 slate) internal {
        address yay = slates[slate];
        approvals[yay] = sub(approvals[yay], weight);
    }
function add(uint x, uint y) internal pure returns (uint z) {
        require((z = x + y) >= x);
    }
function sub(uint x, uint y) internal pure returns (uint z) {
        require((z = x - y) <= x);
    }
}

The question we want MythX to answer here is whether the contract always ensures that a user’s votes are counted. To this end we define a global invariant as suggested by Vera:

• The total approval weight of the option voted for by a user must be at least equal to the deposit of that user.

Again we create a wrapper contract and put the assertion into a modifier which is then applied to all public functions. This way we ensure that the invariant always holds on non-reverting state transitions.

contract VerifySimpleDSChief is SimpleDSChief {
modifier checkInvariants {
        _;
        bytes32 senderSlate = votes[msg.sender];
        address option = slates[senderSlate];
        uint256 senderDeposit = deposits[msg.sender];
         
        assert(approvals[option] >= senderDeposit);
    }
    
    function lockForActor(address addr, uint amount) internal {
        deposits[addr] = amount;
        addWeight(amount, votes[addr]);
    }
    
    constructor() public checkInvariants {
        
        // set up the initial state with some deposits
        
        lockForActor(msg.sender, 1);
        lockForActor(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF, 1);
        lockForActor(0xaAaAaAaaAaAaAaaAaAAAAAAAAaaaAaAaAaaAaaAa, 1);
    }
function voteYays(address yay) public checkInvariants returns (bytes32) {
        return super.voteYays(yay);
    }
function etch(address yay) public checkInvariants returns (bytes32 slate) {
        return super.etch(yay);
    }
    
    function voteSlate(bytes32 slate) public checkInvariants {
        super.voteSlate(slate);
    }
    
    function lock(uint wad) public checkInvariants {
        super.lock(wad);
    }
    
    function free(uint wad) public checkInvariants {
        super.free(wad);
    }
}

This time, if we check this with MythX we’ll run into the limitations of the “quick” analysis preset: When you check contract invariants there will always be a residual risk of false negatives because both the fuzzer and symbolic analyser models some storage variables as concrete values and only a bounded numbers of transactions can be explored. In “quick” analysis mode the tools have a time budget of 120 seconds which is insufficient for exploring long transaction sequences. More compute time means “deeper” analysis and smaller residual risk (shameless plug: that’s why auditors and security-aware developers should sign up for our awesome subscription plans 😀).

Processing a “full” analysis takes around 30 minutes. When you request a full analysis from Remix, you will get a link to the MythX dashboard where you can track the progress of the analysis and view the results. In the case of SimpleDSChief the analysis discovers one possible counter-example to our invariant:

Essentially, the example shows a user voiding their own voting weight.

1. The user calls voteSlate(bytes32), voting for yet a slate that hasn't been etched (i.e. slates[hash] holds the the zero address);
2. The slate voted for in the previous call is now etched by calling etch(addr) where keccak256(addr) equals the hash passed in the previous call;
3. slates[votes[msg.sender]] now points to a different (non-zero) address. approvals[slates[votes[msg.sender]]] == 0 which results in the failure of the assertion.

The key observation here is that checking a simple invariant (“a user’s vote must always be counted”) exposed a weird exceptional case that could easily be overlooked by a human. In practice, defining and checking a full set of invariants provides greater confidence that no edge cases have been missed.

TL;DR

MythX integrates fuzzing, symbolic analysis, and static checks into an easy-to-use interface and should be part of the toolbox of every Solidity developer and auditor. By checking global and functional security properties you can uncover subtle bugs and gain additional confidence that the code behaves correctly:

• By adding preconditions and postconditions to functions you can verify that the function always behaves as expected;
• Contract invariants allow you to ensure that some condition always holds during execution.

Check out the documentation for instructions on setting up MythX for Remix, Truffle, VS Code and other environments. Sign up for a free account on the MythX dashboard. You can read MythX reviews here.

You might also like:

• Generic bug detection with MythX
• Checking custom properties using the AssertionFailed event
• Awesome MythX tools

Get Best Software Deals Directly In Your Inbox