Effective, Usable and Fast: Echidna, a Smart Contract Fuzzing Tool

Smart contracts are nothing new anymore. They’ve been around for a long time and we all know how they work. However, it is to be noted that hackers can’t seem to get enough of them! The number of hacks surrounding smart contracts has only risen in recent years and we’ve all witnessed the consequences.

In case you’re not aware, smart contracts are nothing but computer programs that, once triggered, do your job for you and make life easier! But for a computer program to not have any bugs and errors sounds downright fictitious.

So, what do you do to minimize the chances of your smart contract being struck by an asteroid-sized hack? You fuzz it!

Not sure what we mean? We’ve got you covered.

Fuzz testing or Fuzzing is the art of automatic bug detection. It is a Black Box software testing technique, which consists of finding implementation bugs using malformed/ semi-malformed data injection in an automated fashion. The aim of implementing fuzzing is to stress the application and cause unexpected behavior, resource leaks, or crashes.

We have talked in detail about Smart Contract Fuzzing in the past.

In today’s blog, we’re talking about a smart contract fuzzing tool that is popularly used by testers and auditors. The tool we’re talking about is Echidna! Let’s begin.

An Introduction to Echidna

Table of Contents

1 An Introduction to Echidna
- 1.1 Features of Echidna
2 Fuzzing with Echidna
3 Testing a Property with Echidna
4 Echidna for Smart Contract Build Systems
- 4.1 Limitations and Known Issues

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.

It is a tool designed for testing more complex Ethereum smart contracts. It has features such as:

Optional corpus collection, mutation, and coverage guidance to find deeper bugs.
Automatic test case minimization for quick triage.
Maximum gas usage reporting of the fuzzing campaign.

Features of Echidna

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.
Curses-based retro 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.

Fuzzing with Echidna

Echidna belongs to a specific family of fuzzer: property-based fuzzing heavily inspired by QuickCheck. In contrast to a classic fuzzer that will try to find crashes, Echidna will try to break user-defined invariants.

In smart contracts, invariants are Solidity functions, that can represent any incorrect or invalid state that the contract can reach, including:

Incorrect access control: the attacker became the owner of the contract.
Incorrect state machine: the tokens can be transferred while the contract is paused.
Incorrect arithmetic: the user can underflow its balance and get unlimited free tokens.

Testing a Property with Echidna

We will now see how to test a smart contract with Echidna. The target is the following smart contract:

In the particular contract, we’ve assumed that:

Anyone can have a maximum of 1000 tokens
The token cannot be transferred (it is not an ERC20 token)

Additional Resource:

What is a Smart Contract Seurity Audit

Write a Property

Echidna properties are Solidity functions. A property must:

Have no argument
Return true if it is successful
Have its name starting with echidna

Echidna will:

Automatically generate arbitrary transactions to test the property.
Report any transactions leading the property to return false or throw an error.
Discard side effects when calling a property (i.e. if the property changes a state variable, it is discarded after the test).

The following property checks that the caller has no more than 1000 tokens.

Initiate a Contract

Echidna needs a constructor without argument. If your contract needs a specific initialization, you need to do it in the constructor.

There are some specific addresses in Echidna:

0x00a329c0648769A73afAc7F9381E08FB43dBEA72 which calls the constructor.
0x10000, 0x20000, and 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 which randomly call the other functions

Run Echidna

The core Echidna functionality is an executable called echidna-test. echidna-test 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.

Echidna is launched with:

$ echidna-test contract.sol

If contract.sol contains multiple contracts, you can specify the target:

$ echidna-test contract.sol –contract MyContract

Upon running Echidna, the output would be as follows:

Echidna found that the property is violated if the backdoor is called.

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:

a directory named coverage with JSON files that can be replayed by Echidna
a plain-text file named covered.txt, a copy of the source code with coverage annotations.

The 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)

And that’s how it is done!

Echidna for Smart Contract Build Systems

Echidna can test contracts compiled with different smart contract build systems, including Truffle, Embark, and even Vyper, using crytic-compile.

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, the echidna can call into any contract with a known ABI by passing in the corresponding solidity source in the CLI.

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.

Limitations and Known Issues

Echidna has quite a few limitations in the latest release. Some of these are inherited from hevm while some are results from design/performance decisions or simply bugs in the code.

The issues are listed as follows:

Debug information can be insufficient.
Vyper support is limited.
Limited library support for testing.
If the contract is not properly linked, Echidna will crash.
Assertions are not detected in internal transactions.
Value generation can fail in multi-abi mode since the function hash is not precise enough.

With that being said, it is also to be noted that no testing/fuzzing tool out there is perfect as EVM emulation and testing is a hard nut to crack. However, Echidna is a great tool when dealing with complex smart contracts.

About Us

ImmuneBytes is a Blockchain auditing firm that employs the industry’s best tools and practices to provide a comprehensive smart contract audit. We have a team of robust and experienced security professionals who are adept at their niches and provide you with quality service. We have worked on 175+ projects spread across the world on different Blockchain frameworks with some of the industry’s top firms and we continue to unfold the decentralized movement.

We are also providing consultancy, coming up with a bug bounty platform, and also an insurance product to provide our clients with a hassle-free security product catalog. Stay tuned.

Additional Resources