Solving Malware With Symbolic Execution

---
name: solving-malware-with-symbolic-execution
description: 'Uses symbolic execution (angr) to solve constraint-based malware problems — finding
  inputs that reach a target branch, recovering keys/passwords from a check routine, and
  brute-forcing opaque predicates — by generating a ready-to-edit angr harness. Activates for
  requests to use symbolic execution, solve a malware unlock check with angr, or recover an input
  that reaches a code path.'
domain: cybersecurity
subdomain: reverse-engineering
tags:
  - reverse-engineering
  - symbolic-execution
  - angr
  - deobfuscation
  - automation
version: 1.0.0
author: analyst-ai-pack
license: Apache-2.0
mitre_attack:
  - T1027
  - T1480
  - T1140
d3fend:
  - D3-DA
  - D3-SDA
references:
  - 'angr documentation — https://docs.angr.io/'
  - 'MITRE ATT&CK T1480 Execution Guardrails — https://attack.mitre.org/techniques/T1480/'
---

# 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

```bash
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`](references/api-reference.md) for the harness generator.
- angr docs and ATT&CK T1480 (linked in frontmatter).