符號執行之動態路徑修剪技術

Dynamic Path Pruning in Symbolic Execution

陳盈伸(Ying-Shen Chen)

指導教授 ： 蕭旭君

國立臺灣大學/電機資訊學院/資訊工程學研究所/碩士(2016年)

https://doi.org/10.6342/NTU201602958

摘要

路徑修剪技術是藉由盡早修剪掉不可滿足的路徑（unsatisfiable paths），來減輕符號執行（symbolic execution）遇到路徑爆炸的問題，雖然現有的符號執行已經有一些策略來修剪不可滿足的路徑，但這些策略的效率仍需要進行探討，其因在於我們需要花費額外的時間來檢查並且修剪路徑。
這篇論文先定義了路徑修剪問題（path pruning problem），並且展示了現有的路徑修剪策略在面對不同的執行檔，都有可能會有最糟的探索時間發生。為此，我們提出了動態路徑修剪技術（dynamic path pruning），這個技術可以在不同的執行擋上，都會有接近最佳的探索時間。動態路徑修剪技術的一個直覺的概念是：我們使用較高的檢查比例（checking rate）在較高機率是不滿足的路徑上。動態路徑修剪技術根據探索時的一些特性來進行最佳化並且找到一個最佳的檢查比例，其中探索時的特性像是我們所觀察到的可滿足的路徑比例。動態路徑修剪技術實作在一個開源的符號執行平台上且僅需額外的一百多行程式碼。我們在實驗結果將會呈現使用動態路徑修剪技術來分析 GNU 核心工具組（coreutils）會總是有接近最佳的探索時間。而我們未來方向也將朝向調整檢查範圍（checking range）以及動態超時調整來進行優化。

關鍵字

符號執行 ； 路徑修剪 ； 動態分析

並列摘要

Path pruning can alleviate path explosion in symbolic execution by removing unsatisfiable paths at their early stages before they grow into many. Although existing symbolic execution tools have implemented several strategies to remove unsatisfiable paths, it remains unclear how effective these strategies are because checking a path's satisfiability also takes non-negligible time.
This work formulates the path pruning problem and demonstrates that existing path pruning strategies suffer from unacceptable worst-case performance due to their program-independent behaviors. To this end, we propose dynamic path pruning (DPP), a path pruning strategy that consistently achieves near-optimal exploration time for a wide spectrum of programs. The intuition behind DPP is assigning a higher checking rate to paths that are more likely to be unsatisfiable. DPP finds the optimal checking rate by solving an optimization problem and adjusts to the optimal checking rate based on the observed program's characteristic, including the observed percentage of satisfiable paths. DPP is implemented on top of an open-source symbolic execution platform in only hundred of lines. Our evaluation shows that using DPP for analyzing the coreutils will always yield near-optimal exploration time. We can also adjust the checking range and timeout in DPP to get more optimized in future work.

並列關鍵字

symbolic execution ； path pruning ； dynamic analysis

參考文獻

[2] Angry hacking. DEFCON 2015.

[6] KLEE LLVM execution engine. http://klee.github.io/.

[11] D. Chen, Y. Zhang, L. Cheng, Y. Deng, and X. Sun. Heuristic path pruning algorithm based on error handling pattern recognition in detecting vulnerability. In Computer Software and Applications Conference Workshops (COMPSACW), 2013 IEEE 37th

Annual, pages 95–100. IEEE, 2013.

[13] P. Godefroid, M. Y. Levin, and D. Molnar. Sage: whitebox fuzzing for security testing. Queue, 10(1):20, 2012.