SymFusion: Hybrid Instrumentation for Concolic Execution

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. With the former strategy, the resulting code is more efficient but requires recompilation. With the latter strategy, the instrumentation code is typically less efficient but does not require recompilation. Unfortunately, recompiling the entire code of a program is not always easy or practical for a user, e.g., in presence of third-party components, such as system libraries. At the same time, efficiency may be crucial for the tool’s effectiveness. In this paper, we investigate a different design for a concolic executor, called SymFusion, which is based on hybrid instrumentation. In particular, our approach allows the user to recompile the core components of an application, thus minimizing the analysis overhead on them, while still being able to dynamically instrument the rest of the application components at execution time. Our experimental evaluation shows that our design can achieve a nice balance between efficiency and efficacy on several real-world applications.