A decision procedure for subset constraints over regular languages

ABSTRACT

Reasoning about string variables, in particular program inputs, is an important aspect of many program analyses and testing frameworks. Program inputs invariably arrive as strings, and are often manipulated using high-level string operations such as equality checks, regular expression matching, and string concatenation. It is difficult to reason about these operations because they are not well-integrated into current constraint solvers.

We present a decision procedure that solves systems of equations over regular language variables. Given such a system of constraints, our algorithm finds satisfying assignments for the variables in the system. We define this problem formally and render a mechanized correctness proof of the core of the algorithm. We evaluate its scalability and practical utility by applying it to the problem of automatically finding inputs that cause SQL injection vulnerabilities.

REFERENCES

• 1: Stephen Adams , Thomas Ball , Manuvir Das , Sorin Lerner , Sriram K. Rajamani , Mark Seigle , Westley Weimer, Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis, Proceedings of the 9th International Symposium on Static Analysis, p.230-246, September 17-20, 2002
• 2: S. Bala. Regular language matching and other decidable cases of the satisfiability problem for constraints between regular open terms. In STACS, pages 596--607, 2004.
• 3: T. Ball, B. Cook, S. K. Lahiri, and L. Zhang. Zapato: Automatic theorem proving for predicate abstraction refinement. In Computer Aided Verification, pages 457--461, 2004.
• 4: Thomas Ball , Mayur Naik , Sriram K. Rajamani, From symptom to cause: localizing errors in counterexample traces, ACM SIGPLAN Notices, v.38 n.1, p.97-105, January 2003
• 5: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 6: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 7: Nikolaj Bjørner , Nikolai Tillmann , Andrei Voronkov, Path Feasibility Analysis for String-Manipulating Programs, Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009,, March 22-29, 2009, York, UK [doi>10.1007/978-3-642-00768-2_27]
• 8: British Broadcasting Corporation. UN's website breached by hackers. In http://news.bbc.co.uk/2/hi/technology/6943385.stm, Aug. 2007.
• 9: R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady. Deciding bit-vector arithmetic with abstraction. In Tools and Algorithms for the Construction and Analysis of Systems, pages 358--372, 2007.
• 10: 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]
• 11: A. S. Christensen, A. Møller, and M. I. Schwartzbach. Precise analysis of string expressions. In International Symposium on Static Analysis, pages 1--18, 2003.
• 12: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 13: L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337--340, 2008.
• 14: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 15: V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In Computer-Aided Verification, pages 519--531, 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. Levin, and D. Molnar. Automated whitebox fuzz testing. In Network Distributed Security Symposium (NDSS), 2008.
• 19: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , George C. Necula , Grégoire Sutre , Westley Weimer, Temporal-Safety Proofs for Systems Code, Proceedings of the 14th International Conference on Computer Aided Verification, p.526-538, July 27-31, 2002
• 20: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 21: K. J. Higgins. Cross-site scripting: attackers' new favorite flaw. Technical report, http://www.darkreading.com/document.asp?doc_id=103774&WT.svl=news1_1, Sept. 2006.
• 22: Pieter Hooimeijer , Westley Weimer, Modeling bug report quality, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321639]
• 23: Ranjit Jhala , Rupak Majumdar, Path slicing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 24: Nenad Jovanovic , Christopher Kruegel , Engin Kirda, Pixy: A Static Analysis Tool for Detecting Web Application Vulnerabilities (Short Paper), Proceedings of the 2006 IEEE Symposium on Security and Privacy, p.258-263, May 21-24, 2006 [doi>10.1109/SP.2006.29]
• 25: A. Kie|un, V. Ganesh, P. J. Guo, P. Hooimeijer, and M. D. Ernst. HAMPI: A solver for string constraints. technical report, Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory.
• 26: J. Kodumal and A. Aiken. Banshee: A scalable constraint-based analysis toolkit. In Static Analysis Symposium, pages 218--234, 2005.
• 27: Michal Kunc, The Power of Commuting with Finite Sets of Words, Theory of Computing Systems, v.40 n.4, p.521-551, June 2007 [doi>10.1007/s00224-006-1321-z]
• 28: M. Kunc. What do we know about language equations? In Developments in Language Theory, pages 23--27, 2007.
• 29: S. K. Lahiri, T. Ball, and B. Cook. Predicate abstraction via symbolic decision procedures. Logical Methods in Computer Science, 3(2), 2007.
• 30: 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]
• 31: Michael Martin , Benjamin Livshits , Monica S. Lam, Finding application errors and security flaws using PQL: a program query language, Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 32: 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]
• 33: 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]
• 34: Mayur Naik , Alex Aiken, Conditional must not aliasing for static race detection, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 35: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 36: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 37: Arto Salomaa , Kai Salomaa , Sheng Yu, State complexity of combined operations, Theoretical Computer Science, v.383 n.2-3, p.140-152, September, 2007 [doi>10.1016/j.tcs.2007.04.015]
• 38: Koushik Sen, Race directed random testing of concurrent programs, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 39: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 40: Aaron Stump , Clark W. Barrett , David L. Dill, CVC: A Cooperating Validity Checker, Proceedings of the 14th International Conference on Computer Aided Verification, p.500-504, July 27-31, 2002
• 41: Zhendong Su , Gary Wassermann, The essence of command injection attacks in web applications, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.372-382, January 11-13, 2006, Charleston, South Carolina, USA
• 42: Peter Thiemann, Grammar-based analysis of string expressions, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.59-70, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040300]
• 43: 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
• 44: 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]
• 45: 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]
• 46: Westley Weimer, Patches as better bug reports, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA [doi>10.1145/1173706.1173734]
• 47: Yichen Xie , Alex Aiken, Static detection of security vulnerabilities in scripting languages, Proceedings of the 15th conference on USENIX Security Symposium, July 31-August 04, 2006, Vancouver, B.C., Canada
• 48: Yichen Xie , Alex Aiken, Saturn: A scalable framework for error detection using Boolean satisfiability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.3, p.16-es, May 2007 [doi>10.1145/1232420.1232423]
• 49: Fang Yu , Tevfik Bultan , Marco Cova , Oscar H. Ibarra, Symbolic String Verification: An Automata-Based Approach, Proceedings of the 15th international workshop on Model Checking Software, August 10-12, 2008, Los Angeles, CA, USA [doi>10.1007/978-3-540-85114-1_21]
• 50: Fang Yu , Tevfik Bultan , Oscar H. Ibarra, Symbolic String Verification: Combining String Analysis and Size Analysis, Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009,, March 22-29, 2009, York, UK [doi>10.1007/978-3-642-00768-2_28]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking; Validation

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
decision procedure, regular language