proxyOverflow: Oyente fails to detect Integer Overflow in ADD

[vietlq]

Check the line 206:

if(balances[_from] < _feeSmt + _value) revert();

Use https://pastebin.com/fQmRBmQj or https://etherscan.io/address/0x55f93985431fc9304077687a35a1ba103dc1e081#code

I ran Oyente and it fails to detect this simple case.

[vietlq]

@luongnt95 note that Integer Overflow in ADD is not working that well.

[vietlq]

Oyente even fails to detect this simple overflow:

pragma solidity ^0.4.19;

contract IntegerAddOverflow {
    constructor () public {

    }

    function add(uint256 a, uint256 b) pure public returns (uint256) {
        uint256 c = a + b;
        return c;
    }
}

Result:

$ python oyente/oyente.py -s IntegerAddOverflow.sol
WARNING:root:You are using evm version 1.8.6. The supported version is 1.7.3
WARNING:root:You are using solc version 0.4.23, The latest supported version is 0.4.19
INFO:root:contract IntegerAddOverflow.sol:IntegerAddOverflow:
INFO:symExec:   ============ Results ===========
INFO:symExec:     EVM Code Coverage:             99.0%
INFO:symExec:     Integer Underflow:             False
INFO:symExec:     Integer Overflow:              False
INFO:symExec:     Parity Multisig Bug 2:         False
INFO:symExec:     Callstack Depth Attack Vulnerability:  False
INFO:symExec:     Transaction-Ordering Dependence (TOD): False
INFO:symExec:     Timestamp Dependency:          False
INFO:symExec:     Re-Entrancy Vulnerability:         False
INFO:symExec:   ====== Analysis Completed ======

[luongnt95]

if(balances[_from] < _feeSmt + _value) revert(); is the same as require(balances[_from] < _feeSmt + _value) which Oyente consider as being a false positive. Do you have any idea to distinguish between the REVERT created from require and revert ?

[luongnt95]

The second contract works now with this commit

[vietlq]

@luongnt95 May I ask if these 2 compile to the same OP code?

• if(balances[_from] < _feeSmt + _value) revert();
• require(balances[_from] < _feeSmt + _value);

If yes, only then you should treat them the same.

As for the fix, you can see overflows in both cases and both require & if + revert fail to catch! They can only catch when there's no overflow!!!

So in both cases you should check these 2 conditions:

1. Compulsory: Report MUL/DIV/ADD/SUB operations if people do not use SafeMath or don't check the result after computation
2. Stylistic: Absolutely NO computation (MUL/DIV/ADD/SUB) inside if()/require()/assert() as people tend NOT to think they can underflow/overflow. You can add this fix later

You can see that 2. helps 1. as people learn to write code that is more readable & safer.

[vietlq]

@luongnt95 I want to give you more context about proxyOverflow if you haven't seen the vulnerability exploitation: https://peckshield.com/2018/04/25/proxyOverflow/

[vietlq]

I also found this merge that treats overflows in revertible cases as false positives, but as said before and with given examples, this assumption is not correct:

https://github.com/melonproject/oyente/pull/306/commits/1d1542ff006674eac8499981557b225e00f73fbb

[luongnt95]

Thanks @vietlq I know the expoitation and the commit.

• Yeah, require and if revert() is compiled to the same opcodes.
• The #306 commit will help flag require(a + _value >= a); a += _value as a false positive, without the commit a + _value in require is an overflow. And it's quite annoying to flag this case as a bug. Anyway, think this commit doesn't work well 'cause people use revert() a lot without the intention of avoiding the overflow
• There are a lot of arithmetic opcodes which are not generated from arithmetic operations and it's really expensive to check all these opcodes

[vietlq]

@luongnt95 I think it's OK to revert/replace/enhance #306 because people should be using the SafeMath library instead of writing those lines again and again.

https://github.com/OpenZeppelin/openzeppelin-solidity/blob/master/contracts/math/SafeMath.sol

So require(a + _value >= a); a += _value will be a reminder to use SafeMath, not a false positive. Eventually Solidity needs a standard library and forcing people to use SafeMath is the right first step towards it.