Passing Tests w/ Oyente #689

ghost · 2018-06-27T02:03:35Z

Submit a PR with tests passing with Oyente.

This may require interacting with the project maintainers to get it working 100% with Augur's contracts. We suggest working with them on bug reports, fail cases, etc. Please join the #dev or #bounties channel of our Discord with any questions.

Almost all of the errors are Oyente bugs, there are some failed assertions, but it's failing on spots where Augur doesn't even have an assertion.

Bounty posted with Gitcoin.

[1] https://github.com/melonproject/oyente

gitcoinbot · 2018-06-27T03:18:14Z

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

This issue now has a funding of 250.0 DAI (250.0 USD @ $1.0/DAI) attached to it.

If you would like to work on this issue you can 'start work' on the Gitcoin Issue Details page.
Questions? Checkout Gitcoin Help or the Gitcoin Slack
$28,748.35 more funded OSS Work available on the Gitcoin Issue Explorer

cryptomental · 2018-06-28T05:37:51Z

It seems that the work was already done and submitted #688 , https://travis-ci.com/AugurProject/augur-core/jobs/131758314 . I will then stop working on it.

joeykrug · 2018-06-28T17:05:11Z

It wasn't actually working [e.g. the oyente stuff throws a bunch of errors]

ghost · 2018-06-28T19:24:08Z

cc: @cryptomental ^^

cryptomental · 2018-06-28T20:13:56Z

Hi @joeykrug @tomkysar ok I get it now. I parsed Travis logs and I found quite a few overflows and a few assertion failures:

contract /app/source/contracts/trading/Orders.sol:Orders:
	============ Results ===========
	  EVM Code Coverage: 			 74.5%
	  Integer Underflow: 			 True
	  Integer Overflow: 			 True
	  Parity Multisig Bug 2: 		 False
	  Callstack Depth Attack Vulnerability:  False
	  Transaction-Ordering Dependence (TOD): False
	  Timestamp Dependency: 		 False
	  Re-Entrancy Vulnerability: 		 False
	  Assertion Failure: 			 True
--
contract /app/source/contracts/trading/Trade.sol:Trade:
	============ Results ===========
	  EVM Code Coverage: 			 71.3%
	  Integer Underflow: 			 False
	  Integer Overflow: 			 False
	  Parity Multisig Bug 2: 		 False
	  Callstack Depth Attack Vulnerability:  False
	  Transaction-Ordering Dependence (TOD): False
	  Timestamp Dependency: 		 False
	  Re-Entrancy Vulnerability: 		 False
	  Assertion Failure: 			 True
--
contract /app/source/contracts/trading/Cash.sol:Cash:
	============ Results ===========
	  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
--
contract /app/source/contracts/trading/CreateOrder.sol:CreateOrder:
	============ Results ===========
	  EVM Code Coverage: 			 64.3%
	  Integer Underflow: 			 False
	  Integer Overflow: 			 False
	  Parity Multisig Bug 2: 		 False
	  Callstack Depth Attack Vulnerability:  False
	  Transaction-Ordering Dependence (TOD): False
	  Timestamp Dependency: 		 False
	  Re-Entrancy Vulnerability: 		 False
	  Assertion Failure: 			 True
--
contract /app/source/contracts/trading/CancelOrder.sol:CancelOrder:
	============ Results ===========
	  EVM Code Coverage: 			 34.4%
	  Integer Underflow: 			 False
	  Integer Overflow: 			 False
	  Parity Multisig Bug 2: 		 False
	  Callstack Depth Attack Vulnerability:  False
	  Transaction-Ordering Dependence (TOD): False
	  Timestamp Dependency: 		 False
	  Re-Entrancy Vulnerability: 		 False
	  Assertion Failure: 			 True
--
contract /app/source/contracts/trading/OrdersFetcher.sol:OrdersFetcher:
	============ Results ===========
	  EVM Code Coverage: 			 86.5%
	  Integer Underflow: 			 False
	  Integer Overflow: 			 False
	  Parity Multisig Bug 2: 		 False
	  Callstack Depth Attack Vulnerability:  False
	  Transaction-Ordering Dependence (TOD): False
	  Timestamp Dependency: 		 False
	  Re-Entrancy Vulnerability: 		 False
	  Assertion Failure: 			 True
