Symbolic execution for triage

TL;DR: angr (or Triton, KLEE-Native) is best used to answer narrow questions about a crash — “is this constraint solvable?”, “what input reaches block B?” — not as a black-box bug-finder for full Windows binaries.

What it is

Symbolic execution treats inputs as symbolic variables, walks code paths, and accumulates path constraints; an SMT solver decides feasibility and synthesises concrete inputs. For Windows exploit triage it pairs naturally with IDA/Ghidra: extract the basic-block CFG, mark interesting locations, and ask the engine to produce inputs that reach them — turning a fuzzer crash into a deterministic test case or proving a code path unreachable.

Preconditions / where it applies

A specific question that fits symbolic execution: reachability, satisfiability of a single constraint, value enumeration over a small state.
The target slice is small (single function or a few thousand instructions). Whole-binary symbolic execution on Windows binaries explodes because of Windows API surface and threading.
Either source-level harness (KLEE/Symbolic LLVM) or angr with binary hooks for kernel/Win32 calls.

Technique

1. Define the scope tightly. Pick the function around the crashing instruction. Anything you don’t need to model (registry, file I/O, GDI) should be hooked to return a constant.

2. angr quickstart for a Windows binary.

  
import angr, claripy
proj = angr.Project('vuln.exe', auto_load_libs=False)
state = proj.factory.blank_state(addr=0x401234)
sym_buf = claripy.BVS('buf', 8 * 0x100)
state.memory.store(0x402000, sym_buf)
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=0x4014f0, avoid=0x401590)
print(simgr.found[0].solver.eval(sym_buf, cast_to=bytes))

3. Hook noisy APIs.

  
proj.hook_symbol('GetTickCount', angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained']())

4. Model a syscall edge. For kernel triage, hook NtDeviceIoControlFile to mark input/output buffers symbolic and constrain length.

5. Cap exploration. Use LengthLimiter techniques, loop-handling, and veritesting to keep paths manageable.

6. Common useful queries.

Reach the crash from a clean state. Find concrete input that drives execution to the faulting instruction.
Generalise the crash. What range of inputs (e.g. length values) preserves the constraint that triggers the bug?
Detect dead checks. Show that a length check after a double-fetch is or isn’t constrained by attacker bytes.

Where it fails. Tight loops, heavy floating point, complex string library calls, or anything threaded usually wins against the solver. Combine with concolic seeding (driftuzz, eclipser): use fuzzer-found inputs as a starting concrete trace and only symbolicate the bytes you need.

Detection and defence

This is a researcher-side technique; no runtime detection applies.
The hardened compilation features (CFG, sanitisers) make exploits derived from triage harder to land, not the triage itself.

References

angr docs — engine reference
Triton DSE — Intel-style binary symbolic execution
Project Zero — symbolic triage notes — case write-ups