Wednesday, May 12th, 2010
1:00 – CS Conference Room
Committee: Tevfik Bultan (chair), Oscar H. Ibarra, Richard Kemmerer
Title: Automatic Verification of String Manipulating Programs
Most important Web application vulnerabilities, such as SQL Injection, Cross Site Scripting and Malicious File Execution, are due to inadequate manipulation of string variables. We present sound automata-based symbolic string analysis techniques for automatic verification of string manipulating programs. String analysis is a static analysis technique that determines the values that a string expression can take during program execution at a given program point. This information can be used to detect security vulnerabilities and program errors, and to verify that program inputs are sanitized properly. We use our automata-based string analysis techniques to detect and prevent string related vulnerabilities in Web applications.
Our approach consists of three phases: Given an attack pattern, we first conduct a vulnerability analysis to identify if strings that match the attack pattern can reach security-sensitive functions. Next, we compute the vulnerability signature which characterizes all input strings that can exploit the discovered vulnerability. Given the vulnerability signature, we then construct sanitization statements that 1) check if a given input matches the vulnerability signature and 2) modify the input in a minimal way so that the modified input does not match the vulnerability signature.
We further extend our automata-based approach to analyze systems with both string and integer variables. We present a composite symbolic verification technique that combines string and size analyses with the goal of improving the precision of both. Our composite analysis automatically discovers the relationships among the integer variables and the lengths of the string variables. Finally, we present a relational string verification technique based on multi-track automata and abstraction. Our approach is capable of verifying properties that depend on relations among string variables and generating relational vulnerability signatures (and corresponding sanitization statements) for vulnerabilities that are due to more than one input.
We have developed a tool called Stranger that implements our automata-based symbolic string analysis approach. Stranger can be used to find and eliminate string-related security vulnerabilities in PHP applications.