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/*.so to /usr/local/lib/
    • or you can build and install z3 according to Building Z3 using make and GCC/Clang
  • For MacOS, it is similar to Linux.
• 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 buildExtension under 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 -import -postScript BinAbsInspector “@@”

<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
[-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 Manager and find BinAbsInspector.java
  • Double-click on BinAbsInspector.java entry, 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 git@github.com:KeenSecurityLab/BinAbsInspector.git
cd BinAbsInspector
docker build . -t bai
docker run -v $(pwd):/data/workspace bai “@@

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.