HAMPI: a solver for string constraints

ABSTRACT

Many automatic testing, analysis, and verification techniques for programs can be effectively reduced to a constraint generation phase followed by a constraint-solving phase. This separation of concerns often leads to more effective and maintainable tools. The increasing efficiency of off-the-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 techniques for string-manipulating programs.

We designed and implemented Hampi, a solver for string constraints over fixed-size string variables. Hampi constraints express membership in regular languages and fixed-size context-free languages. Hampi constraints may contain context-free-language definitions, regular language definitions and operations, and the membership predicate. Given a set of constraints, Hampi outputs a string that satisfies all the constraints, or reports that the constraints are unsatisfiable.

Hampi is expressive and efficient, and can be successfully applied to testing and analysis of real programs. Our experiments use Hampi in: static and dynamic analyses for finding SQL injection vulnerabilities in Web applications; automated bug finding in C programs using systematic testing; and compare Hampi with another string solver. Hampi's source code, documentation, and the experimental data are available at http://people.csail.mit.edu/akiezun/hampi.

REFERENCES

• 1: Roland Axelsson , Keijo Heljanko , Martin Lange, Analyzing Context-Free Grammars Using an Incremental SAT Solver, Proceedings of the 35th international colloquium on Automata, Languages and Programming, Part II, July 07-11, 2008, Reykjavik, Iceland [doi>10.1007/978-3-540-70583-3_34]
• 2: A. Biere. Resolve and expand. In SAT, 2005.
• 3: A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. Advances in Computers, 2003.
• 4: N. Bjørner, N. Tillmann, and A. Voronkov. Path feasibility analysis for string-manipulating programs. In TACAS, 2009.
• 5: C. Cadar, D. Dunbar, and D. R. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, 2008.
• 6: Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: automatically generating inputs of death, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180405.1180445]
• 7: A. S. Christensen, A. Møller, and M. I. Schwartzbach. Precise analysis of string expressions. In SAS, 2003.
• 8: E. M. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS, 2004.
• 9: L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In TACAS, 2008.
• 10: Michael Emmi , Rupak Majumdar , Koushik Sen, Dynamic test input generation for database applications, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom [doi>10.1145/1273463.1273484]
• 11: Brics finite state automata utilities. http://www.brics.dk/automaton/faq.html.
• 12: Finite state automata utilities. http://www.let.rug.nl/~vannoord/Fsa/fsa.html.
• 13: AT&T FSM library. http://www.research.att.com/~fsmtools/fsm.
• 14: Xiang Fu , Xin Lu , Boris Peltsverger , Shijun Chen , Kai Qian , Lixin Tao, A Static Analysis Framework For Detecting SQL Injection Vulnerabilities, Proceedings of the 31st Annual International Computer Software and Applications Conference, p.87-96, July 24-27, 2007 [doi>10.1109/COMPSAC.2007.43]
• 15: V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In CAV, 2007.
• 16: Patrice Godefroid , Adam Kiezun , Michael Y. Levin, Grammar-based whitebox fuzzing, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 17: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 18: P. Godefroid, M. Y. Levin, and D. Molnar. Automated whitebox fuzz testing. In NDSS, 2008.
• 19: Sumit Gulwani , Saurabh Srivastava , Ramarathnam Venkatesan, Program analysis as constraint solving, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 20: William Halfond , Alex Orso , Pete Manolios, WASP: Protecting Web Applications Using Positive Tainting and Syntax-Aware Evaluation, IEEE Transactions on Software Engineering, v.34 n.1, p.65-81, January 2008 [doi>10.1109/TSE.2007.70748]
• 21: Pieter Hooimeijer , Westley Weimer, A decision procedure for subset constraints over regular languages, Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation, June 15-21, 2009, Dublin, Ireland
• 22: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 23: K. Jayaraman, D. Harvison, V. Ganesh, and A. Kie|un. jFuzz: A concolic whitebox fuzzer for Java. In NFM, 2009.
• 24: A. Kie|un, P. J. Guo, K. Jayaraman, and M. D. Ernst. Automatic creation of SQL injection and cross-site scripting attacks. In ICSE, 2009.
• 25: Nils Klarlund, Mona & Fido: The Logic-Automaton Connection in Practice, Selected Papers from the11th International Workshop on Computer Science Logic, p.311-326, August 23-29, 1997
• 26: Rupak Majumdar , Ru-Gang Xu, Directed test generation using symbolic grammars, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321653]
• 27: G. Makanin. The problem of solvability of equations in a free semigroup. Sbornik: Mathematics, 32(2), 1977.
• 28: Yasuhiko Minamide, Static approximation of dynamically generated Web pages, Proceedings of the 14th international conference on World Wide Web, May 10-14, 2005, Chiba, Japan [doi>10.1145/1060745.1060809]
• 29: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th annual Design Automation Conference, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 30: G. Pesant. A regular language membership constraint for finite sequences of variables. In CP, 2004.
• 31: C. Quimper and T. Walsh. Global grammar constraints. In CP, 2006.
• 32: Arcot Rajasekar, Applications in Constraint Logic Programming with Strings, Proceedings of the Second International Workshop on Principles and Practice of Constraint Programming, p.109-122, May 02-04, 1994
• 33: Hui Ruan , Jian Zhang , Jun Yan, Test Data Generation for C Programs with String-Handling Functions, Proceedings of the 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, p.219-226, June 17-19, 2008 [doi>10.1109/TASE.2008.25]
• 34: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 35: Daryl Shannon , Sukant Hajra , Alison Lee , Daiqian Zhan , Sarfraz Khurshid, Abstracting Symbolic Execution with String Analysis, Proceedings of the Testing: Academic and Industrial Conference Practice and Research Techniques - MUTATION, p.13-22, September 10-14, 2007
• 36: Michael Sipser, Introduction to the Theory of Computation, International Thomson Publishing, 1996
• 37: Gary Wassermann , Zhendong Su, Sound and precise analysis of web applications for injection vulnerabilities, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 38: Gary Wassermann , Zhendong Su, Static detection of cross-site scripting vulnerabilities, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany [doi>10.1145/1368088.1368112]
• 39: Gary Wassermann , Dachuan Yu , Ajay Chander , Dinakar Dhurjati , Hiroshi Inamura , Zhendong Su, Dynamic test input generation for web applications, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA [doi>10.1145/1390630.1390661]
• 40: Y. Xie and A. Aiken. Saturn: A scalable framework for error detection using Boolean satisfiability. In CAV, 2007.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

General Terms:
Algorithms, Reliability, Verification

Keywords:
context-free languages, regular languages, string constraints