Ethereum Smart Contract Fuzz-Testing with Echidna

What is Fuzzing?                

Fuzz testing (or fuzzing) is an automated software testing method with the goal to find vulnerabilities, security issues, and defects of the application. The idea is to inject invalid, malformed, or unexpected inputs into the application using a fuzzing tool and observing how the system reacts to those inputs (e.g., exceptions, leakage of information, or application crashes).

In the security community, fuzzing is a well-known technique. To discover faults in the application, fuzzing generates more or less random inputs. Traditional software fuzzers are recognized to be very effective bug finders.

Ethereum Property-Based Fuzzing

Echidna is part of a fuzzing family called property-based fuzzing and was influenced by QuickCheck. Rather than looking for crashes like a traditional fuzzer, Echidna will try to break user-defined invariants.

Invariants

In smart contracts, invariants are Solidity functions that can represent any wrong or invalid state the contract can achieve, such as

  • Incorrect access controlΒ results when the attacker becomes the contract’s owner.
  • Incorrect state machine when the tokens can be transferred even with the contract paused.
  • Incorrect arithmetic: the user’s balance can overflow, resulting in a limitless supply of free tokens.

Installation

You install echidna using docker or binaries.

Docker

Run the below command for running with docker.

$ docker run -it --rm  -v $PWD:/code/  trailofbits/eth-security-toolbox

The parameters are explained in brief.

-it is --interactive + --tty
-rm automatically removes the container when it exits
-v  mount a volume, where $PWD is the source and current path of the host machine and /code is the destination path in the docker
trailofbits/eth-security-toolbox is the docker image name 

For the first time, the docker will download the image and then run.

Binaries

You can download and use the binaries directly from this link.

Example Usage

Let’s consider a simple Ether balance (Ethbalance.sol) contract to test.

//SPDX-License-Identifier: MIT
pragma solidity ^0.8.9;

contract EthBalance{

    mapping(address => uint256) balance;
    uint256 z;

    constructor()
    {
       z = 100;
       balance[msg.sender] = 0;
    }
       // Function changing the value of z
    function changeZ(uint256 _newval) external {
        z = _newval;
    }

    // lets assume a max of 100 Eth is allowed to deposit per user
    function deposit(uint256 _amount ) payable external {
      // if (balance[msg.sender] + _amount<= 100)
        balance[msg.sender] += _amount;
    }

}


contract Testbalance is EthBalance{           // Below functions are the invariants or property tests     
         function echidna_deposit_under_100() public view returns(bool){
               return balance[msg.sender] <= 100;
         }

        function echidna_changeZ() public view returns (bool)
        {
            return z == 100;
        }
}

Echidna property or invariant tests

The contract Ethbalance, has two functions deposit() and changeZ() that update the values of the state/storage variables balance and z.

The contract is expected to satisfy two requirements.

  • the balance for any user must not exceed 100 ETH
  • the value of z must remain constant throughout after its initialization to 100 in the constructor.

However, the contract has no check or boundary conditions added to satisfy these requirements. In order to catch these errors, we introduce Echidna property tests with the contract Testbalance that inherits the Ethbalance.

The test echidna_deposit_under_100() expects the balance of any user does not exceed 100, and echidna_changeZ() expects z to be equal to 100.

Running the Tests

To run the tests, start with the docker command

$ docker run -it --rm  -v $PWD/code:/code  trailofbits/eth-security-toolbox

It starts the docker image and enters the docker terminal as below.

Fig: Run docker image

To run the tests, enter the directory where the contracts are mounted, in this case /code in the docker CLI,

$ cd /code

and then run the below command.

$ echidna-test <file name>  --contract <contract name>

In this case, the file name is Ethbalance.sol and the contract name is Testbalance.

$ echidna-test Ethbalance.sol --contract Testbalance

The above command starts the tests with the below results.

Fig: Results of the echidna property tests

As seen above, the results of the tests, using a particular call sequence, the echidna tool was able to catch the errors as the contract failed to add the boundary conditions.

Making Corrections and Testing again

Let us make the corrections in the contract code to meet our requirements.

//SPDX-License-Identifier: MIT
pragma solidity ^0.8.9;

contract EthBalance{

    mapping(address => uint256) balance;
    uint256 z;

    constructor()
    {
       z = 100;
       balance[msg.sender] = 0;
    }
   
 
 // lets assume a max of 100 Eth is allowed to deposit per user
    function deposit(uint256 _amount ) payable external {
         if (balance[msg.sender] + _amount<= 100)         {
              balance[msg.sender] += _amount;
        }

}
  • Added an extra if() condition to ensure that the deposit amount does not exceed 100 ETH
  • Identified and removed the function which was updating the value of z.

With the corrections done and running the tests again.

Fig: Results after correcting contract code

Final Thoughts

As seen in this post, how passing the random and unknown inputs, the Echidna tool was able to identify the bugs associated with the boundary conditions in the contract.

The fuzz tests can play a pivotal role in identifying security bugs or loopholes such as ownership or access control at the very early stages of the contract development, thereby preventing a catastrophe in the future when the contracts are deployed to the mainnet.


Learn Solidity Course

Solidity is the programming language of the future.

It gives you the rare and sought-after superpower to program against the “Internet Computer”, i.e., against decentralized Blockchains such as Ethereum, Binance Smart Chain, Ethereum Classic, Tron, and Avalanche – to mention just a few Blockchain infrastructures that support Solidity.

In particular, Solidity allows you to create smart contracts, i.e., pieces of code that automatically execute on specific conditions in a completely decentralized environment. For example, smart contracts empower you to create your own decentralized autonomous organizations (DAOs) that run on Blockchains without being subject to centralized control.

NFTs, DeFi, DAOs, and Blockchain-based games are all based on smart contracts.

This course is a simple, low-friction introduction to creating your first smart contract using the Remix IDE on the Ethereum testnet – without fluff, significant upfront costs to purchase ETH, or unnecessary complexity.