Memory Models in Symbolic Execution: Key Ideas and New Thoughts

Symbolic execution is a popular program analysis technique that allows seeking for bugs by reasoning over multiple alternative execution states at once. As the number of states to explore may grow exponentially, a symbolic executor may quickly run out of space. For instance, a memory access to a symbolic address may potentially reference the entire address space, leading to a combinatorial explosion of the possible resulting execution states. To cope with this issue, state-of-the-art executors either concretize symbolic addresses that span memory intervals larger than some threshold or rely on advanced capabilities of modern SMT solvers. Unfortunately, concretization may result in missing interesting execution states, e.g., where a bug arises, while offloading the entire problem to constraint solvers can lead to very large query times. In this article, we first contribute to systematizing knowledge about memory models for symbolic execution, discussing how four mainstream symbolic executors deal with symbolic addresses. We then introduce ourname, a new approach to symbolic memory that reduces the need for concretization: %, hence offering the opportunity for broader state explorations and more precise pointer reasoning. rather than mapping address instances to data as previous approaches do, our technique maps symbolic address expressions to data, maintaining the possible alternative states resulting from the memory referenced by a symbolic address in a compact, implicit form. Experiments on prominent programs show that ourname, which we implemented in both angr and klee, enables the exploration of states that are unreachable for memory models that perform concretization, and provides a performance level comparable to memory models relying on advanced solver theories.