Symbolic execution is a powerful technique for software analysis and bug detection. Compilation-based symbolic execution is a recently proposed flavor that has been shown to improve the performance of symbolic execution significantly when source code is available. We demonstrate a novel technique to enable compilation-based symbolic execution of binaries (i.e., without the need for source code). Our system, SymQEMU, builds on top of QEMU, modifying the intermediate representation of the target program before translating it to the host architecture. This enables SymQEMU to compile symbolic-execution capabilities into binaries and reap the associated performance benefits while maintaining architecture independence.

We present our approach and implementation, and we show that it outperforms the state-of-the-art binary symbolic executors S2E and QSYM with statistical significance; on some benchmarks, it even achieves better performance than the source-based SymCC. Moreover, our tool has found a previously unknown vulnerability in the well-tested libarchive library, demonstrating its utility in testing real-world software.

View More Papers

Refining Indirect Call Targets at the Binary Level

Sun Hyoung Kim (Penn State), Cong Sun (Xidian University), Dongrui Zeng (Penn State), Gang Tan (Penn State)

Read More

CROW: Code Diversification for WebAssembly

Javier Cabrera Arteaga, Orestis Floros, Benoit Baudry, Martin Monperrus (KTH Royal Institute of Technology), Oscar Vera Perez (Univ Rennes, Inria,...

Read More

Flexsealing BGP Against Route Leaks: Peerlock Active Measurement and...

Tyler McDaniel (University of Tennessee, Knoxville), Jared M. Smith (University of Tennessee, Knoxville), Max Schuchard (University of Tennessee, Knoxville)

Read More