94 lines
3.3 KiB
Markdown
94 lines
3.3 KiB
Markdown
---
|
|
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).
|