echidna

Ethereum smart contract fuzzer

2,698

357

2,698

144

View on GitHub

Top Related Projects

mythril

3,826

Security analysis tool for EVM bytecode. Supports smart contracts built for Ethereum, Hedera, Quorum, Vechain, Rootstock, Tron and other EVM-compatible blockchains.

oyente

1,317

An Analysis Tool for Smart Contracts

slither

5,235

Static Analyzer for Solidity and Vyper

Quick Overview

Echidna is a Haskell library designed for property-based smart contract testing on the Ethereum blockchain. It uses fuzzing techniques to generate test cases and find vulnerabilities in Solidity smart contracts, helping developers identify and fix potential issues before deployment.

Pros

Powerful fuzzing capabilities for thorough contract testing
Integrates well with existing Ethereum development tools
Supports custom test generation and shrinking strategies
Provides detailed output and counterexamples for failed tests

Cons

Steep learning curve for developers unfamiliar with property-based testing
Limited documentation and examples for advanced use cases
May require significant computational resources for complex contracts
Can produce false positives in certain scenarios

Code Examples

Basic property test:

contract TestContract {
    uint256 public value;

    function setValue(uint256 _value) public {
        value = _value;
    }

    function echidna_test_value() public view returns (bool) {
        return value <= 100;
    }
}

This example tests if the value variable always remains less than or equal to 100.

Custom state setup:

contract TestContract {
    uint256 public balance;

    function setUp() public {
        balance = 1000;
    }

    function withdraw(uint256 amount) public {
        require(amount <= balance, "Insufficient funds");
        balance -= amount;
    }

    function echidna_balance_check() public view returns (bool) {
        return balance >= 0;
    }
}

This example sets up an initial state and tests if the balance never becomes negative.

Testing multiple properties:

contract TestContract {
    uint256 public x;
    uint256 public y;

    function setX(uint256 _x) public {
        x = _x;
    }

    function setY(uint256 _y) public {
        y = _y;
    }

    function echidna_test_properties() public view returns (bool) {
        return x + y >= x && x + y >= y;
    }
}

This example tests multiple properties in a single function, ensuring that the sum of x and y is always greater than or equal to both x and y individually.

Getting Started

Install Echidna:
```
pip install echidna-tool
```
Create a Solidity contract with Echidna test functions (prefixed with echidna_).
Run Echidna:
```
echidna-test YourContract.sol
```
Analyze the output for any failed properties or discovered vulnerabilities.

Competitor Comparisons

manticore

3,671

Symbolic execution tool

Pros of Manticore

More versatile, supporting analysis of binary files and smart contracts
Provides symbolic execution for deeper analysis and bug finding
Offers a Python API for custom analysis scripts

Cons of Manticore

Slower execution compared to Echidna's fuzzing approach
Steeper learning curve due to its more complex features
May require more computational resources for in-depth analysis

Code Comparison

Echidna (property-based testing):

function echidna_balance_under_1000() public view returns (bool) {
    return balances[msg.sender] <= 1000;
}

Manticore (symbolic execution):

def test_balance_under_1000(state):
    balance = state.platform.get_balance(state.creator_account.address)
    state.constrain(balance <= 1000)
    return state.can_be_true(balance <= 1000)

Key Differences

Echidna focuses on smart contract fuzzing, while Manticore offers broader analysis capabilities
Echidna is generally faster and easier to use for quick property checks
Manticore provides more in-depth analysis but requires more setup and expertise

Both tools are valuable for smart contract security, with Echidna excelling in rapid testing and Manticore offering deeper insights through symbolic execution.

mythril

3,826

Security analysis tool for EVM bytecode. Supports smart contracts built for Ethereum, Hedera, Quorum, Vechain, Rootstock, Tron and other EVM-compatible blockchains.

Pros of Mythril

Supports multiple blockchain platforms (Ethereum, EOS, Tron)
Offers a wider range of security analysis techniques (symbolic execution, taint analysis, control flow checking)
Provides a user-friendly web interface (MythX) for easier usage

Cons of Mythril

