# Symbolic Execution 符號執行 ss8651twtw https://hackmd.io/@ss8651twtw/symbolic --- ## 符號執行是啥？ 一種分析程式的方法，用來找出哪些輸入會使程式執行到特定位置 ---- ### 名詞們 - 符號 Symbol - 限制條件 Constrain - 執行路徑 Path ---- ### 執行流程  ---- ### 執行流程 1. 制訂輸入的 Symbol 2. 模擬執行程式並使用 Symbol 表示各個表達式與跳轉的條件判斷式 3. 收集 Constrain 並求解得出 Symbol 實際的值 ---- ### 執行流程 ```c= int f() { ... y = read(); // symbol λ z = y * 2; // 2λ if (z == 12) { // constrain 2λ == 12 fail(); // ... continue execution } else { // constrain 2λ != 12 printf("OK"); // ... continue execution } } ``` ---- ### 和一般執行程式的差別 一般執行 (concrete execution) 依據輸入狀態有確定的執行路徑 ```c= int f() { ... y = read(); // 111 z = y * 2; // 222 if (z == 12) { // not satisfied fail(); } else { // jump here printf("OK"); // ... continue execution } } ``` ---- ### 相關工具 - [angr](https://angr.io/) - multi-architecture binary analysis toolkit platform - [KLEE](https://klee.github.io/) - symbolic execution engine - [Triton](https://triton.quarkslab.com/) - dynamic binary analysis (DBA) framework ---- ### 限制 - Path explosion - Program-dependent efficiency - Memory aliasing - Arrays - Environment interactions --- ## angr 使用說明 <img src="https://angr.io/img/angry_face.png" style="border:0; background:rgba(255, 255, 255, 0)"> ---- ### 安裝 強烈建議使用任一 Python 虛擬環境安裝 ```shell # make sure you use python3 pip install angr ``` ---- ### 範例程式 ```python import angr import claripy # solver engine ``` ---- ### 範例程式 ```python # Loading the binary # auto_load_libs False for improved performance proj = angr.Project("/path/to/binary", auto_load_libs = False) ``` ---- ### 範例程式 ```python # Create a SimState object state = proj.factory.entry_state() ``` ---- ### 範例程式 ```python # Generate a simulation manager object simgr = proj.factory.simulation_manager(state) ``` ---- ### 範例程式 ```python # Symbolically execute until we find a state satisfying our find= and avoid= parameters avoid_addr = [0x400c06, 0x400bc7] find_addr = 0x400c10d simgr.explore(find=find_addr, avoid=avoid_addr) ``` ---- ### 範例程式 ```python # Create symbolic object sym_arg_size = 15 sym_arg = claripy.BVS('sym_arg', 8 * sym_arg_size) ``` ---- ### 範例程式 ```python # Restrict sym_arg to typical char range for byte in sym_arg.chop(8): initial_state.add_constraints(byte >= '\x20') # ' ' initial_state.add_constraints(byte <= '\x7e') # '~' ``` --- ## Reference - https://en.wikipedia.org/wiki/Symbolic_execution - https://angr.io/ - https://github.com/angr/angr-doc/blob/master/CHEATSHEET.md - https://github.com/angr/angr-doc/tree/master/examples - https://klee.github.io/ - https://triton.quarkslab.com/ --- ## Thanks for Listening