An Esemble Verification Tool for Finding Software Vulnerabilities in IoT Concurent programs

EBF is a tool that combines "Bounded Model Checking (BMC)" and AFL "Fuzzing" techniques to verify and detect security vulnerabilities in concurrent programs.

1. python v3
2. llvm clang 11

To Install clang-11 package for ubuntu-18.04:

sudo apt-get install clang-tools-11

3- To use Deagle you need bison and flex packages:

sudo apt-get install -y bison

sudo apt-get -y install flex

Clone EBF package and make sure SYSTEM REQUIREMENTS are correctly satisfied.

Then install the depindencies :

EBF_LLVM_CONFIG=llvm-config LLVM_CC=clang LLVM_CXX=clang++ ./bootstrap.sh

1. afl++ (Apache License)

AFL TOOL URL

1. ESBMC (Apache License)

ESBMC TOOL URL

2. CBMC v 5.44.0 (BSD 4-Clause License)

CBMC TOOL URL

3. CSEQ (BSD 3-Clause License)

CSEQ TOOL URL

4. Deagle (GPLv3)

Deagle TOOL URL

Before running the tool for the first time, please log in as root and temporarily modify the core_pattern as:

sudo echo core >/proc/sys/kernel/core_pattern

To run the tool:

./scripts/RunEBF.py -a 32|64 -c -p property-file benchmark

For example:

./scripts/RunEBF.py -a 32 -p property-file/reach benchmarks/pthread/bigshot_p.c

A demonistration vedio of how to use the tool:

EBF Demonistration

Ps. The tool is still under development and it works perfectly on Ubuntu 18.4 running on macOS machine. Please, raise an issue if you have difficulty running the tool.