SYMSAN: Time and Space Efficient Concolic Execution via Dynamic Data-flow Analysis
SYMSAN: Time and Space Efficient Concolic Execution via Dynamic Data-flow Analysis
复制标题
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Ju Chen;Wookhyun Han;Mingjun Yin;Haochen Zeng;Chengyu Song;Byoungyoung Lee;Heng Yin;I. Shin
中科院分区：
文献类型：
--
作者：
Ju Chen;Wookhyun Han;Mingjun Yin;Haochen Zeng;Chengyu Song;Byoungyoung Lee;Heng Yin;I. Shin
Concolic Execution是一种功能强大的程序分析技术，用于系统地探索执行路径。与基于随机突变的模糊相比，并列执行特别适合于探索由复杂和紧凑的分支谓词保护的路径。然而，缺点是并发执行引擎比本机执行慢得多。虽然并列执行的最新进展显著降低了其性能开销，但我们的分析表明，最先进的并列执行器忽略了管理符号表达式的开销。基于可以将并发执行建模为一种特殊形式的动态数据流分析这一观察结果，我们建议利用现有的高度优化的数据流分析框架来实现并发执行器。为了验证这一思想，我们基于LLVM的数据流消毒器实现了一个原型S YM S An，并使用三组程序对其进行了评估：NBASE、DARPA网络大挑战数据集以及来自Google的Fuzzbench和Binutils的真实应用程序。结果表明，S、S、安对符号表情的处理开销要小得多。减少的开销还可以导致更快的并发执行和改进的代码覆盖率。
Concolic execution is a powerful program analysis technique for systematically exploring execution paths. Compared to random-mutation-based fuzzing, concolic execution is especially good at exploring paths that are guarded by complex and tight branch predicates. The drawback, however, is that concolic execution engines are much slower than native execution. While recent advances in concolic execution have significantly reduced its performance overhead, our analysis shows that state-of-the-art concolic executors overlook the overhead for managing symbolic expressions. Based on the observation that concolic execution can be modeled as a special form of dynamic data-flow analysis, we propose to leverage existing highly-optimized data-flow analysis frameworks to implement concolic executors. To validate this idea, we implemented a prototype S YM S AN based on the data-flow sanitizer of LLVM and evaluated it against the state-of-the-art concolic executors SymCC and SymQEMU with three sets of programs: nbench, the DARPA Cyber Grand Challenge dataset, and real-world applications from Google’s Fuzzbench and binutils. The results showed that S YM S AN has a much lower overhead for managing symbolic expressions. The reduced overhead can also lead to faster concolic execution and improved code coverage.