Smart Contracts Testing using Fuzzing: Introduction to Echidna
What is Fuzzing?Fuzzing, or Fuzz Testing, is a technique which helps find bugs and loopholes in a software. These vulnerabilities are identified by injection of automatically generated random, unexpected, or invalid data into the software and then monitoring the behavior for potential information leakages and crashes.
Introduced in the 1990s, the fuzzing process has gained a lot of traction in the software industry for its reliability. Due to smart contracts’ immutable nature, this process becomes more essential in the context of smart contracts, especially the ones that include financial transactions and complex logic. Since they cannot be altered after deployment, it is crucial to thoroughly test their robustness before deployment. Figure 1 represents the process of Fuzzing.
Can Fuzzing really improve smart contract testing?
Fuzzing is a tried and tested method for detecting vulnerabilities within software. It has been used in testing of several software, e.g., web browsers, network protocols, and operating systems etc. Some examples of such popularly known software are Microsoft Windows, OpenSSL cryptographic library and Apache Web Server.
Figure 1: Fuzzing process for smart contracts (source)
By generating a large number of inputs, fuzzing can help identify edge cases within smart contracts that may potentially remain invisible in other testing methods. In addition to identification of potential vulnerabilities, fuzzing improves the overall quality of a smart contract by detecting errors and inconsistencies. Fixing these issues before deployment can help smart contract developers ensure the reliability and security of their code.
What are the available fuzzing tools for smart contracts?
Echinda
Amongst all the available tools, Echidna is the most famous one. It is essentially a program which is designed for fuzzing Ethereum smart contracts. It also uses contract Application Binary Interface (ABI) to test for unexpected inputs. Since it acknowledges modularity, new mutations in the contract can be tested as well. Some of the features that Echidna provides include creation of inputs customized for specific code, source code integration to identify lines which are covered after the fuzzing campaign, and reduction of test cases for quick testing.
How to use Echidna?
The first step to use Echidna is its installation. One pre-requisite for Echidna is Slither. It is recommended to install Slither in a virtual python environment. Run the following command to install Slither
pip3 install slither-analyzerAfter installing Slither, one can install Echidna using Stack, use a docker container, or use the pre-compiled binaries. For the quickest solution, we recommend using pre-compiled binaries.
Once everything is setup, Echidna can be executed on your smart contracts. In this tutorial we will use the smart contract “SimpleToken” (SimpleToken.sol) shown in Figure 2.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract SimpleToken{
mapping(address => uint) public balances;
function airdrop() public{
balances[msg.sender] = 100;
}
function consume() public{
require(balances[msg.sender] > 0);
balances[msg.sender] -= 1;
}
function secretDoor() public{
balances[msg.sender] += 1;
}
Figure 2: SimpleToken smart contractThis is a simple Solidity contract named SimpleToken that allows users to airdrop tokens to their own address, consume (or use) tokens they own, and access a function named secretDoor() which adds one token to the user's balance.
The airdrop() function allows the caller to add 100 tokens to their own balance in the balances mapping. The consume() function allows the caller to use one token from their own balance in the balances mapping. It uses a require() statement to ensure that the caller has at least one token to consume before subtracting one from their balance. The secretDoor() function allows the caller to add one token to their own balance in the balances mapping. This function does not have any restrictions or requirements on who can call it, so any address can add one token to their own balance by calling this function.
Please note that this contract is missing important security features such as access control, and it may not be suitable for use in a production environment without further modifications.
In order to use Echidna on this contract, we need to write properties (or invariants). Invariants are logical conditions or properties that are always expected to be true during the execution of a smart contract (or program /a piece of code). They are constraints that must hold true before, during, and after the execution of a smart contract. In other words, they are statements that must be true at certain points in the code, regardless of any other factors. An Echidna property is a Solidity function that has the following characteristics:
- It has no arguments.
- It returns a boolean value (i.e., true or false) indicating whether the property is satisfied.
- Its name starts with the word "echidna".
In this regard we create a property (echidna_balance_under_100()) which checks that the caller can have no more than 100 tokens. The property along with “TestSimpleToken” contract (TestSimpleToken.sol) is shown in Figure 3. Please note, it is recommended to separate smart contract code from properties.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
import "SimpleToken.sol";
contract TestSimpleToken is SimpleToken{
constructor() public {}
function echidna_balance_under_100() public view returns(bool){
return balances[msg.sender] <= 100;
}
}
Figure 3: Echidna property to check user balance always less than or equal to 100Finally, Echidna can be used with our sample contract and its property using the following command:
$ echidna-test TestSimpleToken.sol --contract TestSimpleToken
Echidna will generate random sequences to check if the defined property “echidna_balance_under_100 ()” fails or not. Lucky for us, the property fails and Echidna shows the following output as shown in Figure 4. It can be interpreted as follows – If the function airdrop() is called once, the user gets 100 tokens. As per our property (invariant) from Figure 3, the user balance should never exceed 100 tokens. However, Echidna found out that if secretDoor() is called after airdop(), the balance can exceed 100 tokens. Hence, the property failed.
……………
echidna_balance_under_100: failed!
Call sequence:
airdrop()
secretDoor()
Unique instructions: 259
Unique codehashes: 1
Corpus size: 1
Seed: 2633990180718244873
……………
Figure 4: Echidna output for TestSimpleTokenWhile the complexity of the test cases varies with the complexity of the smart contracts, yet the underlying concept of Echidna remains the same, i.e., generate random inputs, pass to the contract functions, and monitor the outputs.
Other tools that help with fuzzing
- Foundry: It is a property-based testing tool which uses mutation-based fuzzing techniques to find reasons for program crashes or its unexpected behavior. It is quite powerful since it allows definition and verification of custom correctness and safety policies.
- Hevm: It is an EVM debugger specifically created for symbolic execution, debugging of smart contracts and unit testing. It also serves as an execution engine for tool suits like dapp and fuzzers like Echidna.
- Tayt: It is a testing library which is adjusted for the analysis of smart contracts written in Cairo. It can be run on an entire project or even a small number of files to check for vulnerabilities by fuzzing the contracts through external functions.
- Solidity Fuzzing Boilerplate (SFB): It is a template repository which contains templates to fuzz the contracts with other tools like Echidna & Foundry. It helps in writing the tests and allows fuzzing of components that use incompatible versions of Solidity.
Conclusion
The brief history of smart contracts has seen some unimaginable exploitation of its vulnerabilities. Given the contract’s immutable nature, these exploitations become irrevocable. Fuzzing has a history of helping ensure software security and has hence now become an essential part of smart contract security audit as well.
About Truscova:
Truscova comes with 30+ years of academic research and hundreds of academic publications which pioneered the area of Formal Verification. The team combines academic leadership, industrial strength and Blockchain expertise. Truscova currently analyzes Solidity code combining Formal Verification techniques: abstract interpretation, constraint solving, theorem proving, and equivalence checking.