This tool attempts to improve the efficiency of symbolic execution technique and use it to detect heap overflow vulnerability in binary programs. Instead of applying symbolic execution to the whole program, this tool initially determines a program test unit probably containing vulnerability using static analysis and based on the specification of heap overflow vulnerability. Then the constraint tree of the program unit is extracted using symbolic execution such that every node in this constraint tree contains the desired path and vulnerability constraints. Finally, using the curve fitting technique and treatment learning, the system inputs are estimated consistent with these constraints. Thus, new inputs are generated that reach the vulnerable instructions in the desired unit from the beginning of the program and cause heap overflow in those instructions.
For more information, see the paper "A Unit-Based Symbolic Execution Method for Detecting Heap Overflow Vulnerability in Executable Codes" presented at the Tests and Proofs (TAP) 2022 conference.
- Static Analysis on x64 Binary Codes for Finding Possibly Vulnerable Units
- Symbolic Execution on Test Units
- Monte Carlo Simulation and Curve Fitting
- Detecting Heap Overflow Vulnerability and Generating Appropriate Inputs for Vulnerability Activation
- Python3
- angr Framework (Installation)
Create and activate a virtual environment:
sudo apt-get install virtualenv
virtualenv -p /usr/bin/python3 env
source env/bin/activate
git clone https://github.com/SoftwareSecurityLab/Heap-Overflow-Detection
cd Heap-Overflow-Detection
Now install project requirements using requirements.txt file:
pip install -r requirements.txt
Everything is completed. Now you can test your desired code using our tool. We put some test cases from the NIST SARD benchmark vulnerable programs in this repository which you can use these test cases.
-h or --help HELP
-b or --binary BINARY [The Name of Binary File You Want to Analyze]
-p or --prototype PROTOTYPE [The Prototype of Test Unit You Want to Analyze]
-s or --sizes SIZES [The Size of Test Unit Arguments]
-a or --args ARGS [The Indexes of Argv Passed to The Test Unit As Function Arguments]
-S or --solo SOLO [The Solo Mode Avoids Executing Nested Functions in Unit Symbolically]
cd Project_Files; chmod +x run.py
You can see possibly vulnerable units in binary program which are need to be analyzed:
gcc ./samples/program.c -o program; ./run.py -b program
For example, you want to analyze the function "signup" as a vulnerable unit:
We need two arguments with the maximum length of 100 as the inputs of "scanf" function, which activate the possible vulnerabilities in the "signup" unit, so we use -s 100,100 for the sizes option.
./run.py -b program -p 'void signup(char*,char*)' -s 100,100 --solo
If you want to analyze the function "authentication" as a vulnerable unit:
We need two arguments with the maximum length of 100 as the inputs of argv, which activate the possible vulnerabilities in the "authentication" unit, so we use -s 100,100 for the sizes option and also since the argv[1] and argv[2] have been passed to the test unit, we use -a 1,2 for the args option.
./run.py -b program -p 'void authentication(char*,char*)' -s 100,100 -a 1,2 --solo
We wish you happy testing!😄
You may get the message "node i is not satisfiable" since the detection tool can not generate appropriate input data if the symbolic buffer does not have enough space to hold the generated input. In this situation, you have to increase the value of parameters in the config.py file.
- Maryam Mouzarani - maryam-mouzarani
- Ali Kamali - alikmli
- Sara Baradaran - SaraBaradaran
- Mahdi Heidari - mheidari98
This project is licensed under the Apache License 2.0 - see the LICENSE file for details
We have tested our project on Ubuntu 18.04.1 LTS.
