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.
![Screenshot 2024-01-07 at 1 47 04 PM](https://private-user-images.githubusercontent.com/47563480/294752752-bea4e63a-c8de-4ce7-a7af-1ebf40550215.png?jwt=eyJhbGciOiJIUzI1NiIsInR5cCI6IkpXVCJ9.eyJpc3MiOiJnaXRodWIuY29tIiwiYXVkIjoicmF3LmdpdGh1YnVzZXJjb250ZW50LmNvbSIsImtleSI6ImtleTUiLCJleHAiOjE3MjQyNjg4ODAsIm5iZiI6MTcyNDI2ODU4MCwicGF0aCI6Ii80NzU2MzQ4MC8yOTQ3NTI3NTItYmVhNGU2M2EtYzhkZS00Y2U3LWE3YWYtMWViZjQwNTUwMjE1LnBuZz9YLUFtei1BbGdvcml0aG09QVdTNC1ITUFDLVNIQTI1NiZYLUFtei1DcmVkZW50aWFsPUFLSUFWQ09EWUxTQTUzUFFLNFpBJTJGMjAyNDA4MjElMkZ1cy1lYXN0LTElMkZzMyUyRmF3czRfcmVxdWVzdCZYLUFtei1EYXRlPTIwMjQwODIxVDE5Mjk0MFomWC1BbXotRXhwaXJlcz0zMDAmWC1BbXotU2lnbmF0dXJlPTI4OGQ1OTIxOTU1MWE0NDZjZDZkZGMxMGZkNjBmYWEzNjhmNzM5ZTk5NWJjNjcwNjlmNDI5NWNjODA5MzBlMTImWC1BbXotU2lnbmVkSGVhZGVycz1ob3N0JmFjdG9yX2lkPTAma2V5X2lkPTAmcmVwb19pZD0wIn0.mpv5DbJiRs0CcRqHzQiPGK88am5C0HYOSseT_bGQfi4)
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
- python v3
- 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
- afl++ (Apache License)
- ESBMC (Apache License)
- CBMC v 5.44.0 (BSD 4-Clause License)
- CSEQ (BSD 3-Clause License)
- Deagle (GPLv3)
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: