Introduction to Echidna

Explore advanced smart contract security with Echidna – your go-to tool for automated vulnerability detection in Solidity, ensuring robust solidity code and heightened security.

What is Fuzzing?

At its core, fuzzing involves three key steps. First, you generate a random input. Next, you test a specific aspect using that input. If the test case fails, you stop and notify the user. If it passes, you initiate a new cycle with fresh input to test again.

The intriguing aspect of web3 fuzzing, especially in smart contracts, lies in how we approach testing something. Unlike traditional fuzzing in web2 where the goal is to crash the program, in web3, the objective is to verify user-defined properties (invariants). Fuzzers generate random inputs to check whether a specified incorrect state can be reached.

System Properties and Pre-conditions

System properties outline the expected behavior of the system, always mathematically true given certain pre-conditions. Pre-conditions act as barriers, specifying when a property should be true.

Example:

Invariant 1:

Consider the transferFunction() responsible for transferring tokens between users. The expected behavior here is that when transferring tokens from user A to user B, A's balance should decrease by a certain amount while B's balance should increase by the same amount. However, this is meaningful only if A has a token balance to spend initially – that's the pre-condition. The transfer function should exhibit this behavior given A possesses some tokens. Fuzz testing, using tools like Echidna, validates whether this expected behavior holds true.

Invariant 2:

Another example is the assertion that a user's balance should never exceed the total supply of tokens. This holds true if the total supply represents the sum of all user balances. There's no logical reason for an individual user's balance to surpass the total supply. If it does, it's likely indicative of a bug in the code.

Fuzzing, with its systematic approach to validating these invariants, becomes an invaluable tool in ensuring the robustness and security of smart contracts in the dynamic landscape of web3.

Role of Echidna:

Now that we grasp the significance of fuzzers in generating random inputs and testing system properties, let's delve into the pivotal role played by Echidna. This open-source tool, with a dash of human intervention, excels in delivering optimal results and heightened productivity during audits and manual reviews. Echidna operates as a property-based fuzzer, systematically generating inputs to unveil bugs in a program.

How Echidna Works:

Echidna operates on two essential elements: the target contract and the properties to test. The target contract is the system undergoing the fuzzing process – it's what Echidna relentlessly tests using various functions and inputs. The properties, on the other hand, are the characteristics being scrutinized. Echidna vigorously interacts with the smart contract, assessing whether it adheres to expected properties. In essence, we furnish Echidna with these two inputs and task it with challenging the invariants, validating crucial aspects of the system.

Key Considerations with Echidna:

• Think of Echidna as an Externally Owned Account (EOA): Picture Echidna as an external entity interacting with the target contract as an externally owned account would. This perspective helps in understanding Echidna's role in the testing process.

• Echidna's Operation:

     - Echidna calls a sequence of functions with random inputs in both the target and inherited contracts.

     - It diligently checks whether the specified property holds true.

     - Properties, in this context, resolve to a truthy value, indicating the expected behavior or condition.

Echidna, with its methodical approach, proves to be an invaluable ally in our quest to ensure smart contracts' integrity and adherence to defined properties.

Installing Echidna:

If you're ready to dive into Echidna for your smart contract security needs, here's how you can get started:

GitHub Repository:

Visit the Echidna GitHub repository to explore its features and documentation:

• https://github.com/crytic/echidna

Install via Docker:

Easily pull the Echidna Docker image from Trail of Bits with this command:

docker pull trailofbits/eth-security-toolbox

Then, run it interactively while mounting your current directory:

docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

Install via Binary:

For those who prefer using binaries, you can find the latest releases on the official GitHub releases page: 

• https://github.com/crytic/echidna/releases/tag/v2.2.1

Additional Information:

For a detailed guide on installation and more insights into Echidna, refer to the official documentation: 

• https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/introduction/installation.md

If facing errors due to crytic module:

python3 -m venv venv
source venv/bin/activate  # On Windows, use 'venv\Scripts\activate'
python -m pip install crytic-compile