--
contract /app/source/contracts/reporting/FeeWindow.sol:FeeWindow:
	============ Results ===========
	  EVM Code Coverage: 			 72.4%
	  Integer Underflow: 			 False
	  Integer Overflow: 			 True
	  Parity Multisig Bug 2: 		 False
	  Callstack Depth Attack Vulnerability:  False
	  Transaction-Ordering Dependence (TOD): False
	  Timestamp Dependency: 		 False
	  Re-Entrancy Vulnerability: 		 False
	  Assertion Failure: 			 True
--
contract /app/source/contracts/reporting/Market.sol:Market:
	============ Results ===========
	  EVM Code Coverage: 			 39.8%
	  Integer Underflow: 			 True
	  Integer Overflow: 			 True
	  Parity Multisig Bug 2: 		 False
	  Callstack Depth Attack Vulnerability:  False
	  Transaction-Ordering Dependence (TOD): False
	  Timestamp Dependency: 		 False
	  Re-Entrancy Vulnerability: 		 False
	  Assertion Failure: 			 True
--
contract /app/source/contracts/reporting/DisputeCrowdsourcer.sol:DisputeCrowdsourcer:
	============ Results ===========
	  EVM Code Coverage: 			 66.0%
	  Integer Underflow: 			 False
	  Integer Overflow: 			 True
	  Parity Multisig Bug 2: 		 False
	  Callstack Depth Attack Vulnerability:  False
	  Transaction-Ordering Dependence (TOD): False
	  Timestamp Dependency: 		 False
	  Re-Entrancy Vulnerability: 		 False
	  Assertion Failure: 			 True

As example let's take the last assertion failure:

contract /app/source/contracts/reporting/DisputeCrowdsourcer.sol:DisputeCrowdsourcer:
	============ Results ===========
	  EVM Code Coverage: 			 66.0%
	  Integer Underflow: 			 False
	  Integer Overflow: 			 True
	  Parity Multisig Bug 2: 		 False
	  Callstack Depth Attack Vulnerability:  False
	  Transaction-Ordering Dependence (TOD): False
	  Timestamp Dependency: 		 False
	  Re-Entrancy Vulnerability: 		 False
	  Assertion Failure: 			 True
/app/source/contracts/reporting/DisputeCrowdsourcer.sol:71:10: Warning: Integer Overflow.
        return true;
        ^
