@tomkysar commented on Tue Jun 26 2018
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 commented on Tue Jun 26 2018
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.
@cryptomental commented on Wed Jun 27 2018
It seems that the work was already done and submitted AugurProject/augur-core#688 , https://travis-ci.com/AugurProject/augur-core/jobs/131758314 . I will then stop working on it.
@joeykrug commented on Thu Jun 28 2018
It wasn't actually working [e.g. the oyente stuff throws a bunch of errors]
@tomkysar commented on Thu Jun 28 2018
cc: @cryptomental ^^
@cryptomental commented on Thu Jun 28 2018
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 commented on Wed Jul 04 2018
@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 commented on Wed Jul 04 2018
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 commented on Wed Jul 04 2018
@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 commented on Thu Jul 05 2018
@nuevoalex makes sense. I will check this later today.
@cryptomental commented on Thu Jul 05 2018
@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.
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:
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2057
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2096
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2149
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2192
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2211
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2225
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2236
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2251
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 commented on Thu Jul 05 2018
@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 commented on Thu Jul 05 2018
Ok I found the maintainer. @luongnt95 I will open a ticket in Oyente space where we can discuss this.
@cryptomental commented on Mon Jul 09 2018
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 commented on Mon Jul 09 2018
AugurProject/augur-core@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 commented on Fri Jul 20 2018
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, 10 months from now. Please review their questions below:
- cryptomental has started work.
- Q: 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 commented on Fri Jul 20 2018
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 commented on Fri Jul 20 2018
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 commented on Fri Jul 20 2018
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.
AugurProject/augur-core#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 commented on Fri Jul 20 2018
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:
@nuevoalex commented on Fri Jul 20 2018
Responded in the PR
@cryptomental commented on Thu Jul 26 2018
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 commented on Mon Jul 30 2018
Z3Prover/z3#1766 was fixed, but another independent Z3 issue appeared, I provided intructions and logs at Z3Prover/z3#1776
@cryptomental commented on Tue Jul 31 2018
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 commented on Thu Aug 02 2018
@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 commented on Fri Aug 03 2018
Thank you @nuevoalex I do hope so!
@adrake33 commented on Fri Nov 30 2018
Copying this over to the AugurProject/augur repo since we are consolidating our Issues there.
@tomkysar commented on Tue Jun 26 2018
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 commented on Tue Jun 26 2018
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.
@cryptomental commented on Wed Jun 27 2018
It seems that the work was already done and submitted AugurProject/augur-core#688 , https://travis-ci.com/AugurProject/augur-core/jobs/131758314 . I will then stop working on it.
@joeykrug commented on Thu Jun 28 2018
It wasn't actually working [e.g. the oyente stuff throws a bunch of errors]
@tomkysar commented on Thu Jun 28 2018
cc: @cryptomental ^^
@cryptomental commented on Thu Jun 28 2018
Hi @joeykrug @tomkysar ok I get it now. I parsed Travis logs and I found quite a few overflows and a few assertion failures:
As example let's take the last assertion failure:
Checking contract's source code it points to withdrawInEmergency()
It claims to assert in line
if balances[msg.sender] == 0
but if
balances[msg.sender] == 0then 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 arequirestatement where needed. Is this the kind of task you defined for this bounty?@sharkcrayon commented on Wed Jul 04 2018
@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 commented on Wed Jul 04 2018
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 commented on Wed Jul 04 2018
@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:
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 commented on Thu Jul 05 2018
@nuevoalex makes sense. I will check this later today.
@cryptomental commented on Thu Jul 05 2018
@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.
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2057
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2096
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2149
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2192
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2211
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2225
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2236
https://github.com/melonproject/oyente/blob/8b825a6ded1f0ba014d462fef3171e218bcc63fc/oyente/symExec.py#L2251
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 commented on Thu Jul 05 2018
@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:
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 commented on Thu Jul 05 2018
Ok I found the maintainer. @luongnt95 I will open a ticket in Oyente space where we can discuss this.
@cryptomental commented on Mon Jul 09 2018
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 commented on Mon Jul 09 2018
AugurProject/augur-core@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 commented on Fri Jul 20 2018
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, 10 months from now. Please review their questions below:
Learn more on the Gitcoin Issue Details page.
@cryptomental commented on Fri Jul 20 2018
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 commented on Fri Jul 20 2018
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
I will try to downgrade and see if I can find a version that is more stable and without assertions.
@cryptomental commented on Fri Jul 20 2018
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.
AugurProject/augur-core#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 commented on Fri Jul 20 2018
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:
@tomkysar please take a look at the submitted work:
$27,836.75 more funded OSS Work available on the Gitcoin Issue Explorer
@nuevoalex commented on Fri Jul 20 2018
Responded in the PR
@cryptomental commented on Thu Jul 26 2018
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 commented on Mon Jul 30 2018
Z3Prover/z3#1766 was fixed, but another independent Z3 issue appeared, I provided intructions and logs at Z3Prover/z3#1776
@cryptomental commented on Tue Jul 31 2018
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 commented on Thu Aug 02 2018
@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 commented on Fri Aug 03 2018
Thank you @nuevoalex I do hope so!
@adrake33 commented on Fri Nov 30 2018
Copying this over to the AugurProject/augur repo since we are consolidating our Issues there.