ecrecover related bugs are not detected

[HarryR]

Description

It doesn't detect ecrecover failing upon invalid input

How to Reproduce

See the following piece of code:

https://gist.github.com/HarryR/cce52596ffebdff2744c5d790888015a

This was caused by a compiler bug in Solidity < 0.4.14, where the output memory area for the ecrecover call wasn't cleared, which means in the case of an invalid signature the memory may contain user-controllable input.

If the contract address is passed in as the last 20 bytes of the 32-byte stuff2hash input, then the if condition will be true and the contract will send all funds to the caller.

This was recently highlighted as a problem with the 0x contracts, see: https://samczsun.com/the-0x-vulnerability-explained/

Expected behavior

this bug should be detected

[gustavo-grieco]

Hi @HarryR

In order to detect an issue in echidna, you need to first add a property to check (e.g. a function with no arguments that returns bool). Echidna won't detect any bug (except maybe self-destruction) if you don't add a property to check.

[HarryR]

Hi

Yes, I am aware.

In the code I tested Echidna with I added a storage variable hacked which defaults to false. In the body of the if condition I set it to true. This must be compiled with Solidity 0.4.13, however the 0x contracts may also be used as an example.

Then I added an echidna_... method which verifies the contract invariant hacked==false etc.

The above issue is just a copy-paste that I used to submit to a bunch of different projects at the same time, I have tested each with variants of the above example which are specific to that project which should be detected but aren't.

[HarryR]

for your reference, the code I used with echidna is:

pragma solidity 0.4.13;

contract EcRecoverExample
{
	bool hacked = false;

    function example(bytes stuff2hash, uint8 v, bytes32 r, bytes32 s)
        public payable
    {
        address result = ecrecover(keccak256(stuff2hash), v, r, s);
        if( result == address(this) ) {
		hacked = true;
	}
    }

    function echidna_nothacked() public returns (bool) {
	return hacked == false;
    }
}

[gustavo-grieco]

So any stuff2hash values where last 20 bytes are equal to address(this) will work? The v, r and s values are irrelevant?

[HarryR]

Yes

[gustavo-grieco]

I have some ideas to deal with something like this but let me discuss them internally first. Thanks a lot for testing Echidna and produce a small example!

[gustavo-grieco]

This bug is too old to make sense to add specific code.