Loop-extended symbolic execution on binary programs

Mixed concrete and symbolic execution is an important technique for finding and understanding software bugs, including securityrelevant ones. However, existing symbolic execution techniques are limited to examining one execution path at a time, in which symbolic variables reflect only direct data dependencies. We introduce loop-extended symbolic execution, a generalization that broadens the coverage of symbolic results in programs with loops. It introduces symbolic variables for the number of times each loop executes, and links these with features of a known input grammar such as variable-length or repeating fields. This allows the symbolic constraints to cover a class of paths that includes different numbers of loop iterations, expressing loop-dependent program values in terms of properties of the input. By performing more reasoning symbolically, instead of by undirected exploration, applications of loop-extended symbolic execution can achieve better results and/or require fewer p...

• Type: Conference
• Year: 2009
• Where: ISSTA
• Authors: Prateek Saxena, Pongsin Poosankam, Stephen McCamant, Dawn Song
• Keywords: ISSTA 2009, Loop-extended Symbolic Execution, Software Engineering, Symbolic Execution, Symbolic Variables