43 lines
1.5 KiB
Markdown
43 lines
1.5 KiB
Markdown
# API Reference: Solving Malware With Symbolic Execution
|
|
|
|
## Overview
|
|
|
|
`scripts/analyst.py` generates an angr harness that loads a binary, explores to a target address
|
|
while avoiding another, constrains a symbolic input, and prints the solving input. `check` reports
|
|
angr availability. The tool only generates text — it does not load the binary or run the sample.
|
|
|
|
## Dependencies
|
|
|
|
| Package | Version | Purpose |
|
|
|---------|---------|---------|
|
|
| angr | latest | runs the generated harness (optional for generation) |
|
|
| (stdlib) | — | JSON, file IO |
|
|
|
|
## Core functions
|
|
|
|
### `check()`
|
|
Reports whether `angr` is importable.
|
|
|
|
### `harness(binary, find, avoid, out)`
|
|
Writes an angr script using `full_init_state`, a `claripy` symbolic stdin (printable-constrained),
|
|
`Veritesting`, and `simgr.explore(find=…, avoid=…)`.
|
|
|
|
## Tuning for convergence
|
|
|
|
- Constrain input length and charset (the skeleton sets printable bytes).
|
|
- Use `Veritesting` (enabled) and consider `LAZY_SOLVES` for branchy code.
|
|
- Provide accurate load-base addresses for `find`/`avoid`.
|
|
|
|
## Usage
|
|
|
|
```bash
|
|
python scripts/analyst.py check
|
|
python scripts/analyst.py harness --binary sample.bin --find 0x401234 --avoid 0x401260 --out solve.py
|
|
```
|
|
|
|
## Sources
|
|
|
|
- angr documentation (simulation managers, exploration techniques) — https://docs.angr.io/
|
|
- MITRE ATT&CK T1480 Execution Guardrails — https://attack.mitre.org/techniques/T1480/
|
|
- claripy symbolic-variable and constraint API from the angr docs
|