SYMSAN: Time and Space Efficient Concolic Execution via Dynamic Data-flow Analysis

Authors: 

Ju Chen, UC Riverside; Wookhyun Han, KAIST; Mingjun Yin, Haochen Zeng, and Chengyu Song, UC Riverside; Byoungyoung Lee, Seoul National University; Heng Yin, UC Riverside; Insik Shin, KAIST

Abstract: 

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 SYMSAN 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 SYMSAN has a much lower overhead for managing symbolic expressions. The reduced overhead can also lead to faster concolic execution and improved code coverage.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {281360,
author = {Ju Chen and WookHyun Han and Mingjun Yin and Haochen Zeng and Chengyu Song and Byoungyoung Lee and Heng Yin and Insik Shin},
title = {{SYMSAN}: Time and Space Efficient Concolic Execution via Dynamic Data-flow Analysis},
booktitle = {31st USENIX Security Symposium (USENIX Security 22)},
year = {2022},
isbn = {978-1-939133-31-1},
address = {Boston, MA},
pages = {2531--2548},
url = {https://www.usenix.org/conference/usenixsecurity22/presentation/chen-ju},
publisher = {USENIX Association},
month = aug,
}

Presentation Video