False positives Augur project

[cryptomental]

Hi @luongnt95 we are trying to fix false positive results in Augur project for

• Assertion Failures
• Re-Entrancy Vulnerability

See

https://github.com/AugurProject/augur-core/issues/689

Is there a feasible way to achieve this or do we depend on z3 solver?

I came up with a workaround to not return 0 code for a subset of vulnerabilities but we would like to make sure that false positives are filtered out and do not show up for Augur contracts.

FYI: @tomkysar @nuevoalex

[cryptomental]

I am attaching a full Oyente log with debug log enabled. oyente.debug.txt

[cryptomental]

Hi @yxliang01 there has not been any reply since two weeks but I noticed that you commented on another ticket yesterday. Is the Oyente project still maintained? And would it be possible to have a look at https://github.com/AugurProject/augur-core/issues/689 and check if false positives could be in any way excluded? If not I will open a PR to Augur to simply treat those assertions as non-errors.

[yxliang01]

Hello @cryptomental , I actually don't know whether this is still being maintained. I have had a look at the error:

/app/source/contracts/trading/Trade.sol:59:29: Warning: Assertion Failure.
        Order.Types _type = Order.getOrderTradingTypeFromFillerDirection(_direction)
Assertion Failure occurs if:
    _direction = 254

But, I couldn't see the assert statements that are failing. Maybe I missed something and you can elaborate more?

[cryptomental]

Hi @yxliang01 thank you a lot for looking into this. This is exactly the case - there are no assert statements and assertions should be marked as false positives. I implemented a workaround where the assertions are treated as warnings not as errors but perhaps there is a way to fix this on Oyente side. But if the project is not actively maintained I would stay with the workaround and inform the Augur team. I would be grateful for your feedback on this.

[cryptomental]

Hi @yxliang01 again, I upgraded Z3 solver and those false assertions are gone, but the analysis was just half done as it segfaulted https://github.com/AugurProject/augur-core/issues/689 , I will try to find a version that does not segfault.

[yxliang01]

@cryptomental This is interesting. Have seen Oyente finished checking Trade.sol without reporting any Assertion Failure?

[cryptomental]

Hi @yxliang01 it did not get to that point, I pasted the whole log for you here https://gist.github.com/cryptomental/c5ff857becfeda48c8c0fbb432eeba90

[yxliang01]

@cryptomental as far as I see, for the contracts that previously said containing assertion failure, they either hasn't been scanned before segfault or they are still being reported as having this vulnerability. So, I didn't see that false assertions are gone.

[cryptomental]

Hi @yxliang01 the assertions there are 'true' assertions. The only one found was for Cash.sol, where indeed the assertion could have been triggered.

      EVM Code Coverage:             97.2%
      Integer Underflow:             False
      Integer Overflow:              False
      Parity Multisig Bug 2:         False
      Callstack Depth Attack Vulnerability:  False
      Transaction-Ordering Dependence (TOD): True
      Timestamp Dependency:          False
      Re-Entrancy Vulnerability:         False
      Assertion Failure:             True
Flow1
/app/source/contracts/trading/Cash.sol:45:9: Warning: Transaction-Ordering Dependency.
        _to.transfer(_amount)
Flow2
/app/source/contracts/trading/Cash.sol:45:9: Warning: Transaction-Ordering Dependency.
        _to.transfer(_amount)
/app/source/contracts/trading/Cash.sol:46:9: Warning: Assertion Failure.
        assert(this.balance >= totalSupply())
Assertion Failure occurs if:
    _amount = 1
    balances[_from] = 1
    ====== Analysis Completed ======

I opened a ticket in Z3 space for the segfault.

[yxliang01]

@cryptomental Hey! I'm wondering what the progress on this issue is at the moment. For the issues I can find on Github, looks like it's paused? Or, is it?