Fuzz testing with Echidna

Let’s break a smart contract in random ways

What is Fuzz testing ?

Fuzz testing is a software testing technique.

It involves inputting large amounts of random, unexpected, or malformed data into a smart contract to identify potential issues.

In this blog, we will demonstrate it using a tool called Echidna.

Echidna

Echidna is a fuzzing tool by Crytic.

Its design allows us to provide “our goal” and Echidna will try to break it with fuzz testing technique.

https://dl.acm.org/doi/pdf/10.1145/3395363.3404366

Echina example

Let’s get our hand on Echidna. For example, we will use it to solve a CTF problem called Naive receiver.

Example 1

Naive receiver is a CTF problem from damnvulnerabledefi.xyz.

The problem statement is

There’s a pool with 1000 ETH in balance, offering flash loans. It has a fixed fee of 1 ETH.

A user has deployed a contract with 10 ETH in balance. It’s capable of interacting with the pool and receiving flash loans of ETH.

Take all ETH out of the user’s contract. If possible, in a single transaction.

Let’s break it down line by line.

There’s a pool with 1000 ETH in balance, offering flash loans. It has a fixed fee of 1 ETH

From this statement, the pool offers flash loans with 1 ETH fee.

This statement is translated to code as:

This code is from V2 of damnvulnerabledefi.xyz. For the full code, follow this link.

From the code, this contract will call “receiveEther” function in the borrower contrcat.

Then 1 ETH fee will be check after the “receiveEther” function is called.

The check is a balance check to enforce the amount of fee sent to be greater than 1 ETH.

Now, let’s move to the next part of the problem statement. Which is

A user has deployed a contract with 10 ETH in balance. It’s capable of interacting with the pool and receiving flash loans of ETH.

Let’s look at its code.

From the code, this “receiveEther” function will pay the loan it receives along with the 1 ETH fee.

“FlashLoanReceiver” contract is deployed with 10 ETH for paying the fee.

Finally, the goal of this problem is:

Take all ETH out of the user’s contract. If possible, in a single transaction.

Now we will use Echidna to archive this goal.

https://dl.acm.org/doi/pdf/10.1145/3395363.3404366

As shown in its architecture, Echidna requires “system properties” as its input.

This “system properties” is how we tell Echidna to archeive our goal.

The steps to define and use this “system properties” with Echidna are as follows.

1. Define our goal in plain text.
2. Create a solidity file to setup our test environment. This file will be our “system properties”.
3. Translate our goal from plain text into the “system properties” file.

Let’s start with the first step.

1. Define our goal in plain text.

So basically, our step is to “Take all ETH out of the user’s contract (FlashLoanReceiver contract)”, this can also be found in the CTF’ test file.

2. Create our test environment.

The system property will be a solidity file to setup our test environment.

To do this, we deploy “NaiveReceiverLenderPool” and “FlashLoanReceiver”. Then we send 1,000 ETH and 10 ETH to them respectively.

This can be shown in the code snippet below. This code is from Crytic’s “damn-vulnerable-defi-echidna” Github repository.

3. Translate our goal into the “system properties” file.

Echidna document states the pattern to write “system properties” or “invariants” as

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:

So we can translate “All ETH out of the user’s contract must be taken” as

However, Echidna will tell us that it can not archeive this goal.

This is because after each round Echidna tries fuzz testing, it will reset the state value and try again with different random actions.

This means after our system properties call pool.flashLoan with a set of random argument, address(receiver).balance will be 9.

Then the state value will be reset. So, address(receiver).balance will be 10 again.

Now when Echidna tries call pool.flashLoan with a different argument, address(receiver).balance will be 9 again. So on and so on.

This means Echidna will never find a path to make address(receiver).balance == 0.

To solve this, we change our goal from “All ETH out of the user’s contract must be taken” to “ETH in user’s contract must not be taken”.

Since if one action can take a portion of ETH in user’s contract, then repeatedly calling that action may take all ETH in user’s contract.

Our new goal “ETH in user’s contract must not be taken” can be written as

