Dynamic symbolic execution is a powerful program analysis technique but often limited by the path-explosion problem, particularly in the presence of heavily branching loops. In this paper, we introduce sparse symbolic loop execution (SSLE), a novel approach aimed at mitigating this issue.
In symbolic execution, program paths are internally represented by states. SSLE observes the edge patterns of sibling states, spawned from the same loop, at program branches up to a pre-computed loop-impact barrier. States that exhibit unique patterns of taken edges are selected for further exploration, while others are postponed.
We implemented SSLE in a prototype called SparKLE and evaluated it on a set of 8 benchmarks against the popular symbolic execution engine KLEE. SSLE shows promising results and could increase line coverage by up to 55% in 1 hour runs using a depth-first-search heuristic. In other cases up to 99.997% of states could be postponed without any loss in coverage. Our planned evaluation will include a diverse set of 50 real-world benchmarks and will aim to better understand the effectiveness of SparKLE in handling symbolic loops, and how it compares with less complex approaches.
Mon 16 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:30 - 17:00 | |||
15:30 15mTalk | Sparse Symbolic Loop Execution FUZZING Frank Busse Imperial College London, Martin Nowack Imperial College London, Cristian Cadar Imperial College London | ||
15:45 15mTalk | LOOL: Low-Overhead, Optimization-Log-Guided Compiler Fuzzing FUZZING Florian Schwarcz Johannes Kepler University Linz, Felix Berlakovich μCSRL, CODE Research Institute, University of the Bundeswehr Munich, Gergö Barany Oracle Labs, Hanspeter Mössenböck JKU Linz | ||
16:00 15mTalk | The Havoc Paradox in Generator-Based Fuzzing FUZZING Ao Li Carnegie Mellon University, Madonna Huang University of British Columbia, Caroline Lemieux University of British Columbia, Rohan Padhye Carnegie Mellon University | ||
16:15 15mTalk | Understanding and Improving Coverage Tracking with AFL++ FUZZING Vasil Sarafov μCSRL, CODE Research Institute, University of the Bundeswehr Munich, David Markvica μCSRL, CODE Research Institute, University of the Bundeswehr Munich, Felix Berlakovich μCSRL, CODE Research Institute, University of the Bundeswehr Munich, Matthias Bernad μCSRL, CODE Research Institute, University of the Bundeswehr Munich, Stefan Brunthaler μCSRL, CODE Research Institute, University of the Bundeswehr Munich | ||
16:30 30mDay closing | Concluding Remarks FUZZING | ||