Solc-select installation

git clone https://github.com/crytic/solc-select.git
cd solc-select
python3 setup.py install 

If using a virtual environment, this must be set so that the echidna can run successfully.

solc-select install 0.8.0
export SOLC_VERSION="0.8.0"
echo $SOLC_VERSION

Fuzzing Approaches:

Property-based Functional Fuzzing:

• Emphasizes testing functional properties under varied inputs.

• Defines specific properties and employs a fuzzer to validate them, mostly needing to use echidna_function_name which returns a boolean with no arguments.

• Ensures consistent system behavior across diverse input scenarios.

• Excels in uncovering subtle bugs and unexpected behaviors.

Assertion-based Fuzzing:

• Focuses on validating explicit assertions within the code using the assert() function.

• Involves inserting conditions at critical points for systematic testing.

• Provides flexibility to target specific functions without altering logic.

• Effective in catching unexpected states, ensuring code resilience.

Running Echidna with Examples:

Property-based Functional Fuzzing example-1

Target Contract: tokenTransfer.sol

// SPDX-License-Identifier: AGPL-3.0
pragma solidity ^0.8.0;

contract NewOwnerContract {
    address public newOwner = msg.sender;

    modifier onlyNewOwner() {
        require(msg.sender == newOwner, "NewOwnerContract: Caller is not the owner.");
        _;
    }
}

contract PausableToken is NewOwnerContract {
    bool private _isPaused;

    function isPaused() public view returns (bool) {
        return _isPaused;
    }

    function pause() public onlyNewOwner {
        _isPaused = true;
    }

    function resume() public onlyNewOwner {
        _isPaused = false;
    }

    modifier whenNotPaused() {
        require(!_isPaused, "PausableToken: Contract is paused.");
        _;
    }
}

contract TokenTransfer is NewOwnerContract, PausableToken {
    mapping(address => uint256) public accountBalances;

    function performTransfer(address to, uint256 amount) public whenNotPaused {
        unchecked {
            accountBalances[msg.sender] -= amount;
            accountBalances[to] += amount;
        }
    }
}

Echidna Test Contract Code: template.sol

// SPDX-License-Identifier: AGPL-3.0
pragma solidity ^0.8.0;

import "./tokenTransfer.sol";

/// @dev Run the template with
///      ```
///      solc-select use 0.8.0
///      echidna template.sol
///      ```
contract NewTestToken is TokenTransfer {
    address echidnaTester = tx.origin;

    constructor() public {
        accountBalances[echidnaTester] = 10000;
    }

    function echidna_TestBalance() public view returns (bool) {
        // added the property
        return accountBalances[echidnaTester] <= 10000;
    }
}

1. Target Contract: tokeTransfer.sol  

• Implements Ownable, Pausable, and Token contracts.

2. Test Contract Code: template.sol

• Uses Echidna to generate random inputs for the Token contract.

• Aims to test the property that the balance of a specific address does not exceed a predefined limit (10,000 tokens).

• Echidna successfully identified an overflow/underflow vulnerability.

Terminal Command to Run:

echidna template.sol --contract NewTestToken

Output:

Observation:

Echidna successfully identified an overflow vulnerability.

Property-based Functional Fuzzing example-2

Target Contract: YourTokenContract.sol

// SPDX-License-Identifier: AGPL-3.0
pragma solidity ^0.8.0;

contract TokenOwner {
    address public ownerAddress = msg.sender;

    function setOwner() public {
        ownerAddress = msg.sender;
    }

    modifier onlyOwner() {
        require(ownerAddress == msg.sender, "Unauthorized access");
        _;
    }
}

contract PausableToken is TokenOwner {
    bool isTokenPaused;

    function getTokenPausedStatus() public view returns (bool) {
        return isTokenPaused;
    }

    function pauseToken() public onlyOwner {
        isTokenPaused = true;
    }

    function resumeToken() public onlyOwner {
        isTokenPaused = false;
    }

    modifier whenTokenNotPaused() {
        require(!isTokenPaused, "Token functionality is paused");
        _;
    }
}

