Precise Pointer Reasoning for Dynamic Test Generation

Dynamic test generation consists of executing a program while gathering symbolic constraints on inputs from predi-cates encountered in branch statements, and of using a con-straint solver to infer new program inputs from previous con-straints in order to steer next executions towards new pro-gram paths. Variants of this technique have recently been adopted in several bug detection tools, including our white-box 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 mem-ory model is the most precise one can hope for in our con-text, under some realistic assumptions. We also describe how the symbolic constraints generated by our model can be solved using modern SMT solvers, which provide powerful constructs for reasoning about bit-vectors and arrays. This new memory model has been implemented in SAGE, and we present results of experiments with several large Windows applications showing that an increase in precision can often be obtained at a reasonable cost. Better precision in sym-bolic pointer reasoning means more relevant constraints and fewer imprecise ones, hence better test coverage, more bugs found and fewer redundant test cases. 1