Spanning multiple lines.
/app/source/contracts/reporting/DisputeCrowdsourcer.sol:14:5: Warning: Integer Overflow.
    function initialize(IMarket _market, uint256 _size, bytes32 _payoutDistributionHash, uint256[] _payoutNumerators, bool _invalid) public onlyInGoodTimes beforeInitialized returns (bool) {
    ^
Spanning multiple lines.
Integer Overflow occurs if:
    _payoutNumerators = 115792089237316195423570985008687907853269984665640564039457584007913129639935
/app/source/contracts/reporting/DisputeCrowdsourcer.sol:66:36: Warning: Assertion Failure.
        uint256 _reputationShare = _reputationSupply.mul(_attotokens).div(_supply)
Assertion Failure occurs if:
    balances[msg.sender] = 0
	====== Analysis Completed ======

Checking contract's source code it points to withdrawInEmergency()

   function withdrawInEmergency() public onlyInBadTimes returns (bool) {
        uint256 _reputationSupply = reputationToken.balanceOf(this);
        uint256 _attotokens = balances[msg.sender];
        uint256 _supply = totalSupply();
        uint256 _reputationShare = _reputationSupply.mul(_attotokens).div(_supply);
        burn(msg.sender, _attotokens);
        if (_reputationShare != 0) {
            require(reputationToken.transfer(msg.sender, _reputationShare));
        }
        return true;
    }

It claims to assert in line

 uint256 _reputationShare = _reputationSupply.mul(_attotokens).div(_supply);

if balances[msg.sender] == 0

but if balances[msg.sender] == 0 then simply _attotokens is 0, and the reputation share is equal 0, if this is the case reputation token is not transferred. I see no assertion here so it is a false positive assertion failure result. I guess we could go through one by one of those and explain the result, and/or add a require statement where needed. Is this the kind of task you defined for this bounty?

sharkcrayon · 2018-07-04T13:57:02Z

@nuevoalex I'm assigning you to this issue. Please be the point-of-contact/coordinator here.

https://app.clubhouse.io/augur/story/13218/github-issue-oyente

cryptomental · 2018-07-04T15:00:09Z

Thanks @sharkcrayon , @nuevoalex you can ping me via Discord on #bounties channel or comment here what / if anything needs to be done for this bounty. Otherwise it can be closed.

nuevoalex · 2018-07-04T17:54:45Z

@cryptomental The focus of this bounty is really to fix the oyente checker itself so that we don't have to ignore it's output when running it. The end goal would be to have the runOyente.py script actually use the exit code provided here:

https://github.com/AugurProject/augur-core/blob/master/source/tools/runOyente.py#L39

For that to be possible we'll need to be able to:

Specify what sort of error should cause a failure and what should not (Transaction-Ordering Dependence hits are sometimes legitimate but we do not care about those in most cases)
Stop getting false positives from oyente

The second point there is where I believe the majority of the work here is. Let me know if you need any more clarity on what we need.

cryptomental · 2018-07-05T12:33:35Z

@nuevoalex makes sense. I will check this later today.

cryptomental · 2018-07-05T13:47:10Z

@nuevoalex I read Oyente paper and analysed the tool's sources. I also analysed Augurs' failures. Lots of under/overlflow reports and the Transaction-Ordering Dependence.

the return code from the Oyente tool is retrieved from symExec.run()
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/oyente.py#L86
whereas return_code itself is a result of vulnerability_found()
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2315
see return results, vulnerability_found()
vulnerability_found() returns 1 if any vulnerabilty is found
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2337
Default vulnerabilities to check are listed here
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2346
appended with optional assertions and parity_multisig_bug_2
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2348

I personally do not like the code style there huge file, lots of global variables etc. but it is likely due to the fact that code comes from a university. The main point to note is that vulnerabilities list is a list of instance variable of classes that hold maps of vulnerabilities found.

Vulnerabilities are detected here:

What I would do here to satisfy Augur's bounty is:

Fork Oyente, add a new optional command line arg with a list of excluded vulnerabilities that cause a failure, e.g. ['assertions', 'time_dependency']. The vulnerabilities would still be checked for and their results displayed but they would not cause return_code to be set to 1.
Patch Oyente by injecting code in this line https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2351 to remove the list of vulnerabilities that cause failure. Likely some introspection hokus-pokus will be needed to check type of the instance vars to be removed.
After 1&2 works redirect Augur's Dockerfile to use the fork and exclude assertions and Transaction-Ordering Dependence hits.

Please let me know if it makes sense for you, if so I can start.

nuevoalex · 2018-07-05T17:34:45Z

@cryptomental I think that all makes sense and sounds great! However by itself that would only satisfy the bounty by ignoring classes of errors that we are actually interested in.

For example we don't actually want to ignore assertion failures. Instead we want the Oyente code to stop giving us false positives and fail if it detects one (since with the false positives removed this would indicate a serious problem).

IMO all we initially care about re: fixing Oyente false positives are:

Assertion Failures
Re-Entrancy Vulnerability

Our codebase shouldn't actually have any of those so with the settings on to return a passing exit code ignoring any other vulnerabilities we should be able to check for those in CI.

As @tomkysar noted in the initial issue description this part may involve working with the project maintainers to get them to fix this or get guidance on how to fix it.

cryptomental · 2018-07-05T22:32:40Z

Ok I found the maintainer. @luongnt95 I will open a ticket in Oyente space where we can discuss this.

…ild optimization. * Switch to Oyente feature branch with ignoring selected issues addon. * Use 8 CPU cores to build Z3 solver * Enable verbose and Oyente debug mode. Refs: AugurProject#689

Return real Oyente exit code. Refs: AugurProject#689

cryptomental · 2018-07-09T12:47:45Z

From what I have seen in the Oyente sources contracts are compiled, then disassembled with post-processing and Z3 solver is running a symbolic execution against the disassembled code. Assertions are detected by detecting an opcode in source map.

I solved ignoring classes of errors and was able to deliver the debug log to Oyente oyente.debug.txt

Unfortunately at this point I need Oyente maintainer support to continue.

cryptomental · 2018-07-09T12:59:41Z

master...cryptomental:feature/ignore-selected-oyente-issues

I will not open a PR until there is an answer from Oyente team, perhaps the failures can be added to false positives on the Oyente side as well.

gitcoinbot · 2018-07-20T09:11:13Z

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

Work has been started.

These users each claimed they can complete the work by 316 years, 2 months from now.
Please review their action plans below:

1) cryptomental has started work.