Can be slower for large contracts due to its comprehensive analysis
May produce more false positives compared to Echidna's targeted approach
Requires more setup and configuration for optimal results

Code Comparison

Echidna (property-based testing):

function echidna_balance_under_1000() public view returns (bool) {
    return balances[msg.sender] <= 1000;
}

Mythril (symbolic execution):

myth analyze <contract_file> --solv 0.5.0

Both tools aim to improve smart contract security, but they use different approaches. Echidna focuses on property-based testing, allowing developers to define specific properties that should hold true for their contracts. Mythril, on the other hand, employs a broader range of analysis techniques to identify potential vulnerabilities automatically.

While Echidna excels in targeted testing and is generally faster, Mythril offers a more comprehensive analysis across multiple platforms. The choice between the two depends on the specific needs of the project and the developer's preferences for testing methodologies.

oyente

1,317

An Analysis Tool for Smart Contracts

Pros of Oyente

Focuses on symbolic execution for vulnerability detection
Supports multiple Ethereum-based languages (Solidity, Vyper)
Provides detailed vulnerability reports with line numbers and explanations

Cons of Oyente

Less actively maintained compared to Echidna
Limited to static analysis, may miss runtime vulnerabilities
Requires more setup and dependencies

Code Comparison

Echidna (property-based fuzzing):

function echidna_test_balance() public view returns (bool) {
    return address(this).balance == 0;
}

Oyente (symbolic execution):

def analyze(self, contract):
    sym_exec = SymbolicExecutor(contract)
    vulnerabilities = sym_exec.run()
    return vulnerabilities

Echidna focuses on writing test properties in Solidity, while Oyente performs symbolic execution on the contract bytecode. Echidna's approach is more dynamic and can uncover complex runtime issues, whereas Oyente excels at identifying potential vulnerabilities through static analysis.

Both tools serve different purposes in smart contract security: Echidna for thorough testing and Oyente for quick vulnerability scanning. Using them in combination can provide a more comprehensive security assessment of Ethereum smart contracts.

slither

5,235

Static Analyzer for Solidity and Vyper

Pros of Slither

Static analysis tool, providing faster and more comprehensive code scanning
Detects a wider range of vulnerabilities and code smells
Easier integration into CI/CD pipelines due to its static nature

Cons of Slither

May produce false positives, requiring manual verification
Limited ability to detect complex, runtime-dependent vulnerabilities
Requires less user interaction but may miss edge cases that dynamic testing could reveal

Code Comparison

Slither (static analysis):

from slither.slither import Slither

slither = Slither('contract.sol')
print(slither.slither_analyzer.analyze_contracts())

Echidna (fuzzing):

contract TestContract {
    function echidna_test_balance() public view returns (bool) {
        return address(this).balance == 0;
    }
}

Slither performs static code analysis, identifying potential vulnerabilities without executing the code. Echidna, on the other hand, uses fuzzing techniques to dynamically test smart contracts by generating random inputs and checking for property violations.

While Slither can quickly scan entire codebases for common issues, Echidna excels at finding edge cases and complex vulnerabilities through repeated execution with various inputs. The choice between the two depends on the specific testing requirements and the stage of development.

Convert designs to code with AI

Introducing Visual Copilot: A new AI model to turn Figma designs to high quality code using your components.

Try Visual Copilot

README

Echidna: A Fast Smart Contract Fuzzer

Echidna is a weird creature that eats bugs and is highly electrosensitive (with apologies to Jacob Stanley)

More seriously, Echidna is a Haskell program designed for fuzzing/property-based testing of Ethereum smart contracts. It uses sophisticated grammar-based fuzzing campaigns based on a contract ABI to falsify user-defined predicates or Solidity assertions. We designed Echidna with modularity in mind, so it can be easily extended to include new mutations or test specific contracts in specific cases.

Features

Generates inputs tailored to your actual code
Optional corpus collection, mutation and coverage guidance to find deeper bugs
Powered by Slither to extract useful information before the fuzzing campaign
Source code integration to identify which lines are covered after the fuzzing campaign
Interactive terminal UI, text-only or JSON output
Automatic test case minimization for quick triage
Seamless integration into the development workflow
Maximum gas usage reporting of the fuzzing campaign
Support for a complex contract initialization with Etheno and Truffle

