Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Loop-Extended Symbolic Execution on Binary Programs

Prateek Saxena, Pongsin Poosankam, Stephen McCamant and Dawn Song

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2009-34
March 2, 2009

http://www.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},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2009},
    Month = {Mar},
    URL = {http://www.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://www.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-34.html
%F Saxena:EECS-2009-34