Write a Blog >>

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.

Thu 13 Oct

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 15:30
Technical Session 27 - Dynamic and Concolic AnalysisResearch Papers / NIER Track / Journal-first Papers at Banquet A
Chair(s): ThanhVu Nguyen George Mason University
13:30
20m
Research paper
LISSA: Lazy Initialization with Specialized Solver Aid
Research Papers
Juan Manuel Copia IMDEA Software Institute; Universidad Politécnica de Madrid, Pablo Ponzio Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Nazareno Aguirre University of Rio Cuarto and CONICET, Argentina, Alessandra Gorla IMDEA Software Institute, Marcelo F. Frias Dept. of Software Engineering Instituto Tecnológico de Buenos Aires
13:50
10m
Vision and Emerging Results
Outcome-Preserving Input Reduction for Scientific Data Analysis Workflows
NIER Track
Anh Duc Vu Humboldt-Universität zu Berlin, Timo Kehrer University of Bern, Christos Tsigkanos University of Bern, Switzerland
Pre-print
14:00
20m
Research paper
SymFusion: Hybrid Instrumentation for Concolic Execution
Research Papers
Emilio Coppa Sapienza University of Rome, Heng Yin UC Riverside, Camil Demetrescu Sapienza University Rome
Pre-print
14:20
20m
Research paper
Scalable Sampling of Highly-Configurable Systems: Generating Random Instances of the Linux Kernel
Research Papers
David Fernandez-Amoros UNED, Ruben Heradio UNED (Universidad Nacional de Educacion a Distancia), Christoph Mayr-Dorn JOHANNES KEPLER UNIVERSITY LINZ, Alexander Egyed Johannes Kepler University Linz
14:40
20m
Paper
A Practical Approach for Dynamic Taint Tracking with Control-Flow RelationshipsVirtual
Journal-first Papers
Katherine Hough , Jonathan Bell Northeastern University
Link to publication DOI Pre-print Media Attached
15:00
20m
Research paper
Prioritized Constraint-Aided Dynamic Partial-Order ReductionVirtual
Research Papers
Jie Su Xidian University, Cong Tian Xidian University, Zuchao Yang Xidian University, Jiyu Yang Xidian University, Bin Yu Xidian University, Zhenhua Duan Xidian University