Programs that deal with heap-allocated inputs are difficult to analyze with symbolic execution (SE). Lazy Initialization (LI) is an approach to SE that deals with heap-allocated inputs by starting SE over a fully symbolic heap, and initializing the inputs’ fields on demand, as the program under analysis accesses them. However, when the program’s assumed precondition has structural constraints over the inputs, operationally captured via repOK routines, LI may produce spurious symbolic structures, making SE traverse infeasible paths and undermining SE’s performance. repOK can only decide the feasibility of fully concrete structures, and thus previous work relied on manually crafted specifications designed to decide the (in)validity of partially symbolic inputs, to avoid producing spurious symbolic structures. However, these additional specifications require significant further effort from developers.
To deal with this issue, we introduce SymSolve, a test generation based approach that, given a partially symbolic structure and a repOK, automatically decides if the structure can be extended to a fully concrete one satisfying repOK. As opposed to previous approaches, SymSolve does not require additional specifications. It works by exploring feasible concretizations of partially symbolic structures in a bounded-exhaustive manner, until it finds a fully concrete structure satisfying repOK, or it exhausts the search space, deeming the corresponding partially symbolic structure spurious. SymSolve exploits sound pruning of the search space, combined with symmetry breaking (to discard structures isomorphic to previously explored ones), to efficiently explore very large search spaces.
We incorporate SymSolve into LI in order to decide the feasibility of partially symbolic inputs, obtaining our LISSA technique. We experimentally assess LISSA against related techniques over various case studies, consisting of programs with heap-allocated inputs with complex constraints. The results show that LISSA is faster and scales better than related techniques.
Thu 13 OctDisplayed 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 20mResearch 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 10mVision 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 20mResearch 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 20mResearch 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 20mPaper | A Practical Approach for Dynamic Taint Tracking with Control-Flow RelationshipsVirtual Journal-first Papers Link to publication DOI Pre-print Media Attached | ||
15:00 20mResearch 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 |