Finally, Echidna gives us a way to decrease ETH in user’s contract.

So, calling pool.flashLoan(0) once will decrease receiver balance by 1.

This means calling pool.flashLoan(0) 10 times will take all ETH from receiver contract. Therefore, we now solve this problem.

Example 2

This example will also be one of the problem from damnvulnerabledefi.xyz. It is called Unstoppable.

There’s a tokenized vault with a million DVT tokens deposited. It’s offering flash loans for free.

To pass the challenge, make the vault stop offering flash loans.

You start with 10 DVT tokens in balance.

Let’s take a look at the code that represents each line of this problem.

There’s a tokenized vault with a million DVT tokens deposited. It’s offering flash loans for free.

From the flashLoan function, it lends borrowAmount to msg.sender then call receiveTokens callback function to get the loan back.

To pass the challenge, make the vault stop offering flash loans.

Now we follow the same steps to use Echidna which is.

1. Define our goal in plain text.

Our goal is to make the vault stop offering flash loans.

2. Create our test environment.

We deploy the DVT token contract along with setting up the UnstoppableLender contract as shown in code snippet below.

3. Translate our goal into the “system properties” file.

First, let’s try translating “make the vault stop offering flash loans” into the system property file.

There are 2 ways we could this.

1. Fixing the loan amount.

This tells Echidna that calling flashLoan 10 as borrowAmount value should not revert.

2. Let Echidna uses a random number for the loan amount.

This tells Echidna that calling flashLoan with random borrowAmount value should not result in implicit errors/assertion error.

However, this second approach uses a technique called assertion mode.

In this blog, the first approach is efficient enough.

Echidna will finds a way to return false, which means if revertion occurs then it will provide us a step to reproduce.

Echidna will try to call any contracts with a known ABI to archeive this goal.

However, trying to call DamnValuableToken wouldn’t do much effect since the Echidna actor does not own any tokens.

So we give it some tokens as shown below.

Now running Echidna gives us the result as:

This means if 1 DVT token is sent to the UnstoppableLender contract, later calling flashLoan will always revert.

This is because the assertion in flashLoan function that expects its token to come through depositTokens function only. This is illustrated in the code snippet below.

Therefore, sending tokens directly to the UnstoppableLender contract will make this assertion become falsy.

Summary

Fuzz testing is a powerful method for uncovering vulnerabilities in smart contracts. In this blog, we provide introductory examples of fuzz testing using Echidna.

By leveraging automated input generation, fuzz testing can help exposing edge cases and security flaws that might be missed through manual testing alone.

Appendix

Echidna requires a configuration file to perform each fuzz testing, we provide them below

“balanceContract” gives ETH balance to Echidna actor.

“multi-abi” and “allContracts” tell Echidna to call any functions if it has the ABI.

“deployer” enforces Echidna to use a specific account to deploy its actor.

“sender” enforces Echidna to enforces a specific account to help the actor contract randomly calls the target contracts we are testing.

Finally, debugging the calls from Echidna requires enabling the Corpus feature. This feature shows the execution traces as:

• * 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)

An example execution trace is shown below.

References

1. We use the problems from https://www.damnvulnerabledefi.xyz/ version 2, its source code can be found at https://github.com/tinchoabbate/damn-vulnerable-defi/tree/82b6049452c387235ee0b452b0de9f3dca88c072.

2. The solutions are mainly from https://github.com/crytic/damn-vulnerable-defi-echidna/tree/solutions.

3. For Echidna configuration document: https://github.com/crytic/echidna/wiki/Config.

4. For Echidna manual: https://github.com/crytic/echidna.

Author Detail

Nattawat Songsom, Smart Contract Auditor and Consultant.

About Valix Consulting

Valix Consulting is a blockchain and smart contract security firm offering a wide range of cybersecurity consulting services. Our specialists, combined with technical expertise, industry knowledge, and support staff, strive to deliver consistently superior quality services.

Website: https://valix.io/

For any business inquiries, please contact us via Twitter, Facebook, or info@valix.io.