Prateek Saxena and Pongsin Poosankam and Stephen McCamant and Dawn Song

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2009-34

March 2, 2009

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-34.pdf

Mixed concrete and symbolic execution is an important technique for finding and understanding software bugs, including security-relevant 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 program executions. To demonstrate our technique, we apply it to the problem of discovering and diagnosing buffer-overflow vulnerabilities in software given only in binary form. Our tool finds vulnerabilities in both a standard benchmark suite and 3 real-world applications, after generating only a handful of candidate inputs, and also diagnoses general vulnerability conditions.

---

BibTeX citation:

@techreport{Saxena:EECS-2009-34,
    Author= {Saxena, Prateek and Poosankam, Pongsin and McCamant, Stephen and Song, Dawn},
    Title= {Loop-Extended Symbolic Execution on Binary Programs},
    Year= {2009},
    Month= {Mar},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-34.html},
    Number= {UCB/EECS-2009-34},
    Abstract= {Mixed concrete and symbolic execution is an important technique for
finding and understanding software bugs, including security-relevant
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 program
executions. To demonstrate our technique, we apply it to the problem
of discovering and diagnosing buffer-overflow vulnerabilities in
software given only in binary form. Our tool finds vulnerabilities in
both a standard benchmark suite and 3 real-world applications, after
generating only a handful of candidate inputs, and also diagnoses
general vulnerability conditions.},
}

EndNote citation:

%0 Report
%A Saxena, Prateek 
%A Poosankam, Pongsin 
%A McCamant, Stephen 
%A Song, Dawn 
%T Loop-Extended Symbolic Execution on Binary Programs
%I EECS Department, University of California, Berkeley
%D 2009
%8 March 2
%@ UCB/EECS-2009-34
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-34.html
%F Saxena:EECS-2009-34