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.
|Commitee:||Ibarra, Oscar H., Kemmerer, Richard|
|School:||University of California, Santa Barbara|
|School Location:||United States -- California|
|Source:||DAI-B 71/10, Dissertation Abstracts International|
|Keywords:||Automatic verification, Security, String analysis, Web applications|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be