Echidna Fuzz Testing (Solidity Code Example)

‍Examples of fuzzing with Echidna 

1. Save the solidity contract as TestEchidna.sol
2. In the folder where your contract is stored execute the following command.

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

Inside docker, your code will be stored at /code, in the root directory.

3. See the comments below and execute echidna commands.

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

/*
echidna TestEchidna.sol --contract TestCounter
*/
contract Counter {
    uint256 public count;

    function inc() external {
        count += 1;
    }

    function dec() external {
        count -= 1;
    }
}

contract TestCounter is Counter {
    function echidna_test_true() public view returns (bool) {
        return true;
    }

    function echidna_test_false() public view returns (bool) {
        return false;
    }

    function echidna_test_count() public view returns (bool) {
        // Here we are testing that Counter.count should always be <= 5.
        // Test will fail. Echidna is smart enough to call Counter.inc() more
        // than 5 times.
        return count <= 5;
    }
}

/*
echidna TestEchidna.sol --contract TestAssert --test-mode assertion
*/
contract TestAssert {
    function test_assert(uint256 _i) external {
        assert(_i < 10);
    }

    // More complex example
    function abs(uint256 x, uint256 y) private pure returns (uint256) {
        if (x >= y) {
            return x - y;
        }
        return y - x;
    }

    function test_abs(uint256 x, uint256 y) external {
        uint256 z = abs(x, y);
        if (x >= y) {
            assert(z <= x);
        } else {
            assert(z <= y);
        }
    }
}

‍

Testing time and sender

Echidna can fuzz timestamp. Range of timestamp is set in the configuration with a ddefault of 7 days.

Contract callers can also be set in the configuration. Default accounts are

• 0x10000
• 0x20000
• 0x30000

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

/*
docker run -it --rm -v $PWD:/code trailofbits/eth-security-toolbox
echidna EchidnaTestTimeAndCaller.sol --contract EchidnaTestTimeAndCaller
*/
contract EchidnaTestTimeAndCaller {
    bool private pass = true;
    uint256 private createdAt = block.timestamp;

    /*
    test will fail if Echidna can call setFail()
    test will pass otherwise
    */
    function echidna_test_pass() public view returns (bool) {
        return pass;
    }

    function setFail() external {
        /*
        Echidna can call this function if delay <= max block delay
        Otherwise Echidna will not be able to call this function.
        Max block delay can be extended by specifying it in a configuration file.
        */
        uint256 delay = 7 days;
        require(block.timestamp >= createdAt + delay);
        pass = false;
    }

    // Default senders
    // Change the addresses to see the test fail
    address[3] private senders =
        [address(0x10000), address(0x20000), address(0x30000)];

    address private sender = msg.sender;

    // Pass _sender as input and require msg.sender == _sender
    // to see _sender for counter example
    function setSender(address _sender) external {
        require(_sender == msg.sender);
        sender = msg.sender;
    }

    // Check default senders. Sender should be one of the 3 default accounts.
    function echidna_test_sender() public view returns (bool) {
        for (uint256 i; i < 3; i++) {
            if (sender == senders[i]) {
                return true;
            }
        }
        return false;
    }
}

‍