mariachris / storm

A blackbox mutational fuzzer for detecting critical bugs in SMT solvers

Installation:

git clone https://github.com/Practical-Formal-Methods/storm
virtualenv --python=/usr/bin/python3.7 venv
source venv/bin/activate
cd storm
python setup.py install

Usage:

storm --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME]

To test the solver on a particular theory, use the --theory flag. For example:

storm --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=LIA

To run n parallel instances of storm on n cores, use the --cores flag. For example:

storm --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=LIA --cores=10

To obtain a smaller SMT instance that revealed a refutational soundness bug in an SMT solver, use:

storm --min --file_path=[PATH TO SMT INSTANCE] --solver=[SOLVER NAME] --solverbin=[PATH TO SOLVER BIN] --theory=[THEORY NAME] 

If the SMT instance is in incremental mode, use --incremental flag.

Soundness bugs detected so far:

STORM has detected many unique and previously unknown "refutational soundness" bugs in multiple mature SMT solvers. Here is a list of issues we filed on public bug tracking systems for various SMT solvers.

SRI-CSL/yices2#150 [yices] [QF_UFIDL]
SRI-CSL/yices2#160 [yices] [QF_UFLRA]
SRI-CSL/yices2#167 [yices] [QF_UF]
Z3Prover/z3#2758 [z3] [QF_S]
Z3Prover/z3#3067 [z3str3] [QF_S]
https://github.com/levnach/z3/issues/115 [z3] [QF_NIA]
https://github.com/levnach/z3/issues/116 [z3] [QF_NRA]
Z3Prover/z3#2828 [z3] [QF_S]
Z3Prover/z3#2871 [z3] [QF_LIA]
SRI-CSL/yices2#170 [yices] [QF_NRA]
Z3Prover/z3#2829 [z3] [QF_LIA]
Z3Prover/z3#2835 [z3] [QF_UFLIA]
Z3Prover/z3#2873 [z3] [QF_BV]
Z3Prover/z3#2993 [z3] [QF_S]
https://github.com/levnach/z3/issues/114 [z3] [AUFNIRA]
Z3Prover/z3#3052 [z3] [LIA]
Z3Prover/z3#3058 [z3] [QF_BVFP]
Z3Prover/z3#3068 [z3] [UF]
SRI-CSL/yices2#169 [yices] [QF_UFIDL]
SRI-CSL/yices2#170 [yices] [QF_NRA]
Z3Prover/z3#2994 [z3str3] [QF_S]
Z3Prover/z3#3031 [z3str3] [QF_S]
Z3Prover/z3#2916 [z3] [QF_S]
Z3Prover/z3#2925 [z3] [QF_FP]
Z3Prover/z3#3040 [z3] [QF_BV]
Z3Prover/z3#3096 [z3] [QF_NIA]
Z3Prover/z3#3256 [z3] [AUFNIRA]
Z3Prover/z3#3822 [z3] [BV]
Z3Prover/z3#3948 [z3] [AUFDTLIA]
Z3Prover/z3#3949 [z3] [QF_UFLRA]
Z3Prover/z3#4590 [z3str3] [QF_S]
SRI-CSL/yices2#280 [yices] [QF_NRA]

Reproducing bugs used in the evaluation section of our ESEC/FSE 2020 paper:

Please follow the instructions here.