2

I was using the SMT Solidity Model Checker, and I Don't understand why I have a :" BMC: Insufficient funds happens here". My code is quite simple, I just wanted to check if the Model Checker analyses well reentrancy. Does anyone know if the checker model actually has a problem, or is it the code that is vulnerable? Thanks in advance for your answers

pragma solidity >=0.8.0;

contract Reentrancy {

uint public balance;
    
function withdraw(uint amount) public payable {
    require (balance > amount);
    balance -= amount;
    payable(msg.sender).transfer(amount);
}

}

1 Answer 1

1

When the contract makes a transfer it does not use your state variable balance, but rather the balance of the contract as in address(this).balance. Since that balance is not being checked, transfer(amount) may revert because address(this).balance < amount is possible. The code below applies the proper check and the warning message is gone:

pragma solidity >=0.8.0;

contract Reentrancy {
    function withdraw(uint amount) public payable {
        require (address(this).balance > amount);
        payable(msg.sender).transfer(amount);
    }

}

Please note that because transfer does not forward a lot of gas, the model checker assumes that reentrancy is not possible in this case. One possible way for you to play with reentrancy in the model checker is, for example:

pragma solidity >=0.8.0;

interface D { function e() external; }

contract C {
    bool locked = true;

    function call(address target) public {
        locked = false;
        D(target).e();
        locked = true;
    }

    function broken() public view {
        assert(locked);
    }
}
1
  • Thank you very much for the answer! Is the reason that the cost of recalling a external function (e.g. the same one, to do reetrancy) is higher than 2300 gas, the allowed gas value for operations done via a transfer function? If so: is it correct to say that as the model checker does not handle function calls via call, there is still no mechanism to warn when a function call is made but the value of an account is updated after that call? For example this can happen in the contract Simple_dao of the link : swcregistry.io/docs/SWC-107#simple-daosol Jun 4, 2021 at 14:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.