Sebastian Poeplau (EURECOM and Code Intelligence), Aurélien Francillon (EURECOM)

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

(Short) Object Removal Attacks on LiDAR-based 3D Object Detectors

Zhongyuan Hau, Kenneth Co, Soteris Demetriou, and Emil Lupu (Imperial College London) Best Short Paper Award Runner-up!

Read More

What Remains Uncaught?: Characterizing Sparsely Detected Malicious URLs on...

Sayak Saha Roy, Unique Karanjit, Shirin Nilizadeh (The University of Texas at Arlington)

Read More

SerialDetector: Principled and Practical Exploration of Object Injection Vulnerabilities...

Mikhail Shcherbakov (KTH Royal Institute of Technology), Musard Balliu (KTH Royal Institute of Technology)

Read More

Is Your Firmware Real or Re-Hosted? A case study...

Abraham A. Clements, Logan Carpenter, William A. Moeglein (Sandia National Laboratories), Christopher Wright (Purdue University)

Read More