.. and a beautiful high-resolution handcrafted logo.

Usage

Executing the test runner

The core Echidna functionality is an executable called echidna, which takes a contract and a list of invariants (properties that should always remain true) as input. For each invariant, it generates random sequences of calls to the contract and checks if the invariant holds. If it can find some way to falsify the invariant, it prints the call sequence that does so. If it can't, you have some assurance the contract is safe.

Writing invariants

Invariants are expressed as Solidity functions with names that begin with echidna_, have no arguments, and return a boolean. For example, if you have some balance variable that should never go below 20, you can write an extra function in your contract like this one:

function echidna_check_balance() public returns (bool) {
    return(balance >= 20);
}

To check these invariants, run:

$ echidna myContract.sol

An example contract with tests can be found tests/solidity/basic/flags.sol. To run it, you should execute:

$ echidna tests/solidity/basic/flags.sol

Echidna should find a call sequence that falsifies echidna_sometimesfalse and should be unable to find a falsifying input for echidna_alwaystrue.

Collecting and visualizing coverage

After finishing a campaign, Echidna can save a coverage maximizing corpus in a special directory specified with the corpusDir config option. This directory will contain two entries: (1) a directory named coverage with JSON files that can be replayed by Echidna and (2) a plain-text file named covered.txt, a copy of the source code with coverage annotations.

If you run tests/solidity/basic/flags.sol example, Echidna will save a few files serialized transactions in the coverage directory and a covered.$(date +%s).txt file with the following lines:

*r  |  function set0(int val) public returns (bool){
*   |    if (val % 100 == 0)
*   |      flag0 = false;
  }

*r  |  function set1(int val) public returns (bool){
*   |    if (val % 10 == 0 && !flag0)
*   |      flag1 = false;
  }

Our tool signals each execution trace in the corpus with the following "line marker":

* if an execution ended with a STOP
r if an execution ended with a REVERT
o if an execution ended with an out-of-gas error
e if an execution ended with any other error (zero division, assertion failure, etc)

Support for smart contract build systems

Echidna can test contracts compiled with different smart contract build systems, including Truffle or hardhat using crytic-compile. To invoke echidna with the current compilation framework, use echidna ..

On top of that, Echidna supports two modes of testing complex contracts. Firstly, one can describe an initialization procedure with Truffle and Etheno and use that as the base state for Echidna. Secondly, Echidna can call into any contract with a known ABI by passing in the corresponding Solidity source in the CLI. Use allContracts: true in your config to turn this on.

Crash course on Echidna

Our Building Secure Smart Contracts repository contains a crash course on Echidna, including examples, lessons and exercises.

Using Echidna in a GitHub Actions workflow

There is an Echidna action which can be used to run echidna as part of a GitHub Actions workflow. Please refer to the crytic/echidna-action repository for usage instructions and examples.

Configuration options

Echidna's CLI can be used to choose the contract to test and load a configuration file.

$ echidna contract.sol --contract TEST --config config.yaml

The configuration file allows users to choose EVM and test generation parameters. An example of a complete and annotated config file with the default options can be found at tests/solidity/basic/default.yaml. More detailed documentation on the configuration options is available in our wiki.

Echidna supports three different output drivers. There is the default text driver, a json driver, and a none driver, which should suppress all stdout output. The JSON driver reports the overall campaign as follows.

Campaign = {
  "success"      : bool,
  "error"        : string?,
  "tests"        : [Test],
  "seed"         : number,
  "coverage"     : Coverage,
  "gas_info"     : [GasInfo]
}
Test = {
  "contract"     : string,
  "name"         : string,
  "status"       : string,
  "error"        : string?,
  "testType"     : string,
  "transactions" : [Transaction]?
}
Transaction = {
  "contract"     : string,
  "function"     : string,
  "arguments"    : [string]?,
  "gas"          : number,
  "gasprice"     : number
}

