Skip to content
This repository was archived by the owner on Feb 14, 2025. It is now read-only.

echidna

Jump to bottom
Dan Guido edited this page Aug 16, 2018 · 4 revisions

Basic Echidna usage

Overview

Learning Objectives

  • Write and execute first Echidna Test
  • Read Echidna output

Tools

  • Echidna
  • IDE

Target

Lesson

Echidna uses solc and the Haskell library HEVM to compile and execute EVM bytecode. Solc exports information about public functions and the expected arguments of those functions. During testing Echidna alternates between calling functions from the contract under test and executing tests (which it identifies based on their function names, tests typically begin with echidna_).

Tests

All Echidna tests are pass/fail tests and are similar to assert() in C and other languages. If an Echidna test fails it's recorded and a best-effort minimal, complete, and verifiable test case is generated.

The skeleton of an Echidna test is

function echidna_check()public returns (bool) {
  bool condition={... generate from rest of contract ...}
  return condition;
}

Shrinking

The process of creating a minimal test is known as "shrinking". The shrinking process is only initiated once an Echidna test has failed. Echidna has no deeper understanding of the contract internals and how different components of the contract interact with each other and takes a black box approach to shrinking. When a test fails, Echidna has a function call history composed of all the function calls it's made in order and the arguments it's passed with a final failing test. Echidna will try removing function calls from the function call chain and replacing arguments with "simpler" ones while still maintaining the failure of the original test. Shrinking is an iterative process that continues until the test is as small as it can get or a predefined threshold is passed.

Exercise

Extend the contract Canal with 4 Echidna checking functions. The Echidna functions should check the values of first_gate_up and second_gate_up. Run Echidna by executing the following command inside the canal folder.

echidna-test canal.sol

Although not necessary because canal.sol only has one contract, you could also explicitly pass the name of the contract you wanted to test like so:

echidna-test canal.sol Canal

By default, echidna will only analyze the first contract it encounters.

Look at the results produced by Echidna. Are they correct? Can you modify the canal contract such that Echidna can no longer find a sequence of calls that violate one of your tests?

Echidna limitations

Overview

Learning Objectives

  • Identify types of bugs Echidna struggles with discovering

Tools

  • Echidna
  • IDE

Target

Lesson

Echidna is not guaranteed to find all bugs in a contract. Echidna struggles with several classes of functions. One such class are known as "point functions" where an "interesting" thing only happens for a very specific input. Point functions are challenging because echidna explores contracts by generating random values for arguments and the likelihood of guessing the specific combinations of inputs to trigger an effect is very small. Echidna uses different strategies to generate random data for different datatypes and some values (like 0) for integers are likely to be tested.

Another area where Echidna is not likely to find bugs is when they're only reachable after very many function calls. Echidna will only construct tests consisting of at most N function calls. Bugs gated behind N+1 calls will never be exposed. The threshold N is configurable but not dynamic and won't change during the duration of a test.

Echidna doesn't look for more than one way to fail a given test and so it's possible that there are more easily understood ways to violate an assumption that are harder for echidna to find.

Exercise

Point Function

Run Echidna on pointfunction.sol. Is it able to identify the value of secret that would cause the test to fail?

Complexity

Run Echidna on complex.sol. Does echidna find a sequence of calls that would cause the test to fail? Can you imagine some real world scenarios where a bug might be deeply nested?

Open ended

Do you know of any EVM based contracts that Echidna might struggle to analyze?

Echidna config.yaml

Overview

Learning Objectives

  • Become familiarized with Echidna config file
  • Extract additional information from Echidna
  • Hack around some of Echidna's limitations

Tools

  • Echidna
  • IDE

Target

Any and all contracts

Lesson

The config.yaml file is your point of leverage over echidna. Using a config file enables you to configure many of the parameters mentioned in previous units such as the number of chained function calls in a test or the prefix used to identify Echidna tests. You can find a full accounting of the options available in config files here.

You can pass a config.yaml file to echidna on the command line with the --config switch

echidna-test <contract.sol> --config ./arbitrary_path/config.yaml

Exercise

Coverage

Enable coverage. Echidna's coverage engine uses a genetic algorithm to try to increase code coverage. How does coverage impact the performance of Echidna? Can coverage help explore problematic point functions? If you're observing any type of coverage statistic jitter can you explain why that might be happening?

Json

Turn on json based output and run some echidna analyses. How might this form of output be useful from a systems integration standpoint?

Prefix and return

There are no hard and fast rules when it comes to what your tests must be named or how they behave if you think returning false or reverting is more intuitive than returning success you can make that the norm.

addrList

In the section on limitations we learned that Echidna uses different generation strategies for different datatypes. Without writing Haskell the only datatype we can influence is the address datatype. By specifying a list of addresses as a yaml list we can ensure that specific addresses will be more likely to turn up and perhaps uncover bugs that would remain hidden if addresses were all totally random.

Gastest

Overview

Learning Objectives

  • Leverage Echidna internals with gastest-exe to profile contract gas usage
  • Understand why there is jitter in the results produced by gastest.

Tools

  • gastest-exe
  • solc

Target

Lesson

Echidna's internals can be leveraged for more than just property testing (like we've been doing so far with echidna_ functions). gastest-exe leverages Echidna's fuzzer engine to come up with

Exercise

compare coverage data from solc --gas <contract.sol> to gastest-exe <contract.sol>.

Use gastest-exe to evaluate gas usage of a contract. You may notice significant differences in some of your tests. Can you design a series of tests to discover when solc and gastest-exe are likely to converge and diverge in their analysis?

Testing without modifying contract

Overview

Learning Objectives

  • Perform high fidelity testing
  • Use Solidity features to create an echidna test harness

Tools

  • Echidna
  • IDE

Target

Lesson

Up until this point all Echidna tests have been written inline with the rest of the contract code. Writing tests in this style is convenient but negatively impacts testing fidelity. In the ideal scenario We'll always be able to construct tests that do not modify the original contract in any way. One way to accomplish this is by leveraging the inheritance feature of the Solidity language.

Exercise

Transfer.sol

Transfer.sol:NewCoin implements a simple coin on top if Ethereum. Note the way TEST is implemented doesn't introduce any additional code into NewCoin.

Missing Constructor

There are two contracts with the missing constructor bug in the Targets section. Can you use the Inheritance technique to verify the presence of the bug without introducing code directly into the contracts?

Clone this wiki locally