Solving Malware With Symbolic Execution

When to Use

• You need to find an input that reaches (or avoids) a specific address — a license/unlock check, an environment guardrail, or an opaque predicate — without manual constraint solving.
• You want to recover a key/password a check routine validates, or prune bogus branches.

Do not use angr's unicorn/concrete execution against untrusted code outside isolation — and do not treat symbolic execution as a substitute for understanding the routine. This skill generates a harness; run it in an isolated environment.

Prerequisites

• The target binary and the relevant addresses (entry, target/avoid). The angr package (the script degrades gracefully and reports availability if absent).

Safety & Handling

• Run generated harnesses in an isolated VM; angr loads the binary — keep inputs contained.

Workflow

Step 1: Check availability and generate a harness

python scripts/analyst.py check
python scripts/analyst.py harness --binary sample.bin --find 0x401234 --avoid 0x401260 \
    --out solve.py

Emits an angr script that loads the binary, sets a symbolic stdin/argument, explores to --find while avoiding --avoid, and prints the solving input.

Step 2: Constrain the input

Edit the harness to add the input's length/charset constraints (printable, specific size) so the solver converges quickly.

Step 3: Run and interpret

Run the harness; the recovered concrete input is the key/password/flag that reaches the target.

Step 4: Validate manually

Confirm the recovered input actually drives the intended path in a debugger/disassembler.

Validation

• The harness sets explicit find/avoid addresses and a constrained symbolic input.
• A found solution is verified to reach the target in a debugger.
• State explosion is mitigated with constraints or veritesting.

Pitfalls

• State explosion on loops/large inputs — constrain length and use LAZY_SOLVES/veritesting.
• Symbolic-execution-hostile code (hashing, heavy crypto) that angr cannot tractably solve.
• Wrong addresses (ASLR/base) — use the binary's load base, not a runtime address.

References

• See references/api-reference.md for the harness generator.
• angr docs and ATT&CK T1480 (linked in frontmatter).