Skip to main content

A fuzzing framework for SMT solvers

Project description

portfolio_view


yinyang

A fuzzing framework for SMT solvers. Given a set of seed SMT formulas, yinyang generates mutant formulas to stress-test SMT solvers. yinyang can be used to robustify SMT solvers. It already found 1,500+ bugs in the two state-of-the-art SMT solvers Z3 and CVC4.

Installation

To install a stable version of yinyang use:

pip3 install yinyang

To install the most recent version, check out the repository:

git clone https://github.com/testsmt/yinyang.git                        
pip3 install antlr4-python3-runtime==4.9.2                                   

Note that you may want to add yinyang/bin to your PATH, for running yinyang conveniently without prefix.

Usage

  1. Get SMT-LIB 2 benchmarks. Edit scripts/SMT-LIB-clone.sh to select the logics for testing. Run ./scripts/SMT-LIB-clone.sh to download the corresponding SMT-LIB 2 benchmarks. Alternatively, you can download benchmarks directly from the SMT-LIB website or supply your own benchmarks.

  2. Get and build SMT solvers for testing. Install two or more SMT solvers that support the SMT-LIB 2 format. You may find it convenient to add them to your PATH.

  3. Run yinyang on the benchmarks e.g. with Z3 and CVC4.

typefuzz "z3 model_validate=true;cvc4 --check-models -m -i -q" benchmarks 

yinyang will by default randomly select formulas from the folder ./benchmarks and generate 300 mutants per seed formula. If a bug has been found, the bug trigger is stored in ./bugs. yinyang will run in an infinite loop. You can use the shortcut CTRL+C to terminate yinyang manually.

📘 Documentation

Feedback

For bugs/issues/questions/feature requests please file an issue. We are always happy to receive your feedback or help you adjust yinyang to the needs of your custom solver, help you build on yinyang, etc.

📬 Contact us

Additional Resources

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

yinyang-0.3.0.tar.gz (109.2 kB view details)

Uploaded Source

Built Distribution

yinyang-0.3.0-py3-none-any.whl (146.6 kB view details)

Uploaded Python 3

File details

Details for the file yinyang-0.3.0.tar.gz.

File metadata

  • Download URL: yinyang-0.3.0.tar.gz
  • Upload date:
  • Size: 109.2 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/3.4.2 importlib_metadata/4.6.1 pkginfo/1.7.1 requests/2.24.0 requests-toolbelt/0.9.1 tqdm/4.61.2 CPython/3.6.9

File hashes

Hashes for yinyang-0.3.0.tar.gz
Algorithm Hash digest
SHA256 f0a5033d2c56909945bcd8e3cca7e0a6b721a2b5cca83fe1297ff526778d8ef9
MD5 921a4090e521855f253404dcbb792283
BLAKE2b-256 5f454a765c7814cfe5f8d1fe00720caa9fca93c2cd08c629b5c3771aa523d9a6

See more details on using hashes here.

File details

Details for the file yinyang-0.3.0-py3-none-any.whl.

File metadata

  • Download URL: yinyang-0.3.0-py3-none-any.whl
  • Upload date:
  • Size: 146.6 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/3.4.2 importlib_metadata/4.6.1 pkginfo/1.7.1 requests/2.24.0 requests-toolbelt/0.9.1 tqdm/4.61.2 CPython/3.6.9

File hashes

Hashes for yinyang-0.3.0-py3-none-any.whl
Algorithm Hash digest
SHA256 21b26361976e514f7e0241a1ae7b3e1fda40f88b96b3f6fde621d3b80e8d986a
MD5 a2bbfb8356c96deaa882f014b045cc48
BLAKE2b-256 4e9bf8ed61e1440e761cacec2fcc7f11af51c1e094fde2de7caebff72c9e0291

See more details on using hashes here.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Pingdom Monitoring Sentry Error logging StatusPage Status page