binsec/haunted

1. This repository is an OCaml binary-analysis platform centered on the binsec executable. Binsec/Haunted extends the original Binsec stack with speculative-constant-time analysis, especially for Spectre-PHT and Spectre-STL. The architecture is organized as a pipeline from binary loading and disassembly into a common intermediate form, then into several analysis engines.

2. The front end starts in src/main.ml and the various *_options.ml modules. Command-line configuration is split by subsystem: loader, disassembly, static analysis, dynamic analysis, formula/SMT, relational symbolic execution, server, and examples. Policy files under src/policy/ steer security-oriented analyses.

3. Binary ingestion is handled by src/loader/. It provides format-specific loaders for ELF and PE, plus buffer/dump utilities. This layer abstracts file format details and produces the program representation consumed by later stages.

4. Disassembly and lifting live under src/disasm/. Architecture-specific decoders exist for x86, ARM, and RISC-V, and the output is translated into DBA, the project’s main low-level intermediate representation. The disassembler also builds control-flow information and performs simplification passes over DBA.

5. DBA is defined in src/dba/ and is the shared semantic backbone of the whole system. It provides instruction and expression types, visitors, printers, utilities, and conversion to formulas. Most higher-level analyses operate over DBA rather than raw machine code.

6. Static reasoning is split across src/static/, including abstract interpretation, simulation, and concrete execution helpers. This subsystem provides domain implementations such as intervals, taint, and reduced products, plus normalization and backward analysis. It is the main boundary for over-approximating program behavior.

7. The Haunted-specific core is in src/relse/. This is the relational symbolic execution engine that models pairs of executions, memory, paths, symbolic terms, and security/insecurity checks. Its submodules for symbolic state, SMT interaction, and insecurity detection are the critical architectural center for speculative-attack analysis.

8. Dynamic analysis is under src/dynamic/ and is structured around trace loading, post-processing, tainting, and dynamic symbolic execution. The dse/path_exploration/ subtree contains exploration strategies, trace/tree management, symbolic inputs, and vulnerability-oriented criteria such as UAF and EIP-rewrite guides. This layer is where runtime observations and trace-driven exploration feed back into analysis.

9. Formula and solver support are isolated in src/formula/ and src/smtlib/. They translate internal formulas to and from SMT-LIB, manage solver interaction, and provide proof/checking utilities. This is the boundary to external SMT solvers such as Boolector, Z3, Yices, or CVC4 mentioned in the README.

10. src/ast/, src/kernel/, src/base/, and src/utils/ provide the shared infrastructure: graph structures, common types, logging, bitvectors, worklists, file and string helpers, instruction/mnemonic abstractions, and generic CFG utilities. These packages are used across every major subsystem and keep the analysis engines decoupled from low-level implementation details.

11. The repository also includes specialized support modules: src/dwarf/ for debug information, src/ida/ for IDA Pro integration, src/llvm/ for LLVM-related decoding/transfer functions, and src/xtrasec/ plus src/sse/ for additional symbolic-security workflows. These are peripheral integrations rather than the main analysis path.

12. External interfaces and tooling are exposed through protobuf definitions in src/proto/, a server layer in src/server/, and example binaries under src/examples/ and src/unittests/. The build is an OCaml/Make/autoconf stack, with generated parsers/lexers (menhir, ocamllex) and solver backends as the main external dependencies.

13. The main data flow to diagram is: binary + options/policy → loader → disassembler/lifter → DBA → selected analysis engine (static, dynamic, or relational symbolic execution) → formula/SMT solving → vulnerability report, trace, or server response. Haunted’s unique contribution sits in the relse path, where pairs of symbolic executions are compared to detect speculative leakage.