Medusa fails to break property after 10min while Echidna can break it in 1min

[aviggiano]

Hello,

I am testing both Echidna and Medusa in a lending & borrowing protocol, and Echidna found an issue where the protocol revenue is being miscalculated due to a logic error, leading to a broken invariant. The problem is that Medusa is not being able to break this invariant after a much longer time.

I understand that this might be the result of pure randomness or sheer luck, or maybe due to a low number of runs, but in any case, I decided to report it here as it might lead to an actual problem with the fuzzer.

This is the sequence that led to the bug, after shrinking:

deposit(uint256 amount)
place(uint256 amount)
pick(uint256 amount)
pick(uint256 amount)
liquidate(uint256 n, bytes32 seed)

After analyzing the coverage report, I can see that the liquidate call is always reverting, which leads me to believe that it has something to do with the random seed used to decide which positions to liquidate:

    function _getIds(
        uint256[] memory array,  
        uint256 n,
        bytes32 seed
    ) internal view returns (uint256[] memory ids) {
        ids = new uint256[](n);
        for (uint256 i = 0; i < n; i++) {
            uint256 index = uint256(keccak256(abi.encodePacked(seed, i))) %
                array.length;
            ids[i] = index;
        }
    }

Unfortunately, the codebase is not open source, and a MWE would take too long to write, but please let me know if there's more information that I can share that can be helpful in debugging this issue.

[ggrieco-tob]

Without the code, we can only speculate, but I suspect could be:

• A missing corpus mutation that is useful in this example (e.g. repeating some transactions)
• Some bug in the dictionary handling of bytes32, either causing values to be always repeated or always random.

[aviggiano]

I think I found a way to create a simplified version of the project, I'll share it soon.

[aviggiano]

Hey

Changing the code altered the behavior of the comparison...
Because of the simplifications I made, Medusa is finding the bug as fast as Echidna.

Btw, can this be related in any way to #139 (comment) ? Does an empty coverage report mean empty information about the coverage, thus worse guidance?

Anyway, I'll see if I can get the original repo to see if we can have a more accurate reproduction.

[anishnaik]

Hey @aviggiano medusa has no support for external libraries at the moment. Does the example you linked in #139 work with echidna? I don't think echidna has support for external libraries either unless you manually link it (see crytic/echidna#836)

Technically, the coverage report should never be empty. Even if we get zero coverage, we should be able to view the files and see where things reverted. If you are seeing nothing it might be a bug tbh.

But yea I think having some sort of testable PoC would be ideal

[aviggiano]

Hey @aviggiano medusa has no support for external libraries at the moment. Does the example you linked in #139 work with echidna? I don't think echidna has support for external libraries either unless you manually link it (see crytic/echidna#836)

I'm manually linking them such as this example. But I do see empty coverage for the library files, even though I know they are being hit as Medusa is finding other bugs.

Anyway I'll try to get the PoC

[ggrieco-tob]

Is this still happening?

[aviggiano]

I don't know. Maybe not. Since there have been a lot of changes, I believe it's safe to close this issue and we can reopen it if necessary