The SBA framework is currently undergoing a significant overhaul:
-
Architecture & Robustness
- Disassembler: Develop a robust, architecture-agnostic disassembler leveraging LLVM MC for high-fidelity binary analysis. Support static analysis directly on raw bytes, bypassing the inherent flaws of traditional disassembly techniques.
- Binary Loading: Integrate LLVMObject for reliable, cross-platform support of ELF, PE, and Mach-O executable formats.
- Lifting: Implement a high-performance C++ lifter to replace the legacy OCaml pipeline.
-
Framework Capabilities
- ControlFlowGraphAPI: Support diverse graph types and construction strategies.
-
AnalysisAPI: Allow seamless integration of forward and backward dataflow analysis.
-
Pre-Disassembly Analysis [1]: Analyze raw bytes, breaking the circular dependency between binary analysis and traditional disassembly, and bypassing inherent flaws to provide high-fidelity results. The approach scales linearly, computing results for every byte offset of an
$n$ -byte binary in$O(n)$ time. - Abstract Interpretation [2] [3] [4] [5]: A foundational technique in program analysis that forms the basis of modern static binary analysis. By evaluating programs over abstract domains, this engine allows the framework to model all possible execution paths without running the code.
-
Pre-Disassembly Analysis [1]: Analyze raw bytes, breaking the circular dependency between binary analysis and traditional disassembly, and bypassing inherent flaws to provide high-fidelity results. The approach scales linearly, computing results for every byte offset of an
-
Applications
-
Jump Table Analysis
- Improve bounds analysis
-
Function Property Check
- Callee-Saved Registers Preservation
- Invalid Pointer Dereference
-
Non-Returning Call Analysis
- Without relying on catalogs of non-returning functions.
-
Jump Table Analysis
SBA requires a C++23 compiler (GCC/Clang), CMake, and OCaml. We recommend using Opam to manage the OCaml environment, as it ensures compatibility across different Linux distributions.
# Fedora/RHEL
sudo dnf install clang make cmake ninja-build opam patch
# Ubuntu/Debian
sudo apt-get install clang make cmake ninja-build opamInitialize Opam and create a switch for OCaml 4.14 (required for the legacy lifter):
opam init
opam switch create sba 4.14.2
eval $(opam env)
opam install camlp4 ocamlfindmkdir build && cd build
cmake .. -G Ninja -DCMAKE_CXX_COMPILER=clang++
ninja -j $(nproc)To analyze a binary object ~/obj, use the following command:
./tools/jump_table x86_64.auto ~/obj
By default, SBA creates temporary files and outputs result in /tmp/sba/. These paths can be specified using -d and -o as follows:
./tools/jump_table -d /tmp/sba/ -o /tmp/sba/result x86_64.auto ~/obj
- Analyzing Bytes: Pre-Disassembly Static Binary Analysis (PLDI 2026)
- Scalable, Sound, and Accurate Jump Table Analysis (ISSTA 2024)
- Accurate Disassembly of Complex Binaries Without Use of Compiler Metadata (ASPLOS 2023)
- SAFER: Efficient and Error-Tolerant Binary Instrumentation (USENIX 2023)
- Practical fine-grained binary code randomization (ACSAC 2020)