Ponce4Ghidra

Interactive symbolic execution for Ghidra. Right-click, symbolize, solve — the plugin finds the password, the license key, the flag.

angr + Z3 Ghidra 11.4+ ELF / Mach-O / .so Veritesting + Unicorn
View on GitHub →

English  |  中文

5 Steps to Crack a Password

1. Open test_crackme in Ghidra
2. Right-click 0x1000004d7 (return 1) → Set as Find Target
3. Right-click 0x100000484 (return 0) → Set as Avoid
4. Ponce4Ghidra → Symbolize argv[1] (size: 4)
5. Solve Constraints → argv1 = P4Rg
Ponce4Ghidra Constraints tab showing solved constraints for test_crackme
Constraints tab: Z3's solution path — each constraint maps to a byte of the password P4Rg
Ponce4Ghidra Results tab showing 5 solutions for a 19-byte license key
Results tab: 5 valid license keys for test_license_elf — multi-solution enumeration on a 19-byte input

How It Works

Not brute force, not fuzzing — equation solving. A 16-byte input has 2128 possibilities. The constraints reduce it to a system Z3 solves in seconds.

YOU Set Find/Avoid Symbolize Ghidra Plugin Java 4-tab panel 8 menu actions Session save/restore JSON/TCP :13370 angr Engine Python Symbolic execution Path forking Constraint collection + Veritesting + Unicorn (optional) constraints Z3 Solver SAT + Theories CDCL engine bit-vector, array P4Rg
1
Symbolize — replace the input with a math variable
argv[1] becomes a 4-byte unknown: BVS("argv1", 32)
2
Fork — at each branch on the symbolic input, explore both sides
if (input[0] == 'P') → fork: one path adds constraint byte0 == 0x50, the other byte0 != 0x50
3
Collect — each path accumulates constraints as it runs
Found path: byte0==0x50 ∧ byte1==0x34 ∧ byte2^0x42==0x10 ∧ byte3+0x20==0x87
4
Solve — send all constraints to Z3
Z3's CDCL engine solves the system in milliseconds → P4Rg

Under the Hood: SAT/SMT Solving

Three layers of technology stack to turn a binary into an equation and solve it.

LAYER 1 — SYMBOLIC EXECUTION (angr) Runs the binary with math variables instead of concrete values. Forks at every branch. BVS("x",32) if(x[0]==0x50) branch → fork path_a: x[0]==0x50 path_b: x[0]!=0x50 Found path constraints: [x[0]==80, x[1]==52, ...] LAYER 2 — SMT SOLVER (Z3) Understands bit-vectors, arrays, and arithmetic. Translates to boolean logic for the SAT engine. Bit-Vector Theory XOR, AND, shift + × mod 2ⁿ Array Theory store(mem, addr, v) load(mem, addr)==v Arithmetic x + 0x20 == 0x87 linear + nonlinear Theory ↔ SAT Loop SAT proposes assignment Theory checks consistency LAYER 3 — SAT ENGINE (CDCL Algorithm) Pure boolean satisfiability. The core NP-complete problem, made practical by conflict-driven clause learning. 1. Decide guess a bit value 2. Propagate deduce forced values 3. Conflict? found contradiction 4. Learn clause + Backtrack permanently prune search space repeat until SAT or UNSAT

Concrete Example: Cracking test_crackme

The check_password function compares each byte of the input. Here's what angr + Z3 see:

