Skip to main content
Reverse engineering binaries has traditionally been a craft, one that takes a long time to develop. Analysts spend hours in disassemblers, recognizing patterns, making educated guesses about data structures, and gradually building models of how code behaves. Training these people takes a lot of time and effort. It works, but it doesn’t scale. Formal modeling offers a different approach: instead of relying solely on intuition, we can apply mathematical techniques to reason about binary behavior systematically. This doesn’t replace traditional reverse engineering, it augments it with tools that can answer specific questions automatically. This series is a broad overview for reverse engineers, security researchers, curious people, and CTF players who want to add formal methods to their toolkit, or for those who want to know what I’m rambling about on Twitter and want to know what the TLA/Alloy files are in all the software I ship. You should be comfortable with assembly, have basic Python experience, and ideally access to a disassembler like Ghidra. This is the first in a three-part series. I’ll cover the foundational concepts. Part 2 covers tools and practical workflows. Part 3 explores security research applications.

​
Three Approaches to Binary Analysis

Before diving into formal methods specifically, it helps to understand where they fit in the broader landscape. Binary analysts typically work with three complementary approaches, each with distinct tradeoffs. Static analysis examines code without executing it. Tools like Ghidra, IDA Pro, Binary Ninja, and radare2 disassemble binaries, recover control flow graphs, and identify patterns. Static analysis is fast and sees all code in the binary, but it can’t resolve values computed at runtime. Indirect jumps, dynamically unpacked code, and heavily obfuscated binaries can defeat it. Dynamic analysis runs the program and observes its behavior. Debuggers (GDB, x64dbg), tracers (strace, ltrace), fuzzers (AFL, libFuzzer), and instrumentation frameworks (DynamoRIO, Frida) fall into this category. Dynamic analysis sees actual runtime values and naturally handles obfuscation, code has to do what it does. The tradeoff: you only see paths that actually execute. Edge cases, error handlers, and paths requiring specific inputs may never run. Formal methods use mathematical reasoning to analyze program behavior. Rather than running concrete inputs or statically pattern-matching, formal techniques like symbolic execution reason about what could happen across classes of inputs. Symbolic execution frameworks like angr and Triton, backed by SMT solvers like Z3, can answer questions like “does any input reach this code?” or “what input satisfies these constraints?” The cost is computational: path explosion limits scalability, and modeling external environments (syscalls, libraries) adds complexity.
AspectStaticDynamicFormal
ExecutionNoneConcrete runsSymbolic/abstract
CoverageAll visible codeExecuted paths onlyExplored paths
ScalabilityExcellentGoodLimited by path explosion
False positivesHigherLowerVaries
False negativesLowerHigherVaries
Best forTriage, structureBehavior, valuesConstraint solving, proofs
In practice, experienced analysts combine all three: static analysis to identify interesting targets, dynamic analysis to understand runtime behavior, and formal methods to solve specific constraint problems or prove properties. The rest of this post focuses on the formal methods side of this triangle.

​
The Core Idea

Formal modeling for binary analysis treats programs as mathematical objects. Rather than running a program with specific inputs and observing what happens, we analyze what could happen across all possible inputs, or ask the computer to find inputs that produce specific behaviors. Three techniques form the foundation of this approach.

​
Symbolic Execution

Symbolic execution runs a program with symbolic values instead of concrete inputs. Instead of saying “the user entered ‘password123’”, we say “the user entered some string X”. As the program executes, we track how X flows through computations and what constraints accumulate. When the program branches on a condition involving X, we explore both paths. One path records that the condition must be true; the other records that it must be false. These accumulated constraints form the path condition a logical formula describing exactly what inputs reach each program point. The key insight: instead of testing one input at a time, symbolic execution reasons about entire classes of inputs simultaneously.

​
SMT Solving

Satisfiability Modulo Theories (SMT) solving takes those accumulated constraints and finds concrete values that satisfy them, or proves no such values exist. The “modulo theories” part is important. Unlike pure boolean satisfiability (SAT), SMT solvers understand the semantics of operations. A bit-vector theory knows that 0xFF + 1 = 0x00 for 8-bit values. An array theory understands indexing and updates. This domain knowledge makes SMT solvers far more powerful than raw SAT solvers for program analysis. Modern SMT solvers like Z3 can handle complex constraints over integers, bit-vectors, arrays, and strings. When symbolic execution discovers a path to interesting code, the SMT solver produces an actual input that reaches it.

​
Abstract Interpretation

Abstract interpretation approximates program behavior to make analysis tractable for larger programs. Instead of tracking exact values, we track properties: “this variable is positive”, “this pointer points to heap memory”, “this value came from user input”. The critical property of abstract interpretation (when used for verification) is soundness: it provides over-approximations that never miss real behaviors. If abstract interpretation says a variable might be negative, it could be negative in some execution. If it says a variable is always positive, that’s guaranteed. The tradeoff is precision. Sound over-approximating analyses may report that something is possible when it actually isn’t (false positives), but they won’t miss real behaviors (no false negatives). This property makes abstract interpretation suitable for proving absence of bugs, not just finding them.

​
A Concrete Example

Consider a program that checks if an input matches a transformed password: 
input = read_user_input()
x = input XOR 0x005A
y = rotate_left(x, 3)
if y == 0x1337:
    grant_access()
Manually, you’d work backward: what value of y equals 0x1337? What x produces that y after rotation? What input produces that x after XOR? With symbolic execution, you mark the input as symbolic and run the program. The engine tracks that:
  • x = input XOR 0x005A
  • y = rotate_left(x, 3)
  • The success path requires y == 0x1337
These constraints go to the SMT solver. Working backward:
  • y = 0x1337 means x = rotate_right(0x1337, 3) = 0xE266 (for 16-bit rotation)
  • x = input XOR 0x005A means input = 0xE266 XOR 0x005A = 0xE23C
The solver returns input = 0xE23C. No manual arithmetic needed—and unlike manual analysis, this scales to far more complex constraint systems.

​
What Can You Do With This?

These techniques unlock capabilities that would be tedious or impossible manually: Automatic Input Generation. Given a program that checks a serial number, symbolic execution can work backward from the “success” path to determine what inputs pass the check. What might take hours of manual analysis becomes a computation that finishes in seconds. Vulnerability Discovery. By adding constraints that represent security violations, buffer overflows, null pointer dereferences, use-after-free, symbolic execution can search for inputs that trigger them. If a triggering input exists along the explored paths, the solver will find it. Reasoning Through Obfuscation. Malware often uses tricks to confuse analysts: opaque predicates, code that appears to branch but always takes one path, encrypted strings decoded at runtime. Symbolic execution follows actual program semantics rather than syntactic appearances, cutting through some obfuscation automatically, but there are techniques that can be employed against this. Protocol Extraction. When analyzing network-facing code, formal methods can help extract the state machine of accepted inputs, mapping out valid message sequences without tedious manual tracing.

​
The Foundation for Practice

Understanding these techniques provides the conceptual foundation for applying formal methods to binary analysis. These techniques have a fundamental challenge: path explosion. Every branch in a program potentially doubles the number of paths to explore. A loop with N iterations and one symbolically-dependent branch per iteration can create 2^N paths. Real programs quickly become intractable for naive analysis. Part 2 addresses how practical tools manage this limitation. In Part 2, we’ll explore the practical side: the tools that implement these techniques, how to set up analysis workflows, and the real-world limitations you’ll encounter.