Fuzzing with Echidna

Intro

Fuzzing is a well-known technique in the security industry to discover bugs in software — invalid, unexpected, or random data is generated automatically and injected into the software to find issues.

In the context of smart contract security, fuzzing tools are relatively new but are gaining more attraction recently. It is pivotal that a smart contract — with its immutable character — is tested thoroughly before any deployment to production. Having an adequate test coverage of your code using unit tests is essential, but there will always be edge cases you did not test for. Thus, it is best practice to extend your testing strategy by using additional security tools, such as static analyzers and fuzzers.

After reading this blog post, you should gain the following takeaways:

• The core component of an audit is a manual review — this is where you catch the most bugs.
• Fuzz tests can be very useful for catching edge cases.
• There are different tools available for fuzz testing. One of the better-known tools is Echidna.
• Have a basic understanding of how Echidna works.

Before introducing Echidna in more detail, here is a list of the more popular security-testing tools available today:

1. Slither – static analysis tool (developed by TrailOfBits)
https://github.com/crytic/slither

2. Manticore – uses symbolic execution to detect vulnerabilities (developed by TrailOfBits)
https://github.com/trailofbits/manticore

3. Scribble – allows one to annotate a smart contract with properties and raises exceptions when the property is violated.
https://github.com/ConsenSys/scribble

4. MythX – uses symbolic execution to detect vulnerabilities (developed by Consensys)
https://mythx.io/

5. Mythril – paid cloud service that includes static analysis, symbolic analysis, and fuzzing (developed by Consensys)
https://github.com/ConsenSys/mythril

6. Foundry support for fuzz testing
https://book.getfoundry.sh/forge/fuzz-testing.html

7. Dapptools support for fuzz testing
https://github.com/dapphub/dapptools/tree/master/src/dapp#property-based-testing

8. Certora - paid service that uses formal verification
https://www.certora.com/

9. Echidna – fuzzing tool (developed by TrailOfBits)
https://github.com/crytic/echidna

In the next chapter we will go deeper into Echidna, a program written in Haskell by the security experts from Trail of Bits.

Echidna

Echidna uses a style of fuzzing called property-based fuzzing. Instead of looking for crashes like a traditional fuzzer, Echidna tries to break user-defined invariants (a.k.a. properties).

Invariants are properties of the program state that are expected to always be true. These invariants have to be manually written in Solidity, as opposed to writing unit tests in Javascript. Currently, Echidna does not support automated fuzz tests.

Once these invariants are defined, Echidna tries to falsify these invariants by generating random sequences of calls to the contract.

Enough theory for now — let’s look at the code.

Installation

Run Echidna by using pre-compiled binary:
https://github.com/crytic/echidna/releases/tag/v2.0.2

or

Another neat way to run Echidna is by using the trailofbits eth-security-toolbox docker image:
https://github.com/trailofbits/eth-security-toolbox

Example 1

Consider the following contract (similar vulnerability as Ethernaut’s Fal1Out challenge).

// ICO.sol
contract ICO {
    bool is_paused;
    address owner = msg.sender;

    function IC0() public {
        owner = msg.sender;
    }

    modifier isOwner() {
        require(owner == msg.sender);
        _;
    }
		
    function resume() public isOwner {
      is_paused = false;      
    }
}

The resume() function can only be called by the owner of the contract. Let’s write a fuzz test to see if Echidna can find a way to break the contract and set the is_paused variable to true:

import "./ICO.sol";

// ICOFuzzTest.sol
contract ICOFuzzTest is ICO {

    constructor() public {
        is_paused = true;
        owner = address(0x0);
    }

    function echidna_test_pause() public view returns (bool) {
        return is_paused == true;
    }
}

Initialization code goes into the constructor. In the above code, is_paused is set to true and the owner is set to 0x0.

Next, we write the test which defines that is_paused should always return true. Note that for executing the tests, Echidna randomly uses the following caller addresses: 0x10, 0x20, and 0x30. In other words, the above test says that there shouldn’t be any way for the caller addresses to set the is_paused variable to false.

Note: All fuzz tests must start with echidna_ in order for Echidna to pick them up.

To start the fuzz test, run the following:

echidna-test ICOFuzzTest.sol --contract ICOFuzzTest

Echidna immediately returns the result:

The test failed, as Echidna found a way to falsify the invariant by making the following calls:

1. IC0()
2. resume()

To the trained eye, the vulnerability was pretty obvious. The IC0() function is not a valid constructor as it is written with the number ‘0’ instead of the letter ‘O’. In addition, with Solidity > 4.21 you need to define the constructor using the constructor keyword instead of using the contract name.

As IC0() is a normal function and is lacking an access modifier, it can be called by anyone to gain ownership. After gaining ownership, the resume function can be called to set is_paused to true.

As simple as the above example was, it clearly demonstrates how Echidna works — it automatically generates arbitrary transactions (with random input) to test the invariant.

Example 2

