Error when trying to verify a contract that uses tx.origin state variable

[jcrreis]

Hello again,

I'm trying to verify the following contract with solc-verify, but it is returning to me an error, that i guess is because this tool can't deal with tx.origin, can you confirm?

Code:

 /// @notice postcondition msg.sender == owner
    /*
        solc-verify can't deal with tx.origin state variable..
    */
    function transfer(address payable _to, uint _amount) public payable{
        require(tx.origin == owner, "Not owner");

        (bool sent, ) = _to.call{value: _amount}("");
        require(sent, "Failed to send Ether");
    }

Command:

solc-verify.py Phishingtxorigin.sol  --show-warnings

output:

Phishingtxorigin.sol:42:17: solc-verify error: Member without corresponding declaration: origin
Phishingtxorigin.sol:41:5: solc-verify warning: Errors while translating function body, will be skipped
Wallet::[constructor]: OK
Attack::[constructor]: OK
Attack::attack: OK
Wallet::transfer: SKIPPED
No errors found.

Also i get errors when using Selfdestruct and delegatecall solidity functions, all these functions were available in 0.7.*, so i'm confused why this tool can't deal with them..

Can you help me on this @hajduakos ? Thank you.

[jcrreis]

Also I'd like to have another question answered if you don't mind... I could actually catch reentrancy in solidity 0.8.* versions, however it doesn't seem to work with transfer() and send() methods, as it always says the invariant might not hold..

/// @notice invariant __verifier_sum_uint(balances) <= address(this).balance
contract Reentrancy is ReentrancyGuard{

    mapping(address =>  uint) balances;

    function deposit() public payable {
        balances[msg.sender] += msg.value;
    }

    function withdraw(uint amount) public {
        require(balances[msg.sender] >= amount, "Insuficient Funds");

        balances[msg.sender] -= amount;
        payable(msg.sender).transfer(amount);
        //payable(msg.sender).send(amount);

        //(bool ok, ) = msg.sender.call{value: amount}("");
        //if (!ok) revert("");

    }
}

Output after running solc-verify:

Reentrancy::deposit: OK
Reentrancy::withdraw: ERROR
 - Reentrancy.sol:18:5: Invariant '__verifier_sum_uint(balances) <= address(this).balance' might not hold at end of function.
Reentrancy::[implicit_constructor]: OK
Reentrancy::[receive_ether_selfdestruct]: OK
ReentrancyGuard::[constructor]: OK
Use --show-warnings to see 2 warnings.
Errors were found by the verifier.

It is similar to send() function, always returns this when these functions are actually reentrant proof right?

Thanks.

[jcrreis]

Sorry @hajduakos can you help me on this questions? I'm researching tools to verify smart contracts and this one seems promising and I would like to investigate it more :) Thank you

[hajduakos]

Hi @jcrreis ! Sorry, I don't actively work on this project so it might take some time to reply.

There are a few thing that the tool can't deal with, even on the 0.7 version, including tx.origin, delegatecall and selfdestruct.

As for reentrancy in 0.8: it looks interesting. Does the same example work with 0.7?

[jcrreis]

Hello @hajduakos ,

Thank you for your clarification.

About reentrancy i couldn't try in version 0.7, but I would say that it should be identical as 0.8, because there were not major changes to these functions in 0.8. Both send() and transfer() were also reentrant proof in 0.7. This should be a feature to look if you are going to make an update in a future.

I liked the idea behind this tool, which brings invariants that doesn't exist in SMTChecker.

For now I will keep an eye in this tool and if I can see a way to improve I will open a pull request.