contract TokenHandler is TokenOwner, PausableToken {
    mapping(address => uint256) public userTokenBalances;

    function transferTokens(address to, uint256 amount) public whenTokenNotPaused {
        userTokenBalances[msg.sender] -= amount;
        userTokenBalances[to] += amount;
    }
}

Echidna Test Contract Code: template.sol

// SPDX-License-Identifier: AGPL-3.0
pragma solidity ^0.8.0;

import "./YourTokenContract.sol";

contract TestYourTokenContract is PausableToken {
    constructor() {
        pauseToken(); // pause the token functionality
        ownerAddress = address(0); // lose ownership
    }

    // Now we are in a state where the test contract is no longer the owner of the system.

    function echidna_testTokenCannotBeUnpaused() public view returns (bool) {
        return isTokenPaused;
    }
}

1. Target Contract: YourTokenContract.sol

•  Implements Ownable, Pausable, and Token contracts.

2. Test Contract Code: template.sol

• Utilizes Echidna to explore the contract's behavior under various inputs.

• Seeks to identify vulnerabilities related to contract pausing and ownership.

• Echidna reveals a critical bug where ownership can be lost, and the contract can be unpaused through specific function calls.

Terminal Command to Run:

echidna template.sol --contract TestYourTokenContract

Output:

Observation:

Echidna successfully identified a critical bug where ownership is lost, and the contract can be unpaused by calling the setOwner() and resumeToken() functions.

Assertion-based Fuzzing:

Echidna Test Contract: template.sol

// SPDX-License-Identifier: AGPL-3.0
pragma solidity ^0.8.0;

import "./YourTokenContract.sol";

contract TestYourTokenContract is PausableToken {
    constructor() {
        pauseToken(); // pause the token functionality
        ownerAddress = address(0); // lose ownership
    }

    // Now we are in a state where the test contract is no longer the owner of the system.


    function testTokenCannotBeUnpaused() public {
        assert(isTokenPaused);
    }
}

Target Contract: YourTokenContract.sol

•  Implements Ownable, Pausable, and Token contracts.

Test Contract Code: template.sol

• Focuses on asserting specific conditions within the code.

• Involves calling functions with explicit assertions to validate the contract's behavior.

• Provides flexibility to target specific functions or conditions without altering the underlying logic.

• A powerful method for catching unexpected code states and ensuring resilience to various inputs and scenarios.

Terminal Command to Run Assertion-based Fuzzing:

echidna template.sol --contract TestYourTokenContract --test-mode assertion

Output:

Result:

Echidna successfully identified the critical bug in the code where isTokenPaused can be set to false by calling certain functions.

These examples demonstrate how Echidna can effectively uncover vulnerabilities and critical bugs in smart contract code, making it a valuable tool for security testing.

Key Takeaways:

• Echidna, as a property-based fuzzer, plays a pivotal role in smart contract security by systematically testing against specified properties.

• A balanced testing approach, incorporating unit testing, manual testing, automated testing tools, and Echidna, contributes to a robust security posture.

• Property-based functional fuzzing and assertion-based fuzzing are powerful techniques that uncover subtle bugs and validate explicit assertions, enhancing the overall security testing strategy.

• Real-world examples demonstrate Echidna's capability to identify vulnerabilities and critical bugs, making it an invaluable tool for Solidity developers.

Conclusion:

The effectiveness of Echidna in smart contract security testing is evident through real-world examples. The combination of property-based functional fuzzing and assertion-based fuzzing provides a comprehensive approach to uncovering vulnerabilities and critical bugs. Solidity developers are encouraged to embrace these advanced fuzzing strategies to ensure the resilience and integrity of their smart contracts.

Was it useful? Help us to improve!

With your feedback, we can improve the letter. Click on a link to vote:

• 👍 That helped me. Thanks

• 😐 Meh - was ok.

• 👎 Not interesting to me.