RFC: Echidna 2.0

[ggrieco-tob]

The next major release of Echidna should allows us to go beyond property testing for smart contracts and see through their code when it fails. In particular, we want a tool that is able to run:

1. Ordinary property tests (e.g. boolean).
2. Assertion tests, either with failed assertions or using events (e.g. AssertionFailure(...)) in any contract and even if the execution reverts.
3. If solc 0.8.x or greater is used, automatic detection of integer overflows, zero division, invalid casts, and others.
4. Value optimization tests, where there is a function that computes a value (int256) and Echidna tries to find a maximum.
5. Other useful tests like the detection of contract destruction (which usually should trigger failures in other tests).

If no test is selected, Echidna should run in exploration mode, where coverage feedback allows our tool to reach deep lines of the contracts.

On top of that, we want Echidna to show us valuable information regarding why the test is failing and what is the state of the contract before and after it failed. That's is why Echidna will show:

1. The cause that triggers a failure in a property or assertion (e.g. a revert in a property test). This allows auditors to quickly detect unexpected failures in properties.
2. The list of events collected during the sequence of transactions that leads to a test to fail (or that provides the maximum value of a certain function if optimization is used). This allows auditors to print any state variable or computation just using events.

This new release also features a simplified interface, using a "test mode" to specify what type of tests you want. For instance, we offer two examples:

1. To test assertions and enables the automatic detection of integer overflows (if solc 0.8.x is used):

echidna-test contract.sol --test-mode assertion 

2. To run an value optimization and find the max in some polynomial:

echidna-test poly.sol --test-mode optimization 

This change enables the removal of the usage of checkAssertion, benchmarkMode or any boolean setting that indicates the testing mode.

The code in this PR is very unstable and it is NOT ready for testing yet.

[rmi7]

Here is an idea i had, maybe it makes sense, maybe it doesn't 🤷‍♂️

Instead of having to manually create valid values using a modulo, or returning early if a value is too low or high, it would be nice if you could specify valid ranges for values.

Pretty much all of the important args to functions in smart contracts are (arrays of) integers. So the below only applies to (u)int and arrays of (u)int).

If you use a modulo to generate valid values then you (1) have to write all the modulo code and (2) echidna will report the original function arg inputs when it finds a violation (instead of the value after the modulo). However, with the proposed changes in this PR you could emit an event to tell you the actual value used, still a bit cumbersome.

If you don't use a modulo but do something like this on the first line of the function if (arg1 > MY_MAX_ALLOWED_UINT) return; , then echidna will waste time on returning here (so don't do it). But if it finds a violation the input params it reports are the actual values.

So how about this

//@echidna amount: <1-10000000000>, fee: <1,10,100>, distribution: <[33,33,34], [25, 50, 25], [10-20, 10-20, 10-20]>
function deposit(uint amount, uint fee, uint[3] memory distribution, bytes data) public {
  // ...
}

• The values of each arg should always be specified inside < and > , lets call the value within these the selector
• Each item in a selector is either an rvalue (=range value) or an array
• An array can only contain rvalues
• An rvalue is either (1) an integer, or a (2) range B-C where B and C can only be integers (and it's inclusive).

I think having such syntax would eliminate a lot of code using modulo to get valid values, be more explicit, and would generally simplify using echidna.

Let me know what you think 🙂

[wuestholz]

@ggrieco-tob asked me to expand on my feedback in #682 here.

Apparently, Echidna currently does not report multiple assertion violations if they are in the same function. This behavior was a bit unexpected for me since most fuzzers will simply accumulate all the crashes until they hit the time limit. I understand that it is important to report violations as soon as they are found. However, that does not necessarily mean that the fuzzer needs to stop. The current design seems to be motivated by the expectation that developers would fix the violation and restart the fuzzer afterwards. However, for audits and long-running campaigns (say 24h or more) it's much more difficult to "fix" the code. It might therefore be useful to support this use case through a separate option.

I had originally tried to use stopOnFail: false to disable this behavior, but this option seems to concern the first violation of the entire campaign. Maybe one could consider replacing stopOnFail with two options maxFails : <int> and maxFailsPerFunction: <int> to make the behavior more explicit.

[montyly]

Regarding The list of events collected during the transaction that trigger a test failure (or that provides the maximum value of a certain function if optimization is used). This allows users to print any state variable or computation just using events, Echidna only prints the event in the property, but we could extend this to print all the events of the transactions

[naszam]

Hi @ggrieco-tob,
I think would also be nice to have an execution count number along with the * when the fuzzing is interrupted, in the coverage text file to have a better understanding of the covered code and overall reachability.

[ggrieco-tob]

Superseded by #716