Z3 4.7.1 segfault at theory_bv.cpp:1394 during Augur contracts analysis

[cryptomental]

Oyente, Ethereum smart contracts analysis tool, which runs Z3 solver under the hood fails with a Z3 segfault when Z3 solver is upgraded to 4.7.1 and Oyente tool is analysing Augur smart contracts.

The segfault does not happen on Z3 4.5.0 and 4.6.0.

Steps to reproduce:

Those commands run Oyente with 4.5.0 solver:

 $  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

Switching to 4.7.1 can be done with the following patch in source/support/test/oyente/Dockerfile :

diff --git a/source/support/test/oyente/Dockerfile b/source/support/test/oyente/Dockerfile
index e12061d5..43acfb23 100644
--- a/source/support/test/oyente/Dockerfile
+++ b/source/support/test/oyente/Dockerfile
@@ -11,9 +11,9 @@ RUN apt-get update \
        && apt-get install -y software-properties-common \
        && apt-get install -y unzip
 
-RUN wget --quiet https://github.com/Z3Prover/z3/archive/z3-4.5.0.zip \
-       && unzip z3-4.5.0.zip -d /tmp \
-       && cd /tmp/z3-z3-4.5.0 \
+RUN wget --quiet https://github.com/Z3Prover/z3/archive/z3-4.7.1.zip \
+       && unzip z3-4.7.1.zip -d /tmp \
+       && cd /tmp/z3-z3-4.7.1 \
        && python scripts/mk_make.py --python \
        && cd build \
        && make -j8 \

Full Oyente log with segfault:

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

Verbose Oyente log including ASM dump:

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

References:

AugurProject/augur-core#689
enzymefinance/oyente#339

[cryptomental]

I built Z3 in debug mode and executed again, the failure happens at https://github.com/Z3Prover/z3/blob/master/src/smt/theory_bv.cpp#L1394:

==============================
EXECUTING: DUP1 
==============================
EXECUTING: EXTCODESIZE 
==============================
EXECUTING: ISZERO 
==============================
EXECUTING: ISZERO 
==============================
EXECUTING: PUSH2 0x0396 
==============================
EXECUTING: JUMPI 
Branch expression: If(code_size_Concat(0, Extract(159, 0, _market)) == 0, 0, 1) !=
0
ASSERTION VIOLATION
File: ../src/smt/theory_bv.cpp
Line: 1394
bits1.size() == bits2.size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
The command '/bin/sh -c python source/tools/runOyente.py -p -a -v' returned a non-zero code: 110

[NikolajBjorner]

Getting back from offline. Can you create a log? Use z3_open_log before all else.

[cryptomental]

Hi @NikolajBjorner thank you for looking into this issue. I was able to reproduce the issue with Z3 log enabled.

Please find below the tarball with the log, it contains all the information, including Z3 build and running the Z3 analysis with segfault reproduced.

Z3 log starts with "cat z3_log.txt".

z3_segfault_with_log.zip

[NikolajBjorner]

Thanks,
The log starts as follows:

V "4.7.1.0 Jul 26 2018"
R
P 0x18c85f8
C 408
= 0x27cd368
R
P 0x18c85f8

The instruction P means it is reading a pointer, previously returned by Z3 as a value to something else.
This indicates that other functions from Z3 were called before the Z3_open_log call. It should be the very first call into Z3.
If you are able to upload an update, could you do me a nice favor and also separate out the pre-amble before the line with V?

[cryptomental]

@NikolajBjorner Oyente tool uses z3 Python bindings. I moved z3 import to the very beginning and opened z3 log right after the import.

+import z3
+z3.Z3_open_log("z3_log.txt")
+
 from oyente.oyente import run_solidity_analysis
 from oyente.input_helper import InputHelper
 from oyente.source_map import SourceMap

Now the log starts with

V "4.7.1.0 Jul 26 2018"
R
C 3
= 0xc40f18
R
P 0xc40f18
C 7
= 0xc9a8b8
...

Please find the full log attached
z3_log_augur_moved_init.zip

The whole docker pre-amble was also separated out as you requested. I hope that you will be able to continue.

[NikolajBjorner]

looking at it. ...
Some notes: the (pretty long running) log, when replayed hits a nullpointer
dereference when a function declaration that is null (out of scope) gets passed in.
This can't be the state you have when running directly (because it would have crashed before).
As I am having some false starts with reproducing the error directly, a concurrent effort would be to trim the set of unit tests that are run before the failure. I don't see "JUMPI" in your project so guess (haven't dug much) that your test imports this from somewhere else.
If your use of Z3 is standard Solver.check() based, then another things we can try is to dump the solver state before the offending call to Solver.check(). The way to serialize it to SMT-LIB2 is Solver.sexpr(). The catch is that bugs don't necessarily reproduce on the SMT2 file.

