Echidna Testing Modes Demystified: Choosing the Right Mode for Comprehensive Smart Contract Evaluation
In our previous blog post – “Smart Contracts Testing using Fuzzing: Introduction to Echidna”, we talked about a very
powerful testing technique – Fuzzing, Echidna tool by trail of bits designed to perform Fuzzing on Solidity smart contracts, and invariants.In this blog post we take over from where we left and further explore the Echidna tool. When it comes to testing smart contracts using the Echidna, it's essential to choose the right testing mode to ensure a comprehensive and thorough evaluation of your code. However, with several options available, it can be challenging to decide which testing mode to use. In this article, we'll discuss the various testing modes that Echidna offers and their advantages and disadvantages.
Stateful vs Stateless
When it comes to testing your smart contract with Echidna, you have the option of choosing between two testing modes: stateful and stateless. Both have their own advantages and disadvantages, so it's important to understand how they work before deciding which one to use. By default, Echidna runs in stateful mode, which means that it will keep the state between each function call and try to break the invariants (or properties). In contrast, stateless mode can be activated using the "--seqLen 1" command when running Echidna. In this mode, Echidna will discard the state changes during the fuzzing.
So, what are the differences between stateful and stateless modes? Let's take a closer look. Stateful mode is more powerful than stateless mode, as it can allow breaking invariants that only exist if the contract reaches a specific state. This means that stateful mode can potentially uncover more bugs and vulnerabilities. On the other hand, stateless tests can be easier to use than stateful tests because they benefit from simpler input generation. However, this ease of use comes at a cost: stateless tests can hide issues that depend on a sequence of operations that is not reachable in a single transaction. It's also important to note that running tests in stateless mode can be slower than in stateful mode because it forces the EVM to reset after each transaction or test. In contrast, stateful mode resets the state only after a certain number of transactions (by default, every 100 transactions).
Boolean Properties
We briefly discussed this in our previous blog post. Echidna's default mode of testing is called the "property" mode, which utilizes special functions called properties to report failures. You can use the Property testing mode when the computation of a property can be easily done using state variables (whether they are public or internal), and there is no requirement of additional parameters. But how do you write your testing functions and properties? Here are a few points to keep in mind:
- Name your testing functions with a specific prefix - "echidna_". This helps to ensure consistency and makes it easier to identify and categorize your tests.
- Your testing functions should take no parameters and always return a boolean value. This ensures that your tests are simple and straightforward, and can be easily interpreted by Echidna.
- Any side effects that occur during the execution of the property shall be reverted at the end. This ensures that your tests don't have any unintended consequences that could affect the rest of your codebase.
- Properties are considered to pass if they return true, and fail if they return false or are reverted. However, if you want to test for the opposite case (i.e. a property that fails if it returns any value, but passes if it is successfully reverted), you can use properties that start with "echidna_revert_".
function echidna_balance_under_100() public view returns(bool){
return balances[msg.sender] <= 100;
}
function echidna_revert_balance_under_100() public view returns(bool){
return balances[msg.sender] <= 100;
}
Pros and Cons
One of the key advantages of Echidna is that properties can be simpler to write and understand compared to other approaches for testing. Additionally, there is no need to worry about side-effects since they are automatically reverted at the end of the property execution.
However, there are a few disadvantages to using Echidna. For example, since the properties take no parameters, any additional input needs to be added using a state variable, which can be cumbersome in some cases. Additionally, any revert during the execution of the property is interpreted as a failure, which is not always what is expected. Furthermore, Echidna does not collect coverage data during its execution, which means that it may not be suitable for testing complex code with a non-trivial amount of branches. In such cases, other types of tests may be more appropriate.
Assertions
Echidna's "assertion" testing mode is particularly useful in this regard. It can help developers identify potential issues early on, before they become major problems. Assertions are a useful testing mode in Echidna that should be considered if your property (or invariant) is more easily expressed using function arguments or if it can only be checked in the middle of a transaction. Additionally, if your code is complex and requires checking and modifying the state, assertions can be an effective way to ensure that the expected behavior is occurring. But what exactly is an assertion and an assert violation?
Assertions are a type of programming statement that are used to verify or "assert" certain conditions in code. They are typically used to check for expected behavior, and will raise an error or exception if the condition being tested is not met. In the context of smart contract development, assertions can be used to ensure that certain conditions are met within the contract, such as verifying that a certain value is within a specified range or that a particular variable has a certain value. An assertion violation in the case of Echidna is any situation where the tool detects an issue that violates an assertion.
There are no specific naming requirements for functions that check assertions in Echidna, unlike properties. These functions are executed like any other function and will retain their side effects if they do not cause the contract to revert. This flexibility allows developers to seamlessly integrate assertion checking into their code without having to worry about naming conventions or other restrictions.
This can happen in a few different ways, including:
- If the execution reverts during a call to assert. In this case, Echidna will detect an assertion failure if it executes an assert call that fails in the first call frame of the target contract.
- If an AssertionFailed event is emitted by any contract, regardless of the number of parameters.
function testStake(uint256 toStake) public {
uint256 balance = balanceOf(msg.sender);
toStake = toStake % (balance + 1);
if (toStake < MINSTAKE) // Pre: minimal stake is required
return;
stake(msg.sender, toStake); // Action: token staking
assert(staked(msg.sender) == toStake); // Post: staking amount is toStake
assert(balanceOf(msg.sender) == balance - toStake); // Post: balance decreased
}
Pros and Cons
One of the key benefits is that it is relatively easy to implement, especially if there are multiple parameters required to compute the invariant. Additionally, coverage is collected during the test execution process, which can help developers identify new failures that may have gone unnoticed otherwise. Another advantage is that if the code already contains assertions for checking invariants, these can be reused, making the testing process more efficient. However, there are also some potential drawbacks to consider when using Echidna for invariant testing. For example, if the code being tested already uses assertions for data validation, it may not work as expected. This can create confusion and potentially lead to false positives or other issues.
Conclusion
In conclusion, Echidna is a powerful tool for testing smart contracts on the Ethereum network. It offers various testing modes, including the assertion mode and property mode, which are designed to help developers test for invariants and ensure the integrity of their smart contracts. The choice between stateless and stateful testing modes depends on the specific needs of the developer and the complexity of the contract being tested. While Echidna has its advantages and disadvantages, it is undoubtedly a useful tool for developers who want to ensure that their smart contracts are secure and reliable. By leveraging the features of Echidna, developers can save time and resources by catching potential bugs and security issues early on in the development process, ultimately leading to a more robust and secure smart contract ecosystem.
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.