Fuzzing
smart-contracts practical aspects: Echidna

In this article, we will review the practical fuzzing of smart contracts and aim to perform two different types of analyses. Our goal is to illustrate what the fuzzing of real-life protocols entails. Our plan involves mentioning vital options in the Echidna configuration, discussing the tweaks that allow for faster fuzzing and addressing the corresponding challenges.

The challenge with comprehensive articles on fuzzing is in the vast number of possible tests and the computational resources required for each test. It encompasses aspects such as configuration, invariants, and test structure, which can be approached in many ways. The quest to find the most efficient method to cover multiple cases can be complex.

We will not delve into the basics of fuzzing testing, as it's already extensively covered in various articles. So, without further ado, let's proceed.

The easiest way to use Echidna is to take the precompiled binary from one of the last releases of Echidna here (we use current release: 2.2.2 and a direct download link of echidna executable is here). Alternatively, you can build it form the sources. In addition, we recommend using a powerful configuration with many CPU cores as the fuzzing process can benefit greatly from parallelization.

With a high probability, you will use Echidna with different contracts, each requiring different versions of the Solidity complier solc. To simplify the switch between different versions of the solc compiler, it's very handy to use the solc-select tool. Install it to easily switch to the needed version of solc with a simple command like solc-select use 0.8.0. Check your current version by running solc --version and switch to the correct one.

Echidna uses HEVM - a symbolic execution for EVM. Some of its features are extremely useful for testing. It enables you to test your contracts at specific blocks, mock the timestamp, and modify storage values. While HEVM doesn't have a lot of features, each of them are extremely powerful for testing purposes.

Echidna allows to analyze not only local contracts by compiling them, but also to use the existing ones, simply connecting to any of the existing networks, and fetch the contract data and storage directly from the blockchain. It's super handy for us as we plan to engage with different existing ERC20 tokens and DeFi protocols, interacting with them using the real chain state, skipping pre-initialization and deployments.

To access the on-chain data, Echidna requires access to the Ethereum RPC node. This access is particularly intensive, especially if you plan to perform numerous fuzzing tests. So, be careful, you can encounter situations where Echidna fires errors in log like:

but continues to perform the test with zero results. These errors can occur only after some time, when you reach the rate-limit on some public RPC node. Therefore, to perform as many fuzzing tests as you need, you should have a good RPC endpoint (preferably your own node) that is able to handle a lot of requests.

The important part of working with Echidna is configuring the tests. Many tests are very heavy, require tuning the number of testing sequences, depth of the analysis, filtering the functions being fuzzed, etc… Also, tests need many preliminary tweaks like starting balances, sender addresses, gas and gas price, etc.

In practice, you will spend a lot of time configuring Echidna for your tests, so it's beneficial to review all the options and their descriptions before getting started. The first thing to read is default.yaml (link to current version) to learn about all the available possibilities. We'll describe some of them because many of parameters don't have a clear explanation in the documentation.

Echidna offers various testing modes, and when testing real protocols, selecting the right mode and test configuration is critical, many cases are entirely unreachable because complex scenarios require hours to be tested and don't guarantee the result. You should remember that a function call or interaction with the contracts (especially those that change the state) can make the analyses too heavy.

In this article, we will use only two different testing modes: property and optimization. The first mode allows us to find a combination of input parameters that "breaks" out the invariant function. The second mode allows us to find input parameters that lead to the maximum value of our "invariant" function. There are other modes, for example, a very useful assertion that makes it possible to avoid writing any special functions. Simply add assert() to your code and try to reach this assertion with Echidna.

In order to demonstrate different fuzzing scenarios, we created an educational repo already containing the echidna binary (version 2.2.2) in the bin folder and two separate test cases in dirs fuzzing-test-1 and fuzzing-test-2. For educational purposes, simplicity and ability to copy, modify and experiment with examples, we prioritize functionality over code aesthetics, so forgive us for the lack of code beauty. :)

Each testcase (first in the fuzzing-test-1 folder) consists of two main files:

• fuzzing-test-*.sol, containing the contract interacting with our target (as we plan to test the interaction with external contracts, not only our own contracts)
• fuzzing-test-*.yaml, an Echidna configuration file for this test

To run this test case, you can use either our echidna binary or your own. The commands to run the first test from the educational repository are as follows:

[NOTE] The last option --format text is used to avoid the problems with colors in the terminal (in case you run Echidna in terminals without color support).

The second test case runs using similar commands, but utilizes another configuration file and different Solidity sources.

Let's examine the first testcase, where we interact with an existing WETH contract in the Sepolia testnet. However, we only perform simple operations, demonstrating Echidna's ability to identify "special" values leading to broken invariants, declared as the echidna_secret_fee_not_taken() function in fuzzing-test-1.sol , we also demonstrate its ability to work with existing contracts like WETH.

The structure of the test is very simple:

• we take the user's ETH sent to our contract here
• we take a secret value from the parameters, and, if this secret possesses certain mathematic properties (such as residing within a certain range or something else), we take a fee from the user's ETH before the swap occurs. The variants of analyzing the secret value are available here
• we swap the user's ETH (subtracting the fee, which can be zero) to WETH here

The goal of Echidna is to find the value of the secret that breaks the invariant here that returns true only if the fee is zero. Here, the search for the secret is simplified, but in real-life scenarios, this process can include the calculation of fees and rewards. Echidna can assist in finding corner cases, when the algorithm calculates the fees/rewards incorrectly, potentially affecting the returns for users or protocols.

Take a look at some important options in:

• seqLen: 1 - it tells Echidna to perform only one call to the contract and not attempt to use sequences of calls. They are extremely useful when testing combination of calls, like "deposit()" followed by "withdraw()"; however, in this case, only one call is needed.
• workers: 15 - don't forget to tune this parameter according to your server parameters, enabling Echidna to create more parallel processes that perform the fuzzing. This adjustment can save a lot of time
• testLimit: 1000000 - one of the most frequently used parameters is the number of iterations. In many cases you will change this parameter, increasing the duration of the test in an attempt to achieve meaningful results

Let's try to run our first test case by uncommenting the CASE 1 line. This is an easy task, and Echidna finds us the value of the secret that breaks our invariant:

The same case is present in CASE 4 with the sqrt() function. If you increase the needed sqrt() value, Echidna will not find the corresponding value.

Here comes the next requirement for test preparation. We can restrict our secret value in the test by using something like require(secret > 7500 && secret < 8000); at the start of the function (and using the condition if (sqrt(secret) == 87) // secret =~ 7569). By adding such restriction, we out a lot of non-useful secret values and save testing iterations. In this case Echidna easily finds us some value, that gives us sqrt(secret) == 87:

The second case is much more complex. As mentioned, our goal is to test real protocols and real-world scenarios. The plan for this part is to explore an extremely interesting type of Echidna fuzzing: optimization. This type of analysis allows to maximize certain parameters (i.e., profit) by testing different combinations of input parameters. Such analysis can provide security auditors with the ability to detect not only invariant breaks, but also the vulnerabilities that could allow an attacker to receive abnormal amounts of rewards, even is the overall logic of the contract is not compromised (such as minting incorrect amounts of rewards, fees, etc.)

In our case, we will test the Uniswap V3 swap pool, aiming to find the range of ticks to allocate liquidity that will maximize profit (in case when we perform some predefined swaps). In Uniswap V3, liquidity should be assigned to a specific price range, and the amount of collected fees depends on the number of swaps and the movement of the swap price between the price ticks. So, we plan to allocate the liquidity, perform some swaps, collect the fees and try to maximize them using Echidna's optimization mode.

[NOTE] Don't be too critical about the quality of the testing code, it's the product of tons of changes made in attempts to achieve optimal performance and demonstrate a real-world scenario. Experimentation with various testing parameters is necessary to achieve this. Remember to expect this complexity when testing any real-life protocol. Fuzzing is not difficult, but does require a lot of experimentation, preliminary testing and time.

Let's describe some steps in fuzzing-test-2.sol more thoroughly:

• prepare some balances of WETH and DAI
— ◦ take 100 ETH, swap them to WETH, then swap half to DAI here
• add liquidity to the WETH/DAI pool (half of our WETH tokens and the corresponding number of DAI) here
— ◦ by calling the UniswapV3 mint() function here
— — ◦ the range of ticks is determined by the input parameter _tickDiff, and this is the parameter that Echidna tries to optimize
• perform multiple swaps (DAI->WETH, WETH->DAI, DAI->WETH) here
• put a small amount of liquidity(1) to the pool here (to make the pool recalculate the fees)
• call collect_rewards() without actual calling the pool's collect() function, simply analysing our position here. It's enough to estimate the amount of received fees, making our test lighter.

In the test, we calculate how much WETH we have placed in the liquidity of the pool. Later, in collect_rewards(), we calculate the relation between the received WETH fees and the amount of WETH that was put in the pool's liquidity. This helps us identify the most profitable range of ticks.

If we run our test in Hardhat (by uncommenting the lines with debug information import 'hardhat/console.sol', and console.log() in collect_rewards()), we receive:

• seqLen: 1 - as in the first test, we plan to test only one call, and only one function. Maybe for other cases, we may want to test a sequences of calls, but in our test, we have a strict order of operations, performed within a single function in order to reduce test complexity ("mint()", "swap()" then "collect()""). Therefore, one call in a sequence is sufficient.
• filterFunctions: ["univ3_fuzzing_test(uint24)"] - tells Echidna to test only this function, attempting to mutate only its input parameters
• testMode: "optimization" - tells Echidna to mutate input parameters, estimate the output of the echidna_optimize_returned_rewards() function and try to maximize it

Other parameters are related to the starting balances of the deployed contract, deployer, sender, and other values required to emulate on-chain logic. They are well described in the documentation.

Let's run our test with the command:

(don't forget to switch to the correct solc version)

This prevents Echidna from spending time checking nonsensical combinations of calls. Additionally, it's advisable to reduce the number of parameters being optimized and then start the fuzzing by gradually "opening" parts of the code step-by-step. Continuously check if the fuzzing process still operates on real values, avoiding testing millions of heavy "revert()"s.

Also, note that "reducing the nonsensical parameter values" can backfire when you exclude dangerous values yourself in an attempt to make the test lighter. While in real life such a parameter can be somehow be passed to the protocol. Be careful.

Let's summarize in which cases fuzzing can effectively enhance the security of your protocol. It's not a "silver bullet" because it requires careful preparation of tests; otherwise, you may simply end up with a hardware burner, spending time on useless computations. The number of possible code flows is huge, so the best usage of fuzzing is working with most interesting sequences of calls from a security point of view. The good examples where the fuzzing can be effective are:

• fuzzing separate functions, accepting many parameters, and performing computations that cannot be easily observed by an auditor (having many logical branches, depending on many values)
• fuzzing the fixed calls sequences that closely resemble real protocol usage, trying to find corner cases and dangerous parameter values
• optimizing the usual call flows, attempting to identify maximums and minimums of resulting values and detecting cases where calculations return unwanted values

As mentioned earlier, fuzzing demands extensive optimization in the code being analyzed, and it's important not to exclude "too much", as this may accidentally remove potential attack vectors.

The approach "here's the contract, billion iterations, dozens of invariants - spot the bug, please" doesn't work with fuzzing if you don't have a supercomputer.

Use fuzzing carefully, prepare to delve deep into your protocol, write lots of tests, and be patient. Be safu!