Incorrect assert violation found sequence

[cleanunicorn]

Description

The following scan of the contract produces an assert violation in an incorrect way.

How to Reproduce

Consider the following contracts

contract A {
    function() external payable {}
    
    // 0x3fa4f245
    function value() public returns (uint) {
        emit Value(address(this).balance);
        return address(this).balance;
    }
    
    // 0xb46300ec
    function send() public {
        msg.sender.transfer(address(this).balance);
    }
    
    // 0x3305a8e4
    function selfDes() public {
        selfdestruct(msg.sender);
    }
    
    event Value(uint amount);
}

contract B {
    A public a;
    
    bool reentrancyGuard = false;
    
    constructor() public payable {
        a = new A();
        
        address payable payableA = address(uint160(address(a)));
        
        (bool success, bytes memory result) = payableA.call.value(msg.value)("");
        
        a.value();
    }
    
    function() external payable {
        address targetContract = address(a);
        
        if (reentrancyGuard == false) {
            reentrancyGuard = true;
            assembly {
                let freememstart := mload(0x40)
                calldatacopy(freememstart, 0, calldatasize())
                let success := call(not(0), targetContract, callvalue, freememstart, calldatasize(), freememstart, 32)
                switch success
                case 0 { revert(freememstart, 32) }
                default { return(freememstart, 32) }
            }        
            reentrancyGuard = false;
        }
    }
    
    function value() public returns (uint) {
        emit Value(address(this).balance);
        return address(this).balance;
    }
    
    function test_balance() public {
        if (this.value() > 0) {
            assert(false);
        }
    }
    
    event Value(uint amount);
}

Save them as contracts.sol and run on the command line:

$ myth a contracts.sol:B -m exceptions
==== Exception State ====
SWC ID: 110
Severity: Low
Contract: B
Function name: test_balance()
PC address: 522
Estimated Gas Usage: 1790 - 36352
A reachable exception has been detected.
It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.
--------------------
In file: a.sol:61

assert(false)

--------------------
Initial State:

Account: [CREATOR], balance: 0x1, nonce:0, storage:{}
Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}
Account: [SOMEGUY], balance: 0x1, nonce:0, storage:{}

Transaction Sequence:

Caller: [CREATOR], data: [CONTRACT_CREATION], value: 0x0
Caller: [ATTACKER], function: test_balance(), txdata: 0x13b07f34, value: 0x0

The found call sequence seems to produce an assert violation but that is incorrect.

Expected behavior

An assert violation should be found if you have the following call sequence:

• Deploy contract with at least 1 wei
• 0x3305a8e4 -> which forwards to A.selfDes() and seldestructs sending all available ether from A to B
• test_balance() will raise an assert error because it received some ether from contract A

Environment

• Mythril version: Mythril version v0.21.20
• Solidity compiler and version: Version: 0.5.13+commit.5b0b510c.Linux.g++
• Python version: Python 3.8.0
• OS and Version: Linux cola 5.3.13-arch1-1 #1 SMP PREEMPT Sun, 24 Nov 2019 10:15:50 +0000 x86_64 GNU/Linux (Arch Linux)

[JoranHonig]

This is an interesting case you found 👍

[norhh]

The following scan of the contract produces an assert violation in an incorrect way. It kinda depends on the assumptions. Mythril assumes that some random guy knows your nonce and may have sent some eth to this address to screw it up before you creating it :sunglasses: , all that matters is whether we want this assumption or not.

[cleanunicorn]

Mythril assumes that some random guy knows your nonce and may have sent some eth to this address to screw it up before you creating it :sunglasses:

I understand that Mythril can do this assumption and I really like it does that. I did not know it also changes the balance of the contracts.

all that matters is whether we want this assumption or not.

I think the initial state should include the balance of the "not yet" deployed contract in this part of the output.

--------------------
Initial State:

Account: [CREATOR], balance: 0x1, nonce:0, storage:{}
<-- HERE
Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}
Account: [SOMEGUY], balance: 0x1, nonce:0, storage:{}

Maybe something like:

Account: [CONTRACT], balance: 0x1, nonce:0, storage:{}

It will make it more explicit and more obvious that Mythril does this and that this behavior is intended.