String Solvers for Web Security

Presented as part of the 2013 HCSS conference.

ABSTRACT

Over the last decade, SMT solvers [1, 2] have made a huge impact in automatic bug-finding, analysis and verification of desktop software. More recently, string solvers are starting to have a similar impact on security analysis and vulnerability detection in web applications. String solvers provide a rich constraint language essential for security analysis of web applications, and recently have become efficient enough to be used at scale.

In this talk, I will present my experience in designing two successful string solvers aimed at finding a variety of security vulnerabilities including SQL Injection and XSS. In particular, I will present three results: First, I will talk about HAMPI [4, 5], a solver for string constraints over bounded string variables. Users of Hampi specify constraints using regular expressions, context-free grammars, equality between string terms (word equations), and typical string operations such as concatenation and substring extraction. Hampi then finds a solution string that either satisfies all input constraints or reports that they are unsatisfiable. I will illustrate Hampi's expressiveness and efficiency by discussing its use in static and dynamic analyses for finding security vulnerabilities in web applications with hundreds of thousands of lines of code. Second, I will discuss a new solver, Z3-str (under submission), that my collaborators (Yunhui Zheng and Professor Xiangyu Zhang of Purdue) and I recently built on top of the Z3 SMT solver [1]. Z3-str supports a unified logic for many non-string and string operations. For example, a user of Z3-str can specify equality between string terms (built using concatenation and extraction) and compare the length of strings using length functions. I will discuss how these solvers can be used through detailed examples, and the underlying techniques that enable these solvers to scale. Third, I will discuss some undecidability/decidability results for certain quantified fragment of the logic supported by Hampi [3].

I will conclude my talk with new techniques to enable greater scalability and usability of string solvers, issues regarding standardization of string solver languages, further integration of string solvers with non-string theories, and some open theoretical problems.

References

1. L. Moura and N. Bjorner. Z3: An Efficient SMT Solver. In TACAS'08.

2. V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In CAV'07.

3. V. Ganesh, M. Minnes, A. Solar-Lezama and M. Rinard. Word equations with length constraints: what's decidable? In HVC'12.

4. A. Kiezun, V. Ganesh, P. Guo, P. Hooimeijer and M. Ernst. HAMPI: a solver for string contraints. In ISSTA'09.

V. Ganesh, A Kiezun, S. Artzi, P. Guo, P. Hooimeijer and M. Ernst. HAMPI: a string solver for testing, analysis and vulnerability detection. In CAV'11.