Precise pointer reasoning for dynamic test generation

Dynamic test generation consists of executing a program while gathering symbolic constraints on inputs from predicates encountered in branch statements, and of using a constraint solver to infer new program inputs from previous constraints in order to steer next executions towards new program paths. Variants of this technique have recently been adopted in several bug detection tools, including our whitebox fuzzer SAGE, which has found dozens of new expensive security-related bugs in many Windows applications and is now routinely used in various Microsoft groups. In this paper, we discuss how to perform precise symbolic pointer reasoning in the context of dynamic test generation. We present a new memory model for representing arbitrary symbolic pointer dereferences to memory regions accessible by a program during its execution, and show that this memory model is the most precise one can hope for in our context, under some realistic assumptions. We also describe how the symbolic constra...

• Type: Conference
• Year: 2009
• Where: ISSTA
• Authors: Bassem Elkarablieh, Patrice Godefroid, Michael Y. Levin
• Keywords: Dynamic Test Generation, ISSTA 2009, Software Engineering, Symbolic Pointer, Symbolic Pointer Reasoning