Consider the following contract:

pragma solidity 0.7.0;

contract Pausable {
    bool is_paused;

    function paused() public {
        is_paused = true;
    }

    function resume() public {
        is_paused = false;
    }
}

contract Token is Pausable {
    mapping(address => uint256) public balances;

    constructor() {
        is_paused = true;
    }

    function transfer(address to, uint256 value) public {
        require(!is_paused);

        uint256 initial_balance_from = balances[msg.sender];
        uint256 initial_balance_to = balances[to];

        balances[msg.sender] -= value;
        balances[to] += value;

        assert(balances[msg.sender] <= initial_balance_from);
        assert(balances[to] >= initial_balance_to);
    }
}

Note that the above code uses Solidity version 0.7.0. For Solidity version 0.8.0 and above the compiler has built in underflow/overflow checks but for older versions you need to take care of it yourself.

In the previous Example 1 we used the “property” testing mode. Echidna supports other testing modes such as “assertion” and “dapptest” (see here). In this example, we run Echidna in “assertion” testing mode. Hereby, Echidna looks out for Solidity assertions in your code and tries to falsify them by generating random transactions and inputs.

To start the fuzz test in “assertion” mode run:

echidna-test Token.sol --test-mode assertion --contract Token

Echidna prints out the following result:

It checked every function for assertions and found 1 test that failed in the transfer(…) function.

Can you figure out why?

The test failed by making the following call:

1. resume()
2. transfer(0x0, 1)

Echidna first called resume to set is_paused = false which is necessary to enter the transfer function. In the 2nd step, transfer was called with the parameters 0x0 for the to address and 1 for the value. The interesting line that brought the test to fail is this:

balances[msg.sender] -= value;

The balance for msg.sender is 0 and gets decreased by 1. This results in an underflow that is not handled as we are using Solidity version 0.7.0. As a consequence, balance of msg.sender will be set to the maximum number of uint256. This behavior breaks the first assertion

assert(balances[msg.sender] <= initial_balance_from);

as now the new balance is much higher than the initial one.£

The easiest way to avoid the above issue is to use Solidity 0.8.0 or higher. If for whatever reason you can’t do that, the 2nd best option is to use OpenZeppelin’s SafeMath library.

The best way to start with Echidna is at its official Github page. For advanced configuration and further examples, visit this tutorial page.

Alternatives to Echidna

Scribble

Scribble is a so-called specification language that allows you to annotate your smart contracts with properties. In a second step, Scribble transforms the annotations into Solidity code with concrete assertions.

The aim of Scribble is to have one universal annotation language for defining your fuzz tests and then to reuse this between different tools.

(Source: https://docs.scribble.codes/)

The above picture shows that Scribble can be used with fuzzing tools like Mythril and MythX (likely because all of these three tools have been developed by Consensys).

As Scribble compiles the annotations into simple Solidity assertions, it should also be possible to use Scribble in combination with Echidna, using the “assertion” testing mode (see here). Please reach out to us if you have experience with this setup!

Foundry

Foundry has become more and more popular over the recent months (see here).

So if Foundry is already your development framework of choice, you don’t have to look further. Foundry has built-in support for fuzz testing. When using Foundry, you already write your unit tests in Solidity. If the test function takes at least 1 parameter, then Foundry automatically runs the test as a property-based fuzz test (see here).

The approach Foundry follows is similar to writing fuzz tests with Echidna but quite different to the annotation-based approach Scribble uses.

While both Foundry and Echidna fall under the same category of property-based fuzzing, Echidna uses more advanced techniques like generating random transactions with random inputs and also keeps track of those transactions to achieve high coverage. On the other hand, Foundry focuses on generating random inputs for your test functions and has support for excluding certain values.

Final Thoughts

Nobody said it’s going to be easy!

Writing fuzz tests isn’t trivial. In the beginning, you will probably spend a lot of time writing meaningful tests — there is a deep learning curve. Additionally, there are a lot of different tools and setups available, and you must first find out what fits best for you and your team.

Nevertheless, the effort will pay off and will make your code more secure. As a builder or auditor, you should add fuzz tests to your toolbox.

References/Resources

A list of security tools:
https://github.com/ConsenSys/ethereum-developer-tools-list#security-tools
https://github.com/trailofbits/eth-security-toolbox

Fuzzing complex projects with Echidna: https://ventral.digital/posts/2021/12/21/fuzzing-complex-projects-with-echidna-sushi-bentobox

Comparison of Slither, MythX, Mythril, Manticore, SmartCheck: https://medium.com/@charingane/smart-contract-security-tools-comparison-4aaddf301f01

Scribble:
https://consensys.net/blog/news/introducing-scribble-by-consensys-diligence/
https://consensys.net/diligence/blog/2021/07/introducing-scribble-generator/

Patrick Collins:
https://github.com/PatrickAlphaC/hardhat-security-fcc
https://www.youtube.com/watch?v=TmZ8gH-toX0