Sebastian Poeplau and Aurélien Francillon, EURECOM
Distinguished Paper Award Winner
A major impediment to practical symbolic execution is speed, especially when
compared to near-native speed solutions like fuzz testing. We propose a
compilation-based approach to symbolic execution that performs better than
state-of-the-art implementations by orders of magnitude. We present SymCC, an
LLVM-based C and C++ compiler that builds concolic execution right into the
binary. It can be used by software developers as a drop-in replacement for
clang
and clang++
, and we show how to add support for other languages with
little effort. In comparison with KLEE, SymCC is faster by up to three orders of
magnitude and an average factor of 12. It also outperforms Qsym, a system that
recently showed great performance improvements over other implementations, by up
to two orders of magnitude and an average factor of 10. Using it on real-world
software, we found that our approach consistently achieves higher coverage, and
we discovered two vulnerabilities in the heavily tested OpenJPEG project, which
have been confirmed by the project maintainers and assigned CVE identifiers.
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.
author = {Sebastian Poeplau and Aur{\'e}lien Francillon},
title = {Symbolic execution with {SymCC}: Don{\textquoteright}t interpret, compile!},
booktitle = {29th USENIX Security Symposium (USENIX Security 20)},
year = {2020},
isbn = {978-1-939133-17-5},
pages = {181--198},
url = {https://www.usenix.org/conference/usenixsecurity20/presentation/poeplau},
publisher = {USENIX Association},
month = aug
}