pathfinder-symexec

CSE 260 honors project repo.

This is basically a small survey plus a few controlled experiments with KLEE and angr. The main write-up is in docs/report.md. The rest of the repo is just the small harnesses, runner scripts, and notes behind that report.

repo layout

• target/ - small C programs used in the experiments
• scripts/ - helper scripts for KLEE and angr
• analysis/ - experiment notes and comparisons
• docs/report.md - final report
• docs/report.pdf - exported report

running it

KLEE with Docker

This is the easiest path on Windows.

1. Start Docker Desktop.
2. Run powershell -ExecutionPolicy Bypass -File scripts\run_klee_docker.ps1
3. To change the search strategy, add -Search dfs, -Search bfs, or -Search random-path
4. To run the larger heuristic harness, add -Program heuristic_demo -MaxInstructions 400

Outputs go in outputs/klee_*.

KLEE in Linux or a dev container

1. Open the project in a Linux environment with KLEE installed.
2. Run make bitcode
3. Run klee --output-dir=outputs/klee_run bitcode/example.bc

angr in WSL

1. Install dependencies: sudo apt install -y python3-venv python3-pip build-essential
2. Create a virtual environment: python3 -m venv .venv
3. Activate it: source .venv/bin/activate
4. Install angr: pip install angr
5. Build the Linux binary: gcc -o binaries/example_plain target/example_plain.c
6. Run the example: python scripts/angr_example.py
7. Run the security demo: gcc -no-pie -o binaries/auth_demo target/auth_demo.c then python scripts/angr_security_demo.py

angr is meant to run on native Linux binaries in WSL. I am not relying on Windows PE analysis here.

useful files

• analysis/path_constraints.md - path-condition walkthrough for the simple harness
• analysis/heuristic_comparison.md - bounded DFS/BFS comparison
• analysis/practical_strategies.md - short survey of practical scaling strategies
• docs/report.md - final project report with bibliography