EBF
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.
SYSTEM REQUIREMENTS:
- 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
INSTALLATION:
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
SUPPORTING TOOLS:
A) Fuzzing engine:
- afl++ (Apache License)
B) BMC engine:
- ESBMC (Apache License)
- CBMC v 5.44.0 (BSD 4-Clause License)
- CSEQ (BSD 3-Clause License)
- Deagle (GPLv3)
HOW TO RUN
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:
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.