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](https://keenlab.tencent.com/). 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](https://github.com/NationalSecurityAgency/ghidra#install)
+ 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](https://github.com/Z3Prover/z3/releases), 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:
1. You can download suitable pre-build package from [here](https://github.com/Z3Prover/z3/releases), extract the zip file and copy `z3-${version}-win/bin/*.so` to `/usr/local/lib/`
2. or you can build and install z3 according to [Building Z3 using make and GCC/Clang](https://github.com/Z3Prover/z3#building-z3-using-make-and-gccclang)
+ For MacOS, it is similar to Linux.
+ Download the extension zip file from [release page](https://github.com/KeenSecurityLab/BinAbsInspector/releases)
+ Install the extension according to [Ghidra Extension Notes](https://ghidra-sre.org/InstallationGuide.html#GhidraExtensionNotes)
# Building
Build the extension by yourself, if you want to develop a new feature, please refer to [development guide](https://github.com/KeenSecurityLab/BinAbsInspector/wiki/Developer-Guide).
| `[-callStringK <callStringMaxLen>]` | Call string maximum length [K](https://github.com/KeenSecurityLab/BinAbsInspector/wiki/Technical-Details#context)|
| `[-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
1. Run Ghidra and import the target binary into a project
2. Analyze the binary with default settings
3. When the analysis is done, open `Window -> Script Manager` and find `BinAbsInspector.java`
4. Double-click on `BinAbsInspector.java` entry, set the parameters in configuration window and click OK
5. 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
The structure of this project is as follows, please refer to [technical details](https://github.com/KeenSecurityLab/BinAbsInspector/wiki/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](https://ghidra-sre.org/) as our foundation and frequently leverage [JImmutable Collections](http://brianburton.github.io/java-immutable-collections/) for better performance.
Here we would like to thank them for their great help!
