University of Virginia Department of
    Computer Science

Monday, April 28, 2008
Pieter Hooimeijer

Chair: Dave Evans; Greg Humphreys
Advisor: Wes Weimer
OLSSON 228E, 3:30 PM

A Master's Thesis Presentation

Generating String Inputs using Constrained Symbolic Execution

ABSTRACT

The most commonly reported security vulnerabilities are related to cross-site scripting and SQL command injection. Both types of attack affect web applications that produce structured output such as SQL, XML, and HTML. Attacks that exploit these vulnerabilities are popular because web applications are ubiquitous, contain potentially valuable information, and are easily accessed remotely.

We present an efficient static analysis that detects SQL injection vulnerabilities and the execution paths
that lead to them. Our algorithm is based on recent work that models sets of string values using context-free grammars. We extend this analysis so that its output—a set of structured bug reports—can be used to generate symbolic constraints over string variables. Our algorithm then solves these constraints, yielding a full set of attack inputs for each vulnerability that is detected.

The output of our algorithm is significantly easier to verify than the bug reports of the original analysis; we support this claim with anecdotal evidence. We also allow the developer to place restrictions on the path generation algorithm. This feature, in the spirit of bounded software model checking, allows our algorithm to automatically rule out certain classes of false positives.

We empirically evaluate the soundness, completeness, and scalability of our implementation by applying it to a previously-published set of error reports.



Other Recent and Upcoming Colloquia