I will check this again with latest Oyente Dockerfile changes and let's close this issue.

Learn more on the Gitcoin Issue Details page.

cryptomental · 2018-07-20T11:56:13Z

I asked Oyente and I am doing Z3 solver upgrade from 4.5.0 to 4.7.1. Let's see if it reduces false positives.

cryptomental · 2018-07-20T12:57:39Z

As I suspected the latest Z3 solver does not show those false positive assertions anymore. Unfortunately it collapsed with a segmentation fault on Orders.sol

contract /app/source/contracts/trading/Orders.sol:Orders:
	============ Results ===========
Segmentation fault (core dumped)

I will try to downgrade and see if I can find a version that is more stable and without assertions.

cryptomental · 2018-07-20T14:24:50Z

I finished the analysis.

False positive assertions reported by Oyente seem to be gone when Z3 solver is upgraded (at least for the contracts that were analysed, unfortunately not all contracts are analysed because then the upgraded Z3 segfaults), so the root cause of the issue seems to be Z3 solver and not Oyente itself , see comments in enzymefinance/oyente#339

Full logs with the segfault:

https://gist.github.com/cryptomental/c5ff857becfeda48c8c0fbb432eeba90
https://gist.github.com/cryptomental/04e70f3b849573980814a29aa45134ac

I opened a ticket for the segfault in Microsoft's Z3 solver:

Z3Prover/z3#1766

and I opened a PR to Augur that allows to treat the assertions as warnings until Z3 solver is fixed.

#715

@tomkysar @joeykrug @nuevoalex @vs77 this is rather a workaround to fix Z3 false positives, but it will allow to fail Oyente test run for Augur contracts if any other issues are found. In this case the Oyente will fail with a non-zero return code. I hope merging this PR will be enough to close this issue as not much more can be done until new Z3 solver is released.

gitcoinbot · 2018-07-20T15:19:57Z

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

Work for 250.0 DAI (250.0 USD @ $1.0/DAI) has been submitted by:

@cryptomental

@tomkysar please take a look at the submitted work:

PR by @cryptomental

Learn more on the Gitcoin Issue Details page
Questions? Checkout Gitcoin Help or the Gitcoin Slack
$27,836.75 more funded OSS Work available on the Gitcoin Issue Explorer

nuevoalex · 2018-07-20T18:19:30Z

Responded in the PR

cryptomental · 2018-07-26T11:16:01Z

A Principal Researcher from Microsoft started to looking into the segfault, see Z3Prover/z3#1766, I provided more logs, hopefully this will be resolved.

cryptomental · 2018-07-30T07:01:31Z

Z3Prover/z3#1766 was fixed, but another independent Z3 issue appeared, I provided intructions and logs at Z3Prover/z3#1776

cryptomental · 2018-07-31T08:19:27Z

I added more information at Z3Prover/z3#1776 (comment) including instructions on how to run Augur's Oyente run with gdb on a free Alpine linux based shell.

This setup allows virtually anyone with a web browser or an old PC with linux or Windows/Putty to quickly build and try out Augur test runs on a quite strong virtual shell instance. Feel free to add this as readme anywhere if looks useful @nuevoalex @tomkysar @joeykrug

nuevoalex · 2018-08-02T19:33:12Z

@cryptomental Excellent. Sounds like they're making progress on the issue as well. Really appreciate the effort put forth here. Hopefully this fixes it all up!

cryptomental · 2018-08-03T09:03:06Z

