TY - GEN
T1 - Dynamic Path Pruning in Symbolic Execution
AU - Chen, Ying Shen
AU - Chen, Wei Ning
AU - Wu, Che Yu
AU - Hsiao, Hsu Chun
AU - Huang, Shih-Kun
N1 - Publisher Copyright:
© 2018 IEEE.
PY - 2019/1/23
Y1 - 2019/1/23
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85062567403&partnerID=8YFLogxK
U2 - 10.1109/DESEC.2018.8625128
DO - 10.1109/DESEC.2018.8625128
M3 - Conference contribution
AN - SCOPUS:85062567403
T3 - DSC 2018 - 2018 IEEE Conference on Dependable and Secure Computing
BT - DSC 2018 - 2018 IEEE Conference on Dependable and Secure Computing
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2018 IEEE Conference on Dependable and Secure Computing, DSC 2018
Y2 - 10 December 2018 through 13 December 2018
ER -