Stops fuzzing after first assertion failure (per function)?

[wuestholz]

I have been trying to run Echidna on code that contrains multiple assertions per function. It seems like Echnida stops fuzzing a function after the first violation. Is this the case?

And if so, is there an option to keep fuzzing? I have already tried setting stopOnFail: false in the yaml configuration.

I have created the following simple contract to reproduce this:

pragma solidity 0.7.6;

contract EchidnaTest {
  event AssertionFailed(string message);
  function TestMe1(uint256 a1, uint256 a2, uint256 a3, uint256 a4) public returns (uint256) {
    if (42 < a1) {
        if (1337 < a2) {
            emit AssertionFailed("2"); return 2;
        }
        emit AssertionFailed("1"); return 1;
    }
    return 0;
  }
  function TestMe2(uint256 a1, uint256 a2, uint256 a3, uint256 a4) public returns (uint256) {
    if (42 < a1) {
        if (1337 < a2) {
            assert(false); return 2;
        }
        assert(false); return 1;
    }
    return 0;
  }
}

I got the following output using Echidna 1.7.2:

assertion in TestMe2: failed!💥
  Call sequence:
    TestMe2(43,90099852,17965598210198,0)

assertion in TestMe1: failed!💥
  Call sequence:
    TestMe1(43,0,0,0)


Unique instructions: 329
Unique codehashes: 1
Corpus size: 1
Seed: 0

[ggrieco-tob]

Hi,

You are right. Echidna will stop when it hits the first assertion failed. The option stopOnFail: false is useful to stop the fuzzing campaign when you find an assertion failure (so it's not doing what you expect). We build echidna in this way because we want to find issues ASAP during a fuzzing campaign. Auditors and developers should fix the code as soon as they find an assertion failure.

As an alternative, you can let echidna to explore the contract (using benchmarkMode: true), without any particular property or assert, save the corpus (and examine coverage line by line) and then enable assertions/properties.

[wuestholz]

@ggrieco-tob Thanks a lot for the quick reply!

Just to clarify: with stopOnFail: true Echidna will stop the entire campaign as soon as it finds any violation. In contrast, with stopOnFail: false Echidna will stop fuzzing a function as soon as any violation was found within it. Is that accurate?

This behavior was a bit unexpected for me since most fuzzers will simply accumulate all the crashes until they hit the time limit. I agree that it's nice to report violations early, but for audits and long-running campaigns it's much more difficult to "fix" the code. It might be useful to support this use case through a separate option.

So, currently the process you would suggests is the following:

1. Comment out all assertions
2. Run Echidna using benchmarkMode: true and corpusDir: /foo/bar (this should run until the specified time limit)
3. Uncomment all assertions
4. Run Echidna again using benchmarkMode: false, corpusDir: /foo/bar, and a much shorter time limit (enough to rerun all the tests in the corpus)

Is that correct?

[wuestholz]

@ggrieco-tob I just tried the process I described above, but it doesn't report additional violations. These are the steps I followed:

$ mkdir current-corpus
$ printf 'testLimit: 1000000000\ntimeout: 120\ncoverage: true\nseed: 0\ncodeSize: 0xfffffff\nstopOnFail: false\nbenchmarkMode: true\ncorpusDir: current-corpus\nformat: text' > config.yaml
$ echidna-test --check-asserts --config config.yaml --contract EchidnaTest EchidnaTest.no-asserts.sol
Loaded total of 0 transactions from current-corpus/coverage
Analyzing contract: EchidnaTest.no-asserts.sol:EchidnaTest
Unique instructions: 263
Unique codehashes: 1
Corpus size: 7
Seed: 0
TIMEOUT!
$ printf 'testLimit: 1000000000\ntimeout: 120\ncoverage: true\nseed: 0\ncodeSize: 0xfffffff\nstopOnFail: false\nbenchmarkMode: false\ncorpusDir: current-corpus\nformat: text' > config.yaml
$ echidna-test --check-asserts --config config.yaml --contract EchidnaTest EchidnaTest.sol
Loaded total of 7 transactions from current-corpus/coverage
Analyzing contract: EchidnaTest.sol:EchidnaTest
assertion in TestMe2: failed!💥
  Call sequence:
    TestMe2(43,1265786331199811591399330962964836901789203661327900632764642694328,41491052894408334436837918065749096052833218613615149925072555277801,29068878132330489745547878183847730950525330373549651741743278400014624)

assertion in TestMe1: failed!💥
  Call sequence:
    TestMe1(43,0,0,0)

Unique instructions: 289
Unique codehashes: 1
Corpus size: 9
Seed: 0

Any idea what I'm doing wrong?

[ggrieco-tob]

Hi,

A few points for this discussion:

Just to clarify: with stopOnFail: true Echidna will stop the entire campaign as soon as it finds any violation. In contrast, with stopOnFail: false Echidna will stop fuzzing a function as soon as any violation was found within it. Is that accurate?

Yes, well, Echidna will always stop fuzzing a function as soon as any violation was found within it, that's how it works. When stopOnFail: true Echidna will stop the entire campaign as you said. To be more precise, when assertions are enabled, echidna will still keep executing functions with random inputs, but it won't report any additional failures.

This behavior was a bit unexpected for me since most fuzzers will simply accumulate all the crashes until they hit the time limit. I agree that it's nice to report violations early, but for audits and long-running campaigns it's much more difficult to "fix" the code. It might be useful to support this use case through a separate option.

This a useful piece of feedback. Can you please elaborate it and post it in the Echidna 2.0 RFC PR for further discussion?

Finally, in benchmarkMode: true there is no need to disabled assertion or events, they will be executed as expected, but nothing will be reported. Once you have that corpus collected, you can manually verify which assertions are reached in the corpus (inspecting the covered.txt file). If you want, you can also disable every assertion, but one, and re-run with the corpus collected, to check how an assertion failed exactly.

[wuestholz]

@ggrieco-tob Thanks a lot for the clarification! I'll try to use the covered.txt file in that case.

I have posted a summary of this discussion here: #674 (comment).