Thank you @nuevoalex I do hope so!

adrake33 · 2018-11-30T21:22:36Z

Copying this over to the AugurProject/augur repo since we are consolidating our Issues there.

adrake33 · 2018-11-30T21:22:50Z

Issue moved to AugurProject/augur #250 via ZenHub

nuevoalex self-assigned this Jul 4, 2018

cryptomental mentioned this issue Jul 5, 2018

False positives Augur project enzymefinance/oyente#339

Open

cryptomental added a commit to cryptomental/augur-core that referenced this issue Jul 9, 2018

source/tools/runOyente: Ignore AssertionFailure and MoneyConcurrency.

e5877c3

Return real Oyente exit code. Refs: AugurProject#689

This was referenced Jul 20, 2018

Z3 4.7.1 segfault at theory_bv.cpp:1394 during Augur contracts analysis Z3Prover/z3#1766

Closed

Feature/ignore selected oyente issues #715

Open

adrake33 mentioned this issue Nov 30, 2018

Passing Tests w/ Oyente AugurProject/augur#250

Closed

adrake33 closed this as completed Nov 30, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Passing Tests w/ Oyente #689

Passing Tests w/ Oyente #689

ghost commented Jun 27, 2018

gitcoinbot commented Jun 27, 2018

cryptomental commented Jun 28, 2018

joeykrug commented Jun 28, 2018

ghost commented Jun 28, 2018

cryptomental commented Jun 28, 2018

sharkcrayon commented Jul 4, 2018 •

edited

Loading

cryptomental commented Jul 4, 2018

nuevoalex commented Jul 4, 2018

cryptomental commented Jul 5, 2018

cryptomental commented Jul 5, 2018

nuevoalex commented Jul 5, 2018

cryptomental commented Jul 5, 2018

cryptomental commented Jul 9, 2018

cryptomental commented Jul 9, 2018

gitcoinbot commented Jul 20, 2018 •

edited

Loading

cryptomental commented Jul 20, 2018

cryptomental commented Jul 20, 2018

cryptomental commented Jul 20, 2018 •

edited

Loading

gitcoinbot commented Jul 20, 2018

nuevoalex commented Jul 20, 2018

cryptomental commented Jul 26, 2018

cryptomental commented Jul 30, 2018 •

edited

Loading

cryptomental commented Jul 31, 2018

nuevoalex commented Aug 2, 2018

cryptomental commented Aug 3, 2018

adrake33 commented Nov 30, 2018

adrake33 commented Nov 30, 2018

Passing Tests w/ Oyente #689

Passing Tests w/ Oyente #689

Comments

ghost commented Jun 27, 2018

gitcoinbot commented Jun 27, 2018

cryptomental commented Jun 28, 2018

joeykrug commented Jun 28, 2018

ghost commented Jun 28, 2018

cryptomental commented Jun 28, 2018

sharkcrayon commented Jul 4, 2018 • edited Loading

cryptomental commented Jul 4, 2018

nuevoalex commented Jul 4, 2018

cryptomental commented Jul 5, 2018

cryptomental commented Jul 5, 2018

nuevoalex commented Jul 5, 2018

cryptomental commented Jul 5, 2018

cryptomental commented Jul 9, 2018

cryptomental commented Jul 9, 2018

gitcoinbot commented Jul 20, 2018 • edited Loading

cryptomental commented Jul 20, 2018

cryptomental commented Jul 20, 2018

cryptomental commented Jul 20, 2018 • edited Loading

gitcoinbot commented Jul 20, 2018

nuevoalex commented Jul 20, 2018

cryptomental commented Jul 26, 2018

cryptomental commented Jul 30, 2018 • edited Loading

cryptomental commented Jul 31, 2018

nuevoalex commented Aug 2, 2018

cryptomental commented Aug 3, 2018

adrake33 commented Nov 30, 2018

adrake33 commented Nov 30, 2018

sharkcrayon commented Jul 4, 2018 •

edited

Loading

gitcoinbot commented Jul 20, 2018 •

edited

Loading

cryptomental commented Jul 20, 2018 •

edited

Loading

cryptomental commented Jul 30, 2018 •

edited

Loading