HAMPI: A Solver for String Theories
Strings are used everywhere from Web apps written in PHP/JavaScript to programs written in Java/C/C++. Analysis of such programs usually results in string constraints, i.e., formulas that are constructed out of string variables, constants, concat, extract and string comparison. In addition, many of these programs have sanitization code that are constructed out of regular expressions and context-free grammars. In order to support the analysis of string-manipulating programs we wrote HAMPI, a solver for string constraints. HAMPI has been used in more than a dozen projects from static to dynamic analysis, from testing to vulnerability detection.
In this talk, I will introduce a theory of strings supported by HAMPI, examples of how HAMPI can be used, and I will explain how HAMPI works.
Vijay Ganesh, MIT, Cambridge, USA
Dr. Vijay Ganesh is a Research Scientist at MIT since October 2007, and he will join IMDEA as an assistant professor in late 2011/early 2012. He completed his PhD in computer science from Stanford University in September 2007. He also has two MS degrees in computer science and electrical engineering, both from Stanford University, and Bachelor of Technology degree from College of Engineering, Trivandrum, India.
His primary research interests are constraint solvers (SAT/SMT solvers), and their applications to software reliability, computer security and biology. He works on both the theory and practice of constraint solvers. He has designed and implemented several constraint solvers, most notably, STP and HAMPI. STP was one of the first solvers to enable an exciting new testing technique called systematic dynamic testing (or concolic testing). STP has been used in more than 100 research projects relating to software reliability and computer security. More recently he designed another solver, HAMPI, aimed at solving string constraints generated by the analysis of PHP, JavaScript and Perl programs. His paper on HAMPI won the ACM Distinguished Paper Award (2009). STP was the co-winner of the SMTCOMP competition for bit-vector solvers in 2006, and the winner in 2010. Dr. Ganesh has also done research in automated software testing, in particular, whitebox fuzzing, and hardware archictecture description languages.
Besides his primary research interest, Dr. Ganesh is also interested in self-adaptive software (self-* programming), i.e., software that adapts itself to the environment. His other interests include quantum information theory and quantum computing.