What is Echidna?

In this part, we will cover the very basics of Echidna usage. Echidna is an animal, but it is also the name of a Solidity fuzzer. This tool is really worth mastering since a skilled user can be able to test a smart contract with it in an automated manner to discover bugs that can be missed using a manual approach (however, it cannot completely replace manual testing either).

Having said that, you probably now wonder if it’s possible to test automatically for bugs in your smart contracts. Echidna may come in handy if you’re a developer looking to do an extended QA of your smart contract or an auditor looking specifically for bugs in the code. However, it is by no means an auto-hack tool and requires serious guidance from the user. In this article, we’d like to demystify some basic echidna usage so you can start testing yourself!

How can you use echidna and how it works

Echidna is a command line tool, in this article, we’ll use it on Ubuntu, but it is compatible with other OSes too. The downside is that it will need a bit more than just a target smart contract to work – a small fuzzing environment setup will be needed. Echidna is a fuzzer, but in the blockchain world, we cannot “crash” something as usual fuzzers (like AFL or Honggfuzz) do. 

Rather, we have to prepare a suitable testcase with a predictable outcome, run Echidna on it, and the tool will start feeding various inputs to our testcase. If our outcome is met (or not), the fuzzer will let us know. Essentially, it is analogous to a tool that will feed all possible inputs to our tested function and determine whether or not it returned an expected value. 

The “predictable outcome” from function is named Invariants or Assertions. They are simply two types of if-checks that you will need to implement in your fuzzing functions (either the first or second one). Despite sounding complex, they are just names of a true/false checks in a fuzzing function.

Let’s assume that we will fuzz a function that checks a transfer operation, and at the end of a single fuzzing cycle we check if the balance after the transfer is lower  or equal to the balance before the transfer. We can do it either using an invariant:

return balanceAfter =< balanceBefore;
//assertion:
assert(balanceAfter =< balanceBefore);

When the program is running, Echidna will feed various inputs to the functions before comparing the current values to our invariant or assertion. Based on this, we can infer, if a certain function is able to return some value we believe is incorrect (e.g., the balance after a transfer is higher than before it). Once such an anomaly is pointed out by Echidna, we can manually investigate what went wrong. Echidna will also show us the call order of functions needed to trigger our “crash”. 

In the end, it is also possible to check a coverage report, so we will know which part of the code was covered by Echidna (however, keep in mind that covering the code doesn’t mean all possible cases were covered – this is still the responsibility of the fuzzer operator).

That’s all the theory. Let’s try to prepare a complete test case and fuzz it!

Setup directory structure

We want to test (fuzz) a Solidity smart contract automatically. We will do it function by function (because that’s how an Echidna works – it cannot swallow the whole contract at once). Since Echidna uses an underlying compiler, the directory structure will be similar to that of a Hardhat project.

Our setup consists of the following files:

Config.yaml:

testMode: assertion
corpusDir: corpus

hardhat.config.js:

/** @type import('hardhat/config').HardhatUserConfig */
module.exports = {
  solidity: "0.8.17",
};

package.json:

{
  "name": "vulnbank",
  "version": "1.0.0",
  "description": "",
  "main": "index.js",
  "scripts": {
    "test": "echo \"Error: There are no tests.\" && exit 1"
  },
  "author": "",
  "license": "ISC",
  "devDependencies": {
    "hardhat": "^2.12.2"
  },
  "dependencies": {
    "@openzeppelin/contracts": "^4.8.0"
  }
}

contracts/VulnerableBank.sol:

pragma solidity 0.8.17;


import "@openzeppelin/contracts/token/ERC20/IERC20.sol";


contract VulnerableBank {


    mapping(address => uint256) public userBalance;
    IERC20 public vulnerableCurrency;


    constructor(address _vulnerableCurrency) {
        vulnerableCurrency = IERC20(_vulnerableCurrency);
    }


    function deposit(uint256 amount) public {


        vulnerableCurrency.transferFrom(msg.sender, address(this), amount);
        userBalance[msg.sender] = 1234; 
    }


    function withdraw(uint256 amount) public {


        require(userBalance[msg.sender] > amount, "Insufficient balance.");
        userBalance[msg.sender] -= amount; 
        vulnerableCurrency.transfer(msg.sender, amount);


    }
}

The above contract will be our fuzz target. We will use contracts/Template.sol, which will be our fuzzing testcase.

How do we fuzz it?

In this example, we will fuzz the Deposit function.

Setting up Echidna is pretty straightforward. We can download it from the official repo here (link) and just unpack. For easier use, we can actually move it to a PATH directory. We will start by preparing a generic template and then think about what to actually fuzz. We want to start with a “clean” template and later insert some reasonable test cases.

contracts/Template.sol:

pragma solidity ^0.8.17;


import "./VulnerableBank.sol";
import "@openzeppelin/contracts/token/ERC20/ERC20.sol";


contract DummyERC20 is ERC20 {


    constructor(string memory _name, string memory _symbol) ERC20(_name, _symbol) {}


    function mint(address _to, uint256 _amount) external {
        _mint(_to, _amount);
    }
}


