Looping Structures in Symbolic Execution

Abstract

Software is everywhere, and going back to a life without software is unimaginable. Unfortunately, software does not always behave as expected, even though during the development cycle, software is usually tested to verify its correctness. To aid in testing, methods such as fuzzing or symbolic execution are used for automatic verification software systems. These methods are able to quickly find inputs to the systems that cover large portions of the code base. However, both of these methods struggle to find inputs that cover code which requires many iterations through loops.

In symbolic execution, loops are a large contributing factor to the path explosion problem and therefore the overall runtime. For loops containing conditional branches, each iteration is a new decision point. This leads to an exponential number of possible paths through a loop in comparison to the number of iterations.

In this work, we investigate the use of loops in symbolic execution to reach portions of the code which require numerous iterations through loops with conditional branches. We propose a novel technique for symbolic execution that uses the effects of one or more iterations through a loop to reach new parts of the code. By implementing this technique and applying it to a set of challenges designed to stress current tools and methods for software verification, we show that our technique is able to efficiently reach new parts of these challenges. These areas are not reached by state-of-the-art methods within the same time budget.

Another method for verifying software behavior is active learning, where simple models are learned from a system. These models capture the behavior of the system at a high level, allowing easier analysis to verify the behavior of a system. During the automatic learning of these models, loops are not handled separately. This leads to models where the behavior of a system is not captured fully, leading to incomplete analysis. We propose new methods for finding changes in behavior after executing these loops numerous times. We have compared our techniques to existing methods and show that this produces more complete models of a system.