Automatic verification of string manipulating programs

In this dissertation, we investigate the string verification problem: Given a program that manipulates strings, we want to verify assertions about string variables. We formalize the string verification problem as reachability analysis of string systems and demonstrate that the string analysis problem is undecidable in general. 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.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 use our automata-based string analysis techniques to detect and prevent such 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. Our approach is capable of generating relational vulnerability signatures (and corresponding sanitization statements) for vulnerabilities that are due to more than one input.We 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.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.