What is BinAbsInspector?
BinAbsInspector (Binary Abstract Inspector) is a static analyzer for automated reverse engineering and scanning vulnerabilities in binaries, which is a long-term research project incubated at Keenlab. It is based on abstract interpretation with the support from Ghidra. It works on Ghidra's Pcode instead of assembly. Currently it supports binaries on x86,x64, armv7 and aarch64.
Installation
- Install Ghidra according to Ghidra's documentation
- Install Z3 (tested version: 4.8.15)
- Note that generally there are two parts for Z3 library: one is Java package, the other one is native library. The Java package is already included in "/lib" directory, but we suggest that you replace it with your own Java package for version compatibility.
- For Windows, download a pre-built package from here, extract the zip file and add a PATH environment variable pointing to
z3-${version}-win/bin - For Linux, install with package manager is NOT recommended, there are two options:
- You can download suitable pre-build package from here, extract the zip file and copy
z3-${version}-win/bin/*.soto/usr/local/lib/ - or you can build and install z3 according to Building Z3 using make and GCC/Clang
- You can download suitable pre-build package from here, extract the zip file and copy
- For MacOS, it is similar to Linux.
- For Windows, download a pre-built package from here, extract the zip file and add a PATH environment variable pointing to
- Download the extension zip file from release page
- Install the extension according to Ghidra Extension Notes
Building
Build the extension by yourself, if you want to develop a new feature, please refer to development guide.
- Install Ghidra and Z3
- Install Gradle 7.x (tested version: 7.4)
- Pull the repository
- Run
gradle buildExtensionunder repository root - The extension will be generated at
dist/${GhidraVersion}_${date}_BinAbsInspector.zip
Usage
You can run BinAbsInspector in headless mode, GUI mode, or with docker.
- With Ghidra headless mode.
$GHIDRA_INSTALL_DIR/support/analyzeHeadless <projectPath> <projectName> -import <file> -postScript BinAbsInspector "@@<scriptParams>"
<projectPath> -- Ghidra project path.
<projectName> -- Ghidra project name.
<scriptParams> -- The argument for our analyzer, provides following options:
| Parameter | Description |
|---|---|
[-K <kElement>] |
KSet size limit K |
[-callStringK <callStringMaxLen>] |
Call string maximum length K |
[-Z3Timeout <timeout>] |
Z3 timeout |
[-timeout <timeout>] |
Analysis timeout |
[-entry <address>] |
Entry address |
[-externalMap <file>] |
External function model config |
[-json] |
Output in json format |
[-disableZ3] |
Disable Z3 |
[-all] |
Enable all checkers (by default) |
[-debug] |
Enable debugging log output |
[-check "<cweNo1>[;<cweNo2>...]"] |
Enable specific checkers |
-
With Ghidra GUI
- Run Ghidra and import the target binary into a project
- Analyze the binary with default settings
- When the analysis is done, open
Window -> Script Managerand findBinAbsInspector.java - Double-click on
BinAbsInspector.javaentry, set the parameters in configuration window and click OK - When the analysis is done, you can see the CWE reports in console window, double-click the addresses from the report can jump to corresponding address
-
With Docker
git clone [email protected]:KeenSecurityLab/BinAbsInspector.git
cd BinAbsInspector
docker build . -t bai
docker run -v $(pwd):/data/workspace bai "@@<script parameters>" -import <file>
Implemented Checkers
So far BinAbsInspector supports following checkers:
- CWE78 (OS Command Injection)
- CWE119 (Buffer Overflow (generic case))
- CWE125 (Buffer Overflow (Out-of-bounds Read))
- CWE134 (Use of Externally-Controlled Format string)
- CWE190 (Integer overflow or wraparound)
- CWE367 (Time-of-check Time-of-use (TOCTOU))
- CWE415 (Double free)
- CWE416 (Use After Free)
- CWE426 (Untrusted Search Path)
- CWE467 (Use of sizeof() on a pointer type)
- CWE476 (NULL Pointer Dereference)
- CWE676 (Use of Potentially Dangerous Function)
- CWE787 (Buffer Overflow (Out-of-bounds Write))
Project Structure
The structure of this project is as follows, please refer to technical details for more details.
├── main
│ ├── java
│ │ └── com
│ │ └── bai
│ │ ├── checkers checker implementatiom
│ │ ├── env
│ │ │ ├── funcs function modeling
│ │ │ │ ├── externalfuncs external function modeling
│ │ │ │ └── stdfuncs cpp std modeling
│ │ │ └── region memory modeling
│ │ ├── solver analyze core and grpah module
│ │ └── util utilities
│ └── resources
└── test
You can also build the javadoc with gradle javadoc, the API documentation will be generated in ./build/docs/javadoc.
Acknowledgement
We employ Ghidra as our foundation and frequently leverage JImmutable Collections for better performance.
Here we would like to thank them for their great help!
