EBF (Ensemble Bounded Model Checking - Fuzzing) is a tool that combines "Bounded Model Checking (BMC)" and AFL "Fuzzing" techniques to verify and detect security vulnerabilities in concurrent programs. In contrast with portfolios, which simply run all possible techniques in parallel, EBF strives to obtain closer cooperation between them. This goal is achieved in a black-box fashion. On the one hand, the model checkers are forced to provide seeds to the fuzzers by injecting additional vulnerabilities in the program under test. On the other hand, off-the-shelf fuzzers are forced to explore different interleavings by adding lightweight instrumentation and systematically re-seeding them.

To compile and run EBF, please refer to the following system requirements and installation instructions. We recommend starting by reading some of the publications to gain a clear understanding of what this tool can offer, as outlined in references 1 and 2.

The figure below illustrates the current EBF architecture. The tool takes a C/C++ program as input and employs the BMC engine to perform safety proving up to a 'k' bound. Then, we inject errors into the program during (stage 2), generating seeds (inputs) extracted from the BMC engine used in the fuzzing phase (stage 3). Finally, the results are aggregated to produce the final verdict, along with the generation of a witness file.

EBF contains an open-source concurrency fuzzer that verifies concurrent programs by injecting delays controlled randomly by the fuzzer. EBF can find different concurrency-related and memory-related bugs, such as:

Memory-related

• User-specified assertion failures

• Out-of-bounds array access

• Illegal pointer dereferences

• Memory leaks

Concurrency-related

• Deadlock

• Data race

• Thread leak

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 dependencies :

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 demonstration video of how to use the tool:

EBF Demonistration