SymFusion: Hybrid Instrumentation for Concolic Execution

Emilio Coppa, Heng Yin, Camil Demetrescu

Abstract

Concolic execution is a dynamic twist of symbolic execution designed with scalability in mind. Recent concolic executors heavily rely on program instrumentation to achieve such scalability. The instrumentation code can be added at compilation time (e.g., using an LLVM pass), or directly at execution time with the help of a dynamic binary translator. The former approach results in more efficient code but requires recompilation. Unfortunately, recompiling the entire code of a program is not always feasible or practical (e.g., in presence of third-party components). On the contrary, the latter approach does not require recompilation but incurs significantly higher execution time overhead.

BibTeX

@inproceedings{Coppa-al:ASE22,
  author    = {Emilio Coppa and
               Heng Yin and
               Camil Demetrescu},
  title     = {{SymFusion:} Hybrid Instrumentation for Concolic Execution},
  booktitle = {ASE},
  pages     = {100:1--100:12},
  publisher = {{ACM}},
  year      = {2022},
}

SymFusion: Hybrid Instrumentation for Concolic Execution

Abstract

Related papers