Support for relevant aspects of ecrecover

[suhabe]

trafficstars

Can solc-verify handle the ecrecover function?

For example, how I can write annotations that specify that this function returns the recovered address if the signature components are valid and otherwise reverts?

pragma solidity 0.5.0;
contract ecrecover00 {
    function execute(bytes32 hash, uint8 sigV, bytes32 sigR, bytes32 sigS) 
                               pure external returns(address) {
        address recovered = ecrecover(hash, sigV, sigR, sigS);
        require(recovered > address(0));
        return recovered;
    }
}

[dddejan]

The ecrecover function is currently treated as uninterpreted so there is no meaning attached to it's computation (see, e.g., example).

It is unlikely that we will ever be able to reason about very specific properties such as "signature components are valid" in a generic way. Automated reasoning tools have serious limitations when it comes to reasoning efficiently about cryptographic functions.

To properly support ecrecover property like this, we'd have to extend our spec language with a dedicated predicate ecvalid(...) and manually encode its properties. This is something we are thinking about but it might take a while.