reverse-skills-max/vendor-new/analyst-ai-pack/skills/solving-malware-with-symbolic-execution/SKILL.md

name, description, domain, subdomain, tags, version, author, license, mitre_attack, d3fend, references

name	description	domain	subdomain	tags	version	author	license	mitre_attack	d3fend	references
solving-malware-with-symbolic-execution	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.	cybersecurity	reverse-engineering	reverse-engineering symbolic-execution angr deobfuscation automation	1.0.0	analyst-ai-pack	Apache-2.0	T1027 T1480 T1140	D3-DA D3-SDA	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

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).