Symbolic execution is a powerful program analysis technique which explores new paths through a program by generating inputs that are guaranteed to exercise those paths. However, there is a lack of modern research on symbolic execution for programs that manipulate strings, especially for C programs. In this work, we develop an approach for symbolically executing string-manipulating C programs and implement it in a proof-of-concept tool called SymCC-str. SymCC-str is built on top of the concolic execution engine SymCC and the smt-switch SMT solving API, enabling it to make use of modern advancements in both symbolic execution and string solving. SymCC-str’s novelty lies in its hybrid data representation, expressing symbolic data both as SMT bitvectors and strings in order to balance the performance and expressivity of these respective theories. Through this novel approach, SymCC-str achieves a median 9.9% increase in branch coverage (up to 990% in the best case) compared to SymCC on 6 real-world benchmark programs.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Integrating String Reasoning in Symbolic Execution of C Programs

  • Rachel Cleaveland,
  • Clark Barrett

摘要

Symbolic execution is a powerful program analysis technique which explores new paths through a program by generating inputs that are guaranteed to exercise those paths. However, there is a lack of modern research on symbolic execution for programs that manipulate strings, especially for C programs. In this work, we develop an approach for symbolically executing string-manipulating C programs and implement it in a proof-of-concept tool called SymCC-str. SymCC-str is built on top of the concolic execution engine SymCC and the smt-switch SMT solving API, enabling it to make use of modern advancements in both symbolic execution and string solving. SymCC-str’s novelty lies in its hybrid data representation, expressing symbolic data both as SMT bitvectors and strings in order to balance the performance and expressivity of these respective theories. Through this novel approach, SymCC-str achieves a median 9.9% increase in branch coverage (up to 990% in the best case) compared to SymCC on 6 real-world benchmark programs.