HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection.

Many automatic testing, analysis, and verification techniques for programs can effectively be reduced to a constraint-generation phase followed by a constraint-solving phase. This separation of concerns often leads to more effective and maintainable software reliability tools. The increasing efficiency of offthe-shelf constraint solvers makes this approach even more compelling. However, there are few effective and sufficiently expressive off-the-shelf solvers for string constraints generated by analysis of string-manipulating programs, and hence researchers end up implementing their own ad-hoc solvers. Thus, there is a clear need for an effective and expressive string-constraint solver that can be easily integrated into a variety of applications. To fulfill this need, we designed and implemented Hampi, an efficient and easy-to-use string solver. Users of the Hampi string solver specify constraints using membership predicate over regular expressions, context-free grammars, and equality/dis-equality between string terms. These terms are constructed out of string constants, bounded string variables, and typical string operations such as concatenation and substring extraction. Hampi takes such a constraint as input and decides whether it is satisfiable or not. If an input constraint is satisfiable, Hampi generates a satsfying assignment for the string variables that occur in it. We demonstrate Hampi's expressiveness and efficiency by applying it to program analysis and automated testing: We used Hampi in static and dynamic analyses for finding SQL injection vulnerabilities in Web applications with hundreds of thousands of lines of code.We also used Hampi in the context of automated bug finding in C programs using dynamic systematic testing (also known as concolic testing). Hampi's source code, documentation, and experimental data are available at http://people.csail.mit.edu/akiezun/hampi