GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → Practical-Formal-Methods → Storm

Practical-Formal-Methods / Storm

Licence: apache-2.0
A blackbox mutational fuzzer for detecting critical bugs in SMT solvers

Labels

testingfuzzingsmt

Projects that are alternatives of or similar to Storm

Reconftw
reconFTW is a tool designed to perform automated recon on a target domain by running the best set of tools to perform scanning and finding out vulnerabilities
Stars: ✭ 974 (+1132.91%)
Mutual labels:  fuzzing
Book
📖 Guides and tutorials on how to fuzz Rust code
Stars: ✭ 67 (-15.19%)
Mutual labels:  fuzzing
Testing Distributed Systems
Curated list of resources on testing distributed systems
Stars: ✭ 1,187 (+1402.53%)
Mutual labels:  fuzzing
Afl Compiler Fuzzer
Variation of american fuzzy lop for testing compilers for C-like languages, revised by Alex Groce & collaborators to fuzz tools processing source code in C-like languages
Stars: ✭ 47 (-40.51%)
Mutual labels:  fuzzing
Erlamsa
Erlang port of famous radamsa fuzzzer.
Stars: ✭ 56 (-29.11%)
Mutual labels:  fuzzing
Randomjson
Provides a Kotlin/Java library to create a random json string
Stars: ✭ 70 (-11.39%)
Mutual labels:  fuzzing
Baresifter
A bare-metal x86 instruction set fuzzer a la Sandsifter
Stars: ✭ 33 (-58.23%)
Mutual labels:  fuzzing
Optee fuzzer
This repository contains the code for a fuzzing prototype for the OP-TEE system call interface using AFL.
Stars: ✭ 78 (-1.27%)
Mutual labels:  fuzzing
Honeybee
An experimental high performance, fuzzing oriented Intel Processor Trace capture and analysis suite
Stars: ✭ 63 (-20.25%)
Mutual labels:  fuzzing
Nopol
Automatic program repair and patch generation system for Java based on dynamic analysis and code synthesis with SMT, developed at University of Lille and Inria, France.
Stars: ✭ 73 (-7.59%)
Mutual labels:  smt
Dockerized fuzzing
Run fuzzing experiments in Docker
Stars: ✭ 48 (-39.24%)
Mutual labels:  fuzzing
Rfsec Toolkit
RFSec-ToolKit is a collection of Radio Frequency Communication Protocol Hacktools.无线通信协议相关的工具集，可借助SDR硬件+相关工具对无线通信进行研究。Collect with ♥ by HackSmith
Stars: ✭ 1,085 (+1273.42%)
Mutual labels:  fuzzing
Dreal4
SMT Solver for Nonlinear Theories of Reals
Stars: ✭ 72 (-8.86%)
Mutual labels:  smt
Afl.rs
🐇 Fuzzing Rust code with American Fuzzy Lop
Stars: ✭ 1,013 (+1182.28%)
Mutual labels:  fuzzing
Afl Patches
Patches to afl to fix bugs or add enhancements
Stars: ✭ 76 (-3.8%)
Mutual labels:  fuzzing
Example Go
Go Fuzzit Example
Stars: ✭ 39 (-50.63%)
Mutual labels:  fuzzing
Elmyr
A utility to make Kotlin/Java tests random yet reproducible
Stars: ✭ 68 (-13.92%)
Mutual labels:  fuzzing
Brundlefuzz
BrundleFuzz is a distributed fuzzer for Windows and Linux using dynamic binary instrumentation.
Stars: ✭ 78 (-1.27%)
Mutual labels:  fuzzing
Awesome Directed Fuzzing
A curated list of awesome directed fuzzing research papers
Stars: ✭ 77 (-2.53%)
Mutual labels:  fuzzing
Boofuzz
A fork and successor of the Sulley Fuzzing Framework
Stars: ✭ 1,180 (+1393.67%)
Mutual labels:  fuzzing
View All Similar Projects ➔

logo

Python application Python package

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.

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

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

Please follow the instructions here.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].