C SOURCE int check_password(char *p) { if (p[0] != 'P') return 0; if (p[1] != '4') return 0; if ((p[2]^0x42)!=0x10) return 0; if ((p[3]+0x20)!=0x87) return 0; return 1; // ← Find target } angr explores CONSTRAINTS COLLECTED x[0] == 0x50 x[1] == 0x34 x[2] ^ 0x42 == 0x10 x[3] + 0x20 == 0x87 4 constraints, 4 unknowns 32 bits total to solve All from the "return 1" path Z3 solves SOLUTION x[0] = 0x50 = 'P' x[1] = 0x34 = '4' x[2] = 0x52 = 'R' x[3] = 0x67 = 'g' P 4 R g password cracked in 0.6 seconds

Why Not Brute Force?

Approach4-byte password16-byte license key32-byte AES key
Brute Force 2³² = 4.3 billion
~minutes		 2¹²⁸ = 3.4 × 10³⁸
heat death of universe		 2²⁵⁶
impossible
SAT/SMT 32 boolean vars
< 1ms		 128 boolean vars
< 1 second		 256 boolean vars
seconds (if constraints exist)

The trick: SAT/SMT doesn't try values — it derives them from constraints. Each learned clause permanently eliminates an exponential family of wrong guesses.

Triton Backend: Concolic Execution

Ponce4Ghidra ships two engines. angr explores all paths; Triton follows one concrete path while tracking symbolic state — no path explosion, ever.

angr — Symbolic Execution entry x[0]==0x50 ✓ x[0]!=0x50 ✗ x[1]==0x34 ✓ x[1]!=0x34 ✗ ... more forks ... Explores all paths simultaneously ⚠ Path explosion on large binaries Triton — Concolic Execution entry cmp [rdi],0x50 concrete: ZF=0 sym: x[0]==0x50 cmp [rdi+1],0x34 ... single path ... Follows one path, records constraints ✓ Never path-explodes

How Triton Works — Instruction-Level Semantics

Triton translates every CPU instruction into a math expression. No intermediate representation — it works directly on x86/ARM machine code.

CPU INSTRUCTION xor eax, 0x42 35 42 00 00 00 Triton Processing eax_new = eax_old ⊕ 0x42 ZF = (eax_new == 0) SF = eax_new[31] + CF, OF, PF, AF flags CONCRETE eax = 0x12 SYMBOLIC eax = input_0 ⊕ 0x42 Jonathan Salwan's core contribution: precise semantics for every instruction x86_64: ~1500 insns AArch64: ~500 insns ARM32: ~300 insns RISC-V: ~200 insns Each instruction modeled with all flag side-effects (EFLAGS: CF, ZF, SF, OF, PF, AF)

When to Use Which Engine

ScenarioangrTriton
Small function, find the password Best — explores all paths, guaranteed to find it Works — but needs a concrete input to start from
Large binary, DRM key derivation Path explosion Best — follows one trace, no explosion
Obfuscated code (VM/whitebox) Constraint explosion Best — doesn't need to "understand" the code
Have a Frida trace Can't replay a trace Best — replay trace with symbolic tracking
No concrete input available Best — starts from scratch Needs a starting input
Want all possible solutions Best — finds every satisfying path One path at a time (negate + re-run for alternatives)

Real Benchmark: angr vs Triton

Both engines solving the same binaries on the same machine, via symbolize_function_argument:

BinaryInput sizeangrTritonWinner
test_crackme
4 byte-compares, no libc		 4 bytes 0.18s ✓ 0.065s ✓ Triton 2.8×
test_license
19-byte key with strlen, XOR, checksum		 19 bytes 3.65s ✓ timeout ✗ angr

Why the difference?

Triton wins on pure computation — no path forking overhead, direct instruction-to-AST translation. For check_password (4 simple byte compares), it's 3× faster.

angr wins on functions that call libc (strlen, printf) — angr auto-hooks them with SimProcedures, while Triton tries to execute the real instructions (and the Mach-O libc stubs aren't loaded). For complex real-world functions, angr's SimOS layer is the deciding factor.

Rule of thumb: Use angr by default. Switch to Triton when angr path-explodes on a large function, or when you have a Frida trace to replay.

The DRM Reverse Engineering Workflow

Frida captures runtime data (keys, I/O samples) → Ponce4Ghidra analyzes the algorithm (angr for small funcs, Triton for large) → unidbg reproduces it as a standalone service.

Features

Σ

Multi-Solution Solver

Find up to 5 alternative solutions per variable. A password may have multiple valid inputs.

C

Constraint Visualization

See every constraint the solver collected. Understand why a path is reachable — not just that it is.

V

Veritesting

Smart path merging at loop boundaries. Large binaries don't path-explode.

U

Unicorn Engine

Concrete blocks execute via Unicorn (fast), symbolic only at branches touching symbolic data.

↻

Session Persistence

Save/Restore sessions across Ghidra restarts. Your Find/Avoid targets and symbolization commands survive.

⚡

Live Progress

Status bar updates every second during exploration: active paths, found count, step number, elapsed time.

When to Use Which Symbolize

MethodUse whenSpeed
Function Argument You know which function checks the input. Analyzing a .so library. Binary is large. Fast
argv[N] Program reads input from command line. Binary is small/simple. Need whole-program context. Medium
Register The unknown is a scalar (int/long), not a buffer. Fast
Memory The unknown is at a known fixed memory address (global variable, struct field). Fast

Rule of thumb: start with Function Argument. Use argv only when you need the entire program's execution context.

Platform Support

FormatArchitecturesStatus
Mach-Ox86_64Fully tested
ELFx86_64, ARM64, ARM32, MIPSTested (static binaries)
Android .soARM64, ARM32Supported (deferred state)

Installation

# 1. Python environment python3 -m venv .venv source .venv/bin/activate pip install angr pip install unicorn # optional: fast concrete execution # 2. Build the Ghidra extension export GHIDRA_INSTALL_DIR=/path/to/ghidra gradle buildExtension # 3. Install in Ghidra # File → Install Extensions → Add → dist/*.zip

Key Papers

Z3: An Efficient SMT Solverde Moura, Bjørner (2008, TACAS) — The solver behind Ponce4Ghidra
angr: (State of) The Art of WarShoshitaishvili et al. (2016, IEEE S&P) — The symbolic execution framework
GRASP: Conflict-Driven Clause LearningMarques-Silva, Sakallah (1996, ICCAD) — The algorithm that makes SAT solving practical
KLEE: Automatic Test GenerationCadar, Dunbar, Engler (2008, OSDI) — Source-level symbolic execution milestone