Dynamic Path Pruning in Symbolic Execution

Ying Shen Chen, Wei Ning Chen, Che Yu Wu, Hsu Chun Hsiao, Shih-Kun Huang

研究成果: Conference contribution同行評審

摘要

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 worst-case 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.

原文English
主出版物標題DSC 2018 - 2018 IEEE Conference on Dependable and Secure Computing
發行者Institute of Electrical and Electronics Engineers Inc.
ISBN(電子)9781538657904
DOIs
出版狀態Published - 23 一月 2019
事件2018 IEEE Conference on Dependable and Secure Computing, DSC 2018 - Kaohsiung, Taiwan
持續時間: 10 十二月 201813 十二月 2018

出版系列

名字DSC 2018 - 2018 IEEE Conference on Dependable and Secure Computing

Conference

Conference2018 IEEE Conference on Dependable and Secure Computing, DSC 2018
國家Taiwan
城市Kaohsiung
期間10/12/1813/12/18

指紋 深入研究「Dynamic Path Pruning in Symbolic Execution」主題。共同形成了獨特的指紋。

引用此