標題: Dynamic Path Pruning in Symbolic Execution
作者: Chen, Ying-Shen
Chen, Wei-Ning
Wu, Che-Yu
Hsiao, Hsu-Chun
Huang, Shih-Kun
資訊工程學系
Department of Computer Science
公開日期: 1-Jan-2018
摘要: To alleviate path explosion in symbolic execution, path pruning removes unsatisfiable paths at an early stage before they multiply. Although existing symbolic execution platforms have implemented several path pruning strategies to determine whether and when to check a path's satisfiability, it remains unclear how effective these strategies are because the time to check a path's satisfiability is non-negligible and may vary drastically. This work proposes dynamic path pruning (DPP), a strategy that aims to minimize the overall exploration time by dynamically adjusting the path checking rate. DPP assigns a higher checking rate to paths that are more likely to be unsatisfiable, and the likelihood is estimated based on the observed program's characteristics, such as the observed percentage of satisfiable paths. DPP is implemented on top of an open source symbolic execution platform in only a few hundred lines. Our evaluation confirms that DPP consistently achieves near-optimal exploration time for a wide spectrum of programs, whereas existing static path pruning strategies suffer from unacceptable worstcase performance due to their program-independent behaviors. Compared with static strategies, DPP performs best in 84% (110 out of 131) of CGC binaries, and the exploration time is within 100-124% of the best static strategy in 95% of the tested handcrafted and coreutils binaries.
URI: http://hdl.handle.net/11536/151736
ISBN: 978-1-5386-5790-4
期刊: 2018 IEEE CONFERENCE ON DEPENDABLE AND SECURE COMPUTING (DSC)
起始頁: 123
結束頁: 130
Appears in Collections:Conferences Paper