# binsec/haunted architecture

> Architecture diagram of the GitHub repository binsec/haunted, generated by GitDiagram from its file tree, README and a sample of source files (last updated 2026-06-27). It is an AI-made overview: check details against the source.

- Interactive diagram: https://gitdiagram.com/binsec/haunted
- Repository: https://github.com/binsec/haunted

## Overview

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.

Main entry points: [`src/main.ml`](https://github.com/binsec/haunted/blob/master/src/main.ml) (binsec), [`src/disasm`](https://github.com/binsec/haunted/tree/master/src/disasm) (Disassembler), [`src/formula`](https://github.com/binsec/haunted/tree/master/src/formula) (Formula), [`src/relse`](https://github.com/binsec/haunted/tree/master/src/relse) (RelSE)

## Diagram (Mermaid)

```mermaid
flowchart TD

subgraph group_frontend["Frontend"]
  node_main(("binsec<br/>entrypoint<br/>[main.ml]"))
  node_options["Options<br/>cli config"]
  node_policy["Policies<br/>security policy"]
end

subgraph group_core["Core IR"]
  node_loader["Loader<br/>binary ingest"]
  node_disasm["Disassembler<br/>decode lift"]
  node_dba{{"DBA<br/>ir"}}
end

subgraph group_analysis["Analysis"]
  node_static["Static AI<br/>abstract interpretation"]
  node_relse["RelSE<br/>relational symbolic exec"]
  node_dynamic["Dynamic DSE<br/>trace-driven analysis"]
  node_formula["Formula"]
  node_smtlib["SMT-LIB<br/>solver bridge"]
end

subgraph group_infra["Infrastructure"]
  node_ast{{"Graphs<br/>cfg/ast"}}
  node_kernel["Kernel<br/>core services"]
  node_base["Base<br/>foundation libs"]
  node_utils["Utils<br/>misc helpers"]
end

subgraph group_integrations["Integrations"]
  node_server["Server"]
  node_proto["Proto<br/>rpc schema"]
  node_examples["Examples<br/>workflows"]
  node_special["Specialized<br/>extensions"]
end

node_main -->|"loads"| node_options
node_main -->|"invokes"| node_loader
node_main -->|"invokes"| node_disasm
node_main -->|"invokes"| node_static
node_main -->|"invokes"| node_relse
node_main -->|"invokes"| node_dynamic
node_main -->|"serves"| node_server
node_options -->|"configures"| node_policy
node_loader -->|"feeds"| node_disasm
node_disasm -->|"lifts"| node_dba
node_disasm -->|"builds"| node_ast
node_dba -->|"converts"| node_formula
node_static -->|"analyses"| node_dba
node_dynamic -->|"executes"| node_dba
node_relse -->|"models"| node_dba
node_relse -->|"emits"| node_formula
node_formula -->|"exports"| node_smtlib
node_smtlib -->|"imports"| node_formula
node_formula -->|"solves"| node_relse
node_dynamic -->|"reports"| node_server
node_proto -->|"describes"| node_server
node_examples -->|"demonstrates"| node_dynamic
node_special -.->|"extends"| node_disasm
node_special -.->|"extends"| node_formula
node_ast -->|"uses"| node_utils
node_kernel -->|"builds on"| node_base
node_loader -->|"uses"| node_base
node_disasm -->|"uses"| node_utils
node_static -->|"uses"| node_kernel
node_dynamic -->|"uses"| node_kernel
node_relse -->|"uses"| node_kernel

click node_main "https://github.com/binsec/haunted/blob/master/src/main.ml"
click node_options "https://github.com/binsec/haunted/tree/master/src"
click node_policy "https://github.com/binsec/haunted/tree/master/src/policy"
click node_loader "https://github.com/binsec/haunted/tree/master/src/loader"
click node_disasm "https://github.com/binsec/haunted/tree/master/src/disasm"
click node_dba "https://github.com/binsec/haunted/tree/master/src/dba"
click node_static "https://github.com/binsec/haunted/tree/master/src/static"
click node_relse "https://github.com/binsec/haunted/tree/master/src/relse"
click node_dynamic "https://github.com/binsec/haunted/tree/master/src/dynamic"
click node_formula "https://github.com/binsec/haunted/tree/master/src/formula"
click node_smtlib "https://github.com/binsec/haunted/tree/master/src/smtlib"
click node_server "https://github.com/binsec/haunted/tree/master/src/server"
click node_proto "https://github.com/binsec/haunted/tree/master/src/proto"
click node_examples "https://github.com/binsec/haunted/tree/master/src/examples"
click node_special "https://github.com/binsec/haunted/tree/master/src"
click node_ast "https://github.com/binsec/haunted/tree/master/src/ast"
click node_kernel "https://github.com/binsec/haunted/tree/master/src/kernel"
click node_base "https://github.com/binsec/haunted/tree/master/src/base"
click node_utils "https://github.com/binsec/haunted/tree/master/src/utils"

classDef toneNeutral fill:#f8fafc,stroke:#334155,stroke-width:1.5px,color:#0f172a
classDef toneBlue fill:#dbeafe,stroke:#2563eb,stroke-width:1.5px,color:#172554
classDef toneAmber fill:#fef3c7,stroke:#d97706,stroke-width:1.5px,color:#78350f
classDef toneMint fill:#dcfce7,stroke:#16a34a,stroke-width:1.5px,color:#14532d
classDef toneRose fill:#ffe4e6,stroke:#e11d48,stroke-width:1.5px,color:#881337
classDef toneIndigo fill:#e0e7ff,stroke:#4f46e5,stroke-width:1.5px,color:#312e81
classDef toneTeal fill:#ccfbf1,stroke:#0f766e,stroke-width:1.5px,color:#134e4a
class node_main,node_options,node_policy toneBlue
class node_loader,node_disasm,node_dba toneAmber
class node_static,node_relse,node_dynamic,node_formula,node_smtlib toneMint
class node_ast,node_kernel,node_base,node_utils toneRose
class node_server,node_proto,node_examples,node_special toneIndigo
```

## Components

### Frontend

CLI, configuration, and orchestration entrypoints

- [binsec](https://github.com/binsec/haunted/blob/master/src/main.ml): entrypoint · Main executable and top-level orchestration · `src/main.ml`
- [Options](https://github.com/binsec/haunted/tree/master/src): cli config · Subsystem-specific command-line configuration · `src`
- [Policies](https://github.com/binsec/haunted/tree/master/src/policy): security policy · Policy files steering security-oriented analyses · `src/policy`

### Core IR

Shared program representation and lowering pipeline

- [Loader](https://github.com/binsec/haunted/tree/master/src/loader): binary ingest · ELF/PE loading and buffer/dump abstraction · `src/loader`
- [Disassembler](https://github.com/binsec/haunted/tree/master/src/disasm): decode lift · Architecture decoding, CFG recovery, and DBA lowering · `src/disasm`
- [DBA](https://github.com/binsec/haunted/tree/master/src/dba): ir · Shared low-level intermediate representation · `src/dba`

### Analysis

Static, dynamic, and relational analysis engines

- [Static AI](https://github.com/binsec/haunted/tree/master/src/static): abstract interpretation · Over-approximate reasoning, simulation, and concrete helpers · `src/static`
- [RelSE](https://github.com/binsec/haunted/tree/master/src/relse): relational symbolic exec · Haunted core for pairwise symbolic execution and speculative checks · `src/relse`
- [Dynamic DSE](https://github.com/binsec/haunted/tree/master/src/dynamic): trace-driven analysis · Trace loading, tainting, and dynamic symbolic execution · `src/dynamic`
- [Formula](https://github.com/binsec/haunted/tree/master/src/formula): formula bridge · Internal formula construction, transforms, and proving support · `src/formula`
- [SMT-LIB](https://github.com/binsec/haunted/tree/master/src/smtlib): solver bridge · SMT-LIB parsing, printing, and solver-facing utilities · `src/smtlib`

### Infrastructure

Common libraries and shared runtime support

- [Graphs](https://github.com/binsec/haunted/tree/master/src/ast): cfg/ast · Control-flow graph and instruction graph helpers · `src/ast`
- [Kernel](https://github.com/binsec/haunted/tree/master/src/kernel): core services · Shared kernel abstractions and global options · `src/kernel`
- [Base](https://github.com/binsec/haunted/tree/master/src/base): foundation libs · Common types, logging, bitvectors, worklists, and utilities · `src/base`
- [Utils](https://github.com/binsec/haunted/tree/master/src/utils): misc helpers · CFG, instruction, directive, and network helpers · `src/utils`

### Integrations

External interfaces and specialty workflows

- [Server](https://github.com/binsec/haunted/tree/master/src/server): service · Server layer for analysis I/O and callbacks · `src/server`
- [Proto](https://github.com/binsec/haunted/tree/master/src/proto): rpc schema · Protobuf definitions for configs, traces, and messages · `src/proto`
- [Examples](https://github.com/binsec/haunted/tree/master/src/examples): workflows · Example binaries and analysis scenarios · `src/examples`
- [Specialized](https://github.com/binsec/haunted/tree/master/src): extensions · Debug, IDA, LLVM, xtrasec, and SSE integration modules · `src`

## Connections

- binsec → Options: loads · Parses subsystem-specific CLI configuration
- binsec → Loader: invokes · Starts binary ingestion
- binsec → Disassembler: invokes · Runs disassembly and lifting
- binsec → Static AI: invokes · Selects static analysis path
- binsec → RelSE: invokes · Selects speculative relational analysis
- binsec → Dynamic DSE: invokes · Selects dynamic analysis path
- binsec → Server: serves · Can expose analyses through the server layer
- Options → Policies: configures · Policies shape analysis behavior
- Loader → Disassembler: feeds · Produces code and image data for decoding
- Disassembler → DBA: lifts · Lowers machine instructions into DBA
- Disassembler → Graphs: builds · Creates control-flow structures during disassembly
- DBA → Formula: converts · DBA terms and instructions become formulas
- Static AI → DBA: analyses · Consumes DBA for abstract interpretation and simulation
- Dynamic DSE → DBA: executes · Uses DBA-backed semantics for trace-driven analysis
- RelSE → DBA: models · Relational symbolic execution operates over DBA semantics
- RelSE → Formula: emits · Builds symbolic constraints and checks
- Formula → SMT-LIB: exports · Translates formulas to solver language
- SMT-LIB → Formula: imports · Reconstructs formulas from solver language
- Formula → RelSE: solves · SMT results drive security checks and path reasoning
- Dynamic DSE → Server: reports · Dynamic analyses can be exposed through service endpoints
- Proto → Server: describes · Schemas define exchanged analysis messages
- Examples → Dynamic DSE: demonstrates · Example binaries exercise dynamic workflows
- Specialized → Disassembler: extends · Peripheral decoders and integrations feed the pipeline
- Specialized → Formula: extends · Specialized symbolic-security workflows reuse formulas
- Graphs → Utils: uses · Graph utilities depend on shared helpers
- Kernel → Base: builds on · Kernel services sit on foundational primitives
- Loader → Base: uses · Binary parsing relies on common primitives
- Disassembler → Utils: uses · Disassembly reuses instruction and CFG helpers
- Static AI → Kernel: uses · Analysis orchestration depends on kernel abstractions
- Dynamic DSE → Kernel: uses · Dynamic execution reuses kernel services
- RelSE → Kernel: uses · Relational execution reuses kernel services