[cryptomental]

@NikolajBjorner I managed to dump sexpr() before each solver.check() call. Full log attached.

full_sexpr_dump.zip

It gets interesting now as I logged into the Docker container to apply changes in Oyente and executed the Oyente tool from inside Docker console. With Z3 compiled in debug mode after Z3 sassert was thrown, Z3 asked me to jump into the debugger or throw an exception, I chose the latter and the Oyente tool continued its execution. The ASSERTION VIOLATION
File: ../src/smt/theory_bv.cpp:1394 happened 3 times during the whole run, you should be able to observe this in the log.

As a side note, About the JUMPI and the Oyente itself - I am neither the author, nor maintainer of the tool, I am merely trying to fix false positive assertions returned by the tool for Augur, Ethereum-based smart contracts.

JUMPI is one of the Ethereum virtual machine opcodes, and the Oyente definition for Z3 is available at https://github.com/melonproject/oyente/blob/52bf194f1da39f0de2a6e06a4c9e9452739cc3e0/oyente/opcodes.py

The Oyente tool was developed in Singapore as a research project and I am not sure if it is still maintained https://www.comp.nus.edu.sg/~loiluu/papers/oyente.pdf I tried to ask them but it might be they are not that responsive due to holiday season.

The original reason I got involved into this issue and discovered Z3 is that the Oyente tool returns a few false positives Assertion errors, reporting assertions in source code where assertions are not visible.

Integer Overflow occurs if:
    marketOrderData[_market].totalEscrowed = 1
    _amount = 115792089237316195423570985008687907853269984665640564039457584007913129639935
/app/source/contracts/trading/Orders.sol:85:27: Warning: Assertion Failure.
        return worstOrder[getBestOrderWorstOrderHash(_market, _outcome, _type)
Assertion Failure occurs if:
    _type = 254
/app/source/contracts/trading/Orders.sol:149:20: Warning: Assertion Failure.
        _orderId = getOrderId(_type, _market, _amount, _price, _sender, block.number, _outcome, _moneyEscrowed, _sharesEscrowed)
Assertion Failure occurs if:
    _type = 254
    _outcome = 18004803423401827660848029348735919068346528269279243844115834335381596143615
/app/source/contracts/trading/Orders.sol:81:26: Warning: Assertion Failure.
        return bestOrder[getBestOrderWorstOrderHash(_market, _outcome, _type)
Assertion Failure occurs if:
    _type = 254

I tried to upgrade Z3 to see if it helps and encountered the segfault. I do not think that I will be able to fix those false positives, spent already too much time on this, but at least Z3 segfault could be addressed.

[cryptomental]

I just noticed the log is missing stderr, I will execute again and paste here the relevant part.

[cryptomental]

Surprisingly the job failed now twice in a row on a different line (786), I am pasting only the part that includes last two sexpr() dumps.

last_two.txt

[cryptomental]

I will now have to leave for the weekend, please let me know if you need anything else and I will add this on Monday. I could also prepare a branch of the tool that includes Z3 with a short instruction on how to reproduce the issue, perhaps it will be easier for you to jump straight into the debugger to see what happened.

[NikolajBjorner]

Ha, bingo, I finally hit it. The repro takes quite some time, but it is there. I will try to see what I can do in the next few days so we can close in on this when you are back.

[NikolajBjorner]

The timeouts exposed a bug in how bit-vectors are internalized.
I will fix this in the current master branch.

[cryptomental]

Hi @NikolajBjorner thank you for fixing this one so fast. I did not expect it will be closed over the weekend.

Unfortunately, another assertion in the same Augur run popped up

EXECUTING: REVERT 
TERMINATING A PATH ...
Money flow: [('Is', 'Ia', 'Iv')]
ASSERTION VIOLATION
File: ../src/util/ref_vector.h
Line: 91
sz <= m_nodes.size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

I am not sure if this is related to the fix or a completely separate issue. I will prepare a branch and open another ticket for that one.

[NikolajBjorner]

This is most likely unrelated to the bits initialization, but likely related to handling cancellations.
The challenge with these is that they depend on timeouts that you specify for the calls.

[NikolajBjorner]

BTW, could you paste the stack? There is a slim chance this can tell me something.

[cryptomental]

@NikolajBjorner I pasted Python stack, gdb backtrace, z3 logs and instructions into #1776
I hope that will help.