contract EchidnaTemplate {


    VulnerableBank vulnerableBankContract;
    DummyERC20 vulnerableCurrency;


    constructor() {
        vulnerableCurrency = new DummyERC20("VulnCoin", "VC");
        vulnerableCurrency.mint(address(this), type(uint128).max);
        vulnerableBankContract = new VulnerableBank(address(vulnerableCurrency));
    }




    function testDeposit(uint256 amount) public {
        //testcase here
    }


    function testWithdraw(uint256 amount) public {
        //testcase here
    }
}

As you can see, the template actually initializes our contracts and also it mints a helper token which will be the currency of our bank target. We are not fuzzing that currency, but we need it to actually test the deposit and withdrawal functions. 

We will soon run Echidna while in the main directory. Run npm install to install all the required dependencies. Then: 

echidna-test . --contract EchidnaTemplate --config config.yaml

Additionally, subsequent runs should be performed by clearing the artifacts prior to invoking the Echidna. Since we will be experimenting with the fuzzer, it is good to clear compiled files to reflect the latest changes each time.

rm -rf artifacts/ && echidna-test . --contract EchidnaTemplate --config config.yaml

Wait for a moment before running to properly fill the Template.sol, which is described in a later paragraph, as running it so far will do nothing because our test cases are empty. In the following listings, we will present the updated content of the Template.sol testcase. Keep in mind that other files stay the same.

The very basic testcase:

contracts/Template.sol:

pragma solidity ^0.8.17;


import "./VulnerableBank.sol";
import "@openzeppelin/contracts/token/ERC20/ERC20.sol";


contract DummyERC20 is ERC20 {


    constructor(string memory _name, string memory _symbol) ERC20(_name, _symbol) {}


    function mint(address _to, uint256 _amount) external {
        _mint(_to, _amount);
    }
}


contract EchidnaTemplate {


    VulnerableBank vulnerableBankContract;
    DummyERC20 vulnerableCurrency;


    constructor() {
        vulnerableCurrency = new DummyERC20("VulnCoin", "VC");
        vulnerableCurrency.mint(address(this), type(uint128).max);
        vulnerableBankContract = new VulnerableBank(address(vulnerableCurrency));
    }




    function testDeposit(uint256 amount) public {
        //testcase here
        //assert(1 == 1);
        //assert(amount != 1337);
    }


    function testWithdraw(uint256 amount) public {
        //testcase here


        //assert(amount != 1337);
        //assert(1 == 2);
        //assert(1 == 1);
    }
}

To understand assertions, you can run echidna on such a testcase with one of the assertions uncommented.

If you are running it for the first time, try both and observe the results. The last one shows the purpose in the most clear way: the only “1337” input will cause the fuzzer to throw a “false” at the assertion.

The real testcase

The function takes a certain number of tokens from the user and adds them to the user’s balance. For simplicity, we ignore the possible unchecked return value here (assuming the bank initializer checks the token instead). So our test case should be checking if: the money is properly taken away from user account, and the money is added to contract balance and if still the amount is the same.

contracts/Template.sol:

pragma solidity ^0.8.17;


import "./VulnerableBank.sol";
import "@openzeppelin/contracts/token/ERC20/ERC20.sol";


contract DummyERC20 is ERC20 {


    constructor(string memory _name, string memory _symbol) ERC20(_name, _symbol) {}


    function mint(address _to, uint256 _amount) external {
        _mint(_to, _amount);
    }
}


contract EchidnaTemplate {


    VulnerableBank vulnerableBankContract;
    DummyERC20 vulnerableCurrency;


    constructor() {
        vulnerableCurrency = new DummyERC20("VulnCoin", "VC");
        vulnerableCurrency.mint(address(this), type(uint128).max);
        vulnerableBankContract = new VulnerableBank(address(vulnerableCurrency));
    }




    function testDeposit(uint256 amount) public {
        //testcase here


        uint256 balanceBefore = vulnerableBankContract.userBalance(address(this));


        vulnerableBankContract.deposit(amount);


        uint256 balanceAfter = vulnerableBankContract.userBalance(address(this));
        


        assert(balanceBefore + amount == balanceAfter);
    }


    function testWithdraw(uint256 amount) public {
        //testcase here
    }
}

The testcase does the following:

• Checks balance in the bank before transfer,
• Transfers some amount there,
• Checks balance in the bank after transfer,
• Asserts if the bank balance after is equal to balance before + the deposited amount,
• If the last check fails, that means that the bank mishandles the transfer.

We run the fuzzer once more with the command:

rm -rf artifacts/ && echidna-test . --contract EchidnaTemplate --config config.yaml

which produces the following result:

which means we should examine the testDeposit() function. Indeed, it is intentionally bugged.

Viewing coverage reports

To check the text coverage report, we should wait for the fuzz test to complete (otherwise we won’t see the HTML file) and later check the corpus/ directory:

The report contains information on all contracts tested during the fuzzing. The below image shows the part responsible for our VulnerableBank contract.

You can see the full explanation of the colors (and the text symbols of coverage) on the tool’s GitHub page here.

We recommend you also our second version of “Automated auditing” topic, available here -> https://monethic.io/automated-auditing-part-2-usage-of-ai-for-smart-contracts-testing/