In this talk, I will present automata-based symbolic string analysis techniques. The goal of string analysis is to identify and eliminate string manipulation errors in software applications. According to the Open Web Application Security Project (OWASP)'s top ten list that identifies the most serious web application vulnerabilities, the top three vulnerabilities are: 1) Cross Site Scripting (XSS), 2) Injection Flaws (such as SQL injection) and 3) Malicious File Execution (MFE). All these vulnerabilities involve string manipulation operations and they occur due to inadequate sanitization and use of input strings provided by users.

Our string analysis techniques are capable of: (1) identifying vulnerable programs with respect to specific attack patterns, as well as generating vulnerability signatures, and (2) checking sanitization routines and proving their correctness. Our approach combines forward and backward reachability analyses based on symbolic automata constructions and operations including a language-based replacement operation. Using forward reachability analysis, we compute an over-approximation of all possible values that string variables can take at each program point. If this conservative approximation does not include any attack pattern, we conclude that the program does not contain any errors or vulnerabilities. Otherwise, intersecting these with the attack patterns produces the potential attack strings. Using backward analysis we automatically generate string-based vulnerability signatures, i.e., a characterization of all malicious inputs that can be used to generate attack strings. In addition to identifying existing vulnerabilities and their causes, these vulnerability signatures can be used to filter out malicious inputs and generate effective patches of the application.

Based on the presented techniques, we have implemented Stranger, an automata-based string analysis tool for finding and eliminating string-related security vulnerabilities in PHP applications. Stranger and several benchmarks can be downloaded from http://www.cs.ucsb.edu/~vlab/stranger.

Fang Yu is the fifth year PhD student in the VLab of the Department of Computer Science at the University of California, Santa Barbara. His research interests include software verification, formal methods, automata theory, membrane computing and web security. Fang Yu received his Bachelor's Degree in 1998 and Master's Degree in 2000 from the Department of Information Management at the National Taiwan University. From 2000 to 2005, he worked in the Verification Automation Lab of the Institute of Information Science at Academia Sinica, Taiwan.