A symbolic execution framework for Binary Ninja's Low-Level IL (LLIL).

• Concrete & symbolic emulation of 65+ LLIL operations
• BitVector arithmetic backed by Boost.Multiprecision (int512_t)
• Symbolic expressions with automatic simplification (7-pass fixpoint)
• Z3 solver integration (batch and incremental Push/Pop/Assert)
• Memory model with byte-level granularity, symbolic load/store handlers, and a memory provider callback for backing binary data
• Sub-register windowing (e.g., reading eax from rax)
• Explorer — BFS/DFS multi-path execution with interprocedural support, call hooks, function resolver, and configurable limits
• Taint tracking per register and memory byte
• Context cloning for forking execution state

bn-emu requires a Visual Studio Developer Shell (or equivalent compiler environment) and an installed copy of Binary Ninja.

# Configure (Z3_DIR must point to your Z3 install; Boost is fetched automatically)
cmake --preset relwithdebinfo -DZ3_DIR="D:/libs/z3/lib/cmake/z3"

# Build
cmake --build build/relwithdebinfo

# Install test & example plugins into Binary Ninja
cmake --build build/relwithdebinfo --target install

After building, install bn-emu to a prefix:

cmake --install build/relwithdebinfo --prefix D:/libs/bn-emu

Then in your consumer project:

# Your CMakeLists.txt
find_package(bnemu REQUIRED CONFIG)
target_link_libraries(my_plugin PRIVATE bnemu::bnemu)

Configure with the install prefix on CMAKE_PREFIX_PATH:

cmake -B build -DCMAKE_PREFIX_PATH="D:/libs/bn-emu;D:/libs/z3-release"

The consumer must also provide:

• Binary Ninja API — via FetchContent (same pattern as bn-emu)
• Boost multiprecision/math — via FetchContent or system install
• Z3 — findable via find_package(Z3 CONFIG)

Tests are compiled as a Binary Ninja plugin (bnemu-tests.dll). After cmake --build build/relwithdebinfo --target install, open Binary Ninja and run the test commands from the command palette or plugin menu.

emulator/
  emulator.h/cc    LLIL emulator (Step/Run, 65+ ops)
  context.h/cc     Execution state: registers, memory, constraints, flags
  bitvector.h/cc   Arbitrary-width bitvector arithmetic
  symbolic.h/cc    Symbolic variables and expressions
  value.h          Abstract Value base class
  solver.h         Abstract solver interface
  solver_z3.h/cc   Z3 backend
  simplifier.h/cc  Expression simplifier (7 passes + custom)
  explorer.h/cc    Multi-path BFS/DFS explorer
test/              Unit tests (Google Test, runs inside BN)
examples/          Example BN plugins (password solver, OOB detector)
cmake/             CMake package config template

This project is licensed under the MIT License.