Feature/ignore selected oyente issues

[cryptomental]

This PR allows to treat selected Oyente issue types as warnings instead of errors.

Reference and reason of the PR: #689

[cryptomental]

I have no idea why Travis errored, the build is fine locally:

 $  git clone https://github.com/cryptomental/augur-core.git
 $  cd augur-core/
 $  git co feature/ignore-selected-oyente-issues
 $  npm run docker:run:test:security:oyente

[nuevoalex]

@cryptomental I'm seeing this generate Assertion Failure Positive hits and still pass.

It looks like the config provided will ignore Assertion failures, but this is one of the two error types we actually want to be correct and fail on.

The two we care about are:

• Assertion Failures
• Re-Entrancy Vulnerability

Even then it appears to just be ignoring any failures too since I see Integer under/overflow hits that must be getting ignored (This is fine but I would expect it to have to be specified in the config)

I guess I have these two questions about the work done here:

• What will this actually fail on?
• Which false positives are fixed in this PR?

[cryptomental]

Hi @nuevoalex , I have to split the answer in two parts. First, the reason of the behavior that you observe is that Oyente does not treat Integer underflow/overflow hits as errors but only reports them as warnings.

I hope that it will be easier to understand when you have a look at https://github.com/melonproject/oyente/blob/master/oyente/symExec.py#L2337

Oyente by default returns non-zero return code if any of [callstack, money_concurrency, time_dependency, reentrancy] vulnerabilities are found.

Additionally by specifying CHECK_ASSERTIONS , the assertions and parity multisig bug are analysed and if any assertion failure/parity bug is found, Oyente returns a non-zero return code.

A few lines above https://github.com/melonproject/oyente/blob/master/oyente/symExec.py#L2326 it can be seen, that integer_underflow and integer_overflow are logged, but they are not taken into account when returning a non-zero return code.

Therefore, to answer your first question, after the change Oyente will fail if any of vulnerabilities are found, excluding integer overflow/underflow, AssertionFailure, and MoneyConcurrency.

Second, no false positives are fixed. All errors are shown, but assertions are not considered as errors.
False positives may have been fixed by Microsoft's Z3 solver, but as reported here Z3Prover/z3#1766 the solver segfaults in the middle of analysis.

Please let me know if this is satisfactory, if not the all the work for the bounty will need to be cancelled and I will void the pull request, as fixing would be on Z3 side.

[nuevoalex]

@cryptomental Are you fairly certain that once the Z3 problems are fixed that we could update this and start failing on assertion errors safely?

[cryptomental]

@nuevoalex yes. We can leave this PR in a limbo until there is a response from Z3 side. Perhaps I can also have a look at their dev branch, try to build Z3 from there and dig deeper on what causes the segfault. I will play around and try to answer till Thursday the latest.

[nuevoalex]

Sounds good! Thank you!

[cryptomental]

@nuevoalex I found out that Z3 segfaults at https://github.com/Z3Prover/z3/blob/master/src/smt/theory_bv.cpp#L1394 , I added this information to Z3Prover/z3#1766 but unfortunately I cannot do much more about it, hopefully Z3 team will pick it up soon.

[pgebheim]

@nuevoalex Can this be closed now or does this apply to V2/monorepo still?