SECURITY REVIEW
Not yet assessed
Review the original instructions and requested permissions before installing.
No security review is available for this catalog entry yet.
Community / AGENT SKILL
solving-malware-with-symbolic-execution
0
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.
Understand the trade-offs.
SKILL QUALITY
Not yet assessed
How clearly the skill guides your agent, how complete its workflow is, and how you can check the outcome.
No quality assessment is available for this catalog entry yet.
The full skill.
Original instructions from the publisher’s SKILL.md
# 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).