符號執行

• 符號執行 (Symbolic Execution)

• Concolic Execution 具體-符號 執行，也稱為 Dynamic Symbolic Execution (DSE)

• Execution Generated Test (EGT)

工具

• S2E

SMT solver

Satisfiability Modulo Theories solver

• z3
• Angr Solver Engine

AEG

stack-based buffer overflow

可以透過 angr 找到 unconstrained state，之後去檢查 program counter 是否為 symbolic

如果為 symbolic 我們就對該 state 設置 pc 的條件約束，之後進行約束求解得出 PoC input

範例

• practice/pwn/AEG

參見

• MIT OpenCourseWare Symbolic Execution
• 简单理解符号执行技术 K0rz3n’s Blog
• 符号执行入门
• Fuzzing

---

Symbolic Execution AEG SMT