Coverage is a dict describing certain coverage-increasing calls. Each GasInfo entry is a tuple that describes how maximal gas usage was achieved, and is also not too important. These interfaces are subject to change to be slightly more user-friendly at a later date. testType will either be property or assertion, and status always takes on either fuzzing, shrinking, solved, passed, or error.

Debugging Performance Problems

One way to diagnose Echidna's performance issues is to run echidna with profiling on. To run Echidna with basic profiling, add +RTS -p -s to your original echidna command:

$ nix develop # alternatively nix-shell
$ cabal --enable-profiling run echidna -- ... +RTS -p -s
$ less echidna.prof

This produces a report file (echidna.prof), that shows which functions take up the most CPU and memory usage.

If the basic profiling doesn't help, you can use more advanced profiling techniques.

Common causes for performance issues that we observed:

Costly functions called in hot paths
Lazy data constructors that accumulate thunks
Inefficient data structures used in hot paths

Checking for these is a good place to start. If you suspect some computation is too lazy and leaks memory, you can use force from Control.DeepSeq to make sure it gets evaluated.

Limitations and known issues

EVM emulation and testing are hard. Echidna has some limitations in the latest release. Some of these are inherited from hevm while some are results from design/performance decisions or simply bugs in our code. We list them here including their corresponding issue and the status ("wont fix", "on hold", "in review", "fixed"). Issues that are "fixed" are expected to be included in the next Echidna release.

Description	Issue	Status
Vyper support is limited	#652	wont fix
Limited library support for testing	#651	wont fix

Installation

Precompiled binaries

Before starting, make sure Slither is installed (pip3 install slither-analyzer --user). If you want to quickly test Echidna in Linux or MacOS, we provide statically linked Linux binaries built on Ubuntu and mostly static MacOS binaries on our releases page. You can also grab the same type of binaries from our CI pipeline, just click the commit to find binaries for Linux or MacOS.

Homebrew (macOS / Linux)

If you have Homebrew installed on your Mac or Linux machine, you can install Echidna and all of its dependencies (Slither, crytic-compile) by running brew install echidna.

You can also compile and install the latest master branch code by running brew install --HEAD echidna

You can get further information in the echidna Homebrew Formula page. The formula itself is maintained as part of the homebrew-core repository

Docker container

If you prefer to use a pre-built Docker container, check out our docker package, which is auto-built via GitHub Actions. The echidna container is based on ubuntu:focal and it is meant to be a small yet flexible enough image to use Echidna on. It provides a pre-built version of echidna, as well as slither, crytic-compile, solc-select and nvm under 200 MB.

Note that the container images currently only build on x86 systems. Running them on ARM devices, such as Mac M1 systems, is not recommended due to the performance loss incurred by the CPU emulation.

Different tags are available for the Docker container image:

Tag	Build in tag
`vx.y.z`	Build corresponding to release `vx.y.z`
`latest`	Latest Echidna tagged release.
`edge`	Most recent commit on the default branch.
`testing-foo`	Testing build based on the `foo` branch.

To run the container with the latest Echidna version interactively, you can use something like the following command. It will map the current directory as /src inside the container, and give you a shell where you can use echidna:

$ docker run --rm -it -v `pwd`:/src ghcr.io/crytic/echidna/echidna

Otherwise, if you want to locally build the latest version of Echidna, we recommend using Docker. From within a clone of this repository, run the following command to build the Docker container image:

$ docker build -t echidna -f docker/Dockerfile --target final-ubuntu .

Then, you can run the echidna image locally. For example, to install solc 0.5.7 and check tests/solidity/basic/flags.sol, you can run:

$ docker run -it -v `pwd`:/src echidna bash -c "solc-select install 0.5.7 && solc-select use 0.5.7 && echidna /src/tests/solidity/basic/flags.sol"

Building using Stack

If you'd prefer to build from source, use Stack. stack install should build and compile echidna in ~/.local/bin. You will need to link against libreadline and libsecp256k1 (built with recovery enabled), which should be installed with the package manager of your choosing. You also need to install the latest release of libff. Refer to our CI tests for guidance.

Some Linux distributions do not ship static libraries for certain things that Haskell needs, e.g. Arch Linux, which will cause stack build to fail with linking errors because we use the -static flag. In that case, use --flag echidna:-static to produce a dynamically linked binary.

If you're getting errors building related to linking, try tinkering with --extra-include-dirs and --extra-lib-dirs.

Building using Nix (works natively on Apple M1 systems)

Nix users can install the latest Echidna with:

$ nix-env -i -f https://github.com/crytic/echidna/tarball/master

With flakes enabled, you can run Echidna straight from this repo:

$ nix run github:crytic/echidna # master
$ nix run github:crytic/echidna/v2.1.1 # specific ref (tag/branch/commit)

To build a standalone release for non-Nix macOS systems, the following will build Echidna in a mostly static binary. This can also be used on Linux systems to produce a fully static binary.

$ nix build .#echidna-redistributable

Nix will automatically install all the dependencies required for development including crytic-compile and solc. A quick way to start developing Echidna:

$ git clone https://github.com/crytic/echidna
$ cd echidna
$ nix develop # alternatively nix-shell
[nix-shell]$ cabal run echidna
[nix-shell]$ cabal run tests
[nix-shell]$ cabal new-repl

Public use of Echidna

Property testing suites

This is a partial list of smart contracts projects that use Echidna for testing:

Security reviews

The following shows public security reviews that used Echidna to uncover vulnerabilities

Trophies

The following security vulnerabilities were found by Echidna. If you found a security vulnerability using our tool, please submit a PR with the relevant information.

Project	Vulnerability	Date
0x Protocol	If an order cannot be filled, then it cannot be canceled	Oct 2019
0x Protocol	If an order can be partially filled with zero, then it can be partially filled with one token	Oct 2019
0x Protocol	The cobbdouglas function does not revert when valid input parameters are used	Oct 2019
Balancer Core	An attacker cannot steal assets from a public pool	Jan 2020
Balancer Core	An attacker cannot generate free pool tokens with joinPool	Jan 2020
Balancer Core	Calling joinPool-exitPool does not lead to free pool tokens	Jan 2020
Balancer Core	Calling exitswapExternAmountOut does not lead to free assets	Jan 2020
Liquity Dollar	Closing troves require to hold the full amount of LUSD minted	Dec 2020
Liquity Dollar	Troves can be improperly removed	Dec 2020
Liquity Dollar	Initial redeem can revert unexpectedly	Dec 2020
Liquity Dollar	Redeem without redemptions might still return success	Dec 2020
Origin Dollar	Users are allowed to transfer more tokens that they have	Nov 2020
Origin Dollar	User balances can be larger than total supply	Nov 2020
Yield Protocol	Arithmetic computation for buying and selling tokens is imprecise	Aug 2020

Research

We can also use Echidna to reproduce research examples from smart contract fuzzing papers to show how quickly it can find the solution. All of these can be solved, in a few seconds to one or two minutes on a laptop computer.

Source	Code
Using automatic analysis tools with MakerDAO contracts	SimpleDSChief
Integer precision bug in Sigma Prime	VerifyFunWithNumbers
Learning to Fuzz from Symbolic Execution with Application to Smart Contracts	Crowdsale
Harvey: A Greybox Fuzzer for Smart Contracts	Foo, Baz

Academic Publications

Paper Title	Venue	Publication Date
echidna-parade: Diverse multicore smart contract fuzzing	ISSTA 2021	July 2021
Echidna: Effective, usable, and fast fuzzing for smart contracts	ISSTA 2020	July 2020
Echidna: A Practical Smart Contract Fuzzer	FC 2020	Feb 2020

If you are using Echidna for academic work, consider applying to the Crytic $10k Research Prize.

Getting help

Feel free to stop by our #ethereum slack channel in Empire Hacking for help using or extending Echidna.

Get started by reviewing these simple Echidna invariants
Considering emailing the Echidna development team directly for more detailed questions

License

Echidna is licensed and distributed under the AGPLv3 license.

Top Related Projects

Convert designs to code with AI

Introducing Visual Copilot: A new AI model to turn Figma designs to high quality code using your components.

Try Visual Copilot