Automatic partial loop summarization in dynamic test generation
- 17 July 2011
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
Abstract
Whitebox fuzzing extends dynamic test generation based on symbolic execution and constraint solving from unit testing to whole-application security testing. Unfortunately, input-dependent loops may cause an explosion in the number of constraints to be solved and in the number of execution paths to be explored. In practice, whitebox fuzzers arbitrarily bound the number of constraints and paths due to input-dependent loops, at the risk of missing code and bugs. In this work, we investigate the use of simple loop-guard pattern-matching rules to automatically guess an input constraint defining the number of iterations of input-dependent loops during dynamic symbolic execution. We discover the loop structure of the program on the fly, detect induction variables, which are variables modified by a constant value during loop iterations, and infer simple partial loop invariants relating the value of such variables. Whenever a guess is confirmed later during the current dynamic symbolic execution, we then inject new constraints representing pre and post loop conditions, effectively summarizing sets of executions of that loop. These pre and post conditions are derived from partial loop invariants synthesized dynamically using pattern-matching rules on the loop guards and induction variables, without requiring any static analysis, theorem proving, or input-format specification. This technique has been implemented in the whitebox fuzzer SAGE, scales to large programs with many nested loops, and we present results of experiments with a Windows 7 image parser.Keywords
This publication has 11 references indexed in Scilit:
- Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit-State Model CheckingIEEE Transactions on Software Engineering, 2010
- Compositional may-must program analysisPublished by Association for Computing Machinery (ACM) ,2010
- A Symbolic Execution Framework for JavaScriptPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2010
- Loop-extended symbolic execution on binary programsPublished by Association for Computing Machinery (ACM) ,2009
- Software Model Checking Improving Security of a Billion ComputersLecture Notes in Computer Science, 2009
- Dynamic test input generation for database applicationsPublished by Association for Computing Machinery (ACM) ,2007
- Compositional dynamic test generationPublished by Association for Computing Machinery (ACM) ,2007
- EXEPublished by Association for Computing Machinery (ACM) ,2006
- Boogie: A Modular Reusable Verifier for Object-Oriented ProgramsLecture Notes in Computer Science, 2006
- DARTPublished by Association for Computing Machinery (ACM) ,2005