Here are some useful tricks for getting the best out of Echidna.

Echidna is a fuzzing tool for smart contracts written in Solidity. Solidity smart contracts primarily work on the Ethereum blockchain. Some smart contracts are responsible for managing large amounts of cryptocurrency. With Echidna you can evaluate the security of smart contracts.

Compared to code scanners and formal methods, Echidna is good at finding transactions that can trigger unintended behavior in smart contracts. Since Echidna is a coverage-guided fuzzer, it’s also good at finding ways to hit the entire code surface of a smart contract.

To test a smart contract with Echidna, you have to define a testing interface that it can to interact with your contract under test. This interfaces contains either assertions or properties. You can select which kind of test Echidna should perform using the command line flag --test-mode.

Configuration options

Echidna has a lot of configuration options. Here are some options that I recently used when going through the Building Secure Contracts Echidna tutorial:

testMode: When working through the tutorials, I’ve only ever used property or assertion.
deployer and sender: Set these to the same value to ensure that the same account makes all transactions. deployer takes a single address, sender accepts a list of strings.
cryticArgs: Set ["--solc-remaps", "prefix=target"] if you have dependencies somewhere else. Example: @openzeppelin=../node_modules/@openzeppelin if your Node.js modules are in the parent directory.
balanceContract: Give this some Ether so that the contract under test can deploy and fund other contracts.
balanceAddr: Give deployer and sender Ether using this setting.
shrinkLimit: Shrinking stops too early? Set the limit to a higher number than the default 5000.
testLimit: Tests stop too early? Add more iterations using this setting.

Here’s how it can look like when you combine some of these settings:

# Give both the Test contract, as well as the sender 100 Wei
balanceContract: 100
balanceAddr: 100
# Run in assertion mode
testMode: assertion
# Let Echidna interact with the public interfaces of all contracts
allContracts: true
# You can leave out leading zeros in addresses
# This address deploys your contract
deployer: "0x30000"
# These addresses interact with your contracts
sender:
  - "0x10000"
  - "0x20000"
  - "0x30000"
# Don't let Echidna send Ether to the test contract
filterBlackList: true
filterFunctions:
  - "Test.fallback()"
cryticArgs:
  - "--solc-remaps"
  - "@openzeppelin=../node_modules/@openzeppelin"
# Run 20 workers in parallel. Adjust to the number of CPU cores
workers: 20
# Attempt to shrink an interesting case 10,000 times
shrinkLimit: 10000
# Run 1 million tests
testLimit: 1000000

When you create your configuration file, you can tell Echidna to use it with the --config command line flag. Here’s how to run Echidna using the configuration file echidna.yaml.

echidna --config echidna.yaml --contract Test test.sol

This assumes your test contract is called Test and is in a file called test.sol:

Echidna tricks

Configuration options

Resources

Tags