×

An efficient SMT solver for string constraints. (English) Zbl 1404.68135

Summary: An increasing number of applications in verification and security rely on or could benefit from automatic solvers that can check the satisfiability of constraints over a diverse set of data types that includes character strings. Until recently, satisfiability solvers for strings were standalone tools that could reason only about fairly restricted fragments of the theory of strings and regular expressions (e.g., strings of bounded lengths). These solvers were based on reductions to satisfiability problems over other data types such as bit vectors or to automata decision problems. We present a set of algebraic techniques for solving constraints over a rich theory of unbounded strings natively, without reduction to other problems. These techniques can be used to integrate string reasoning into general, multi-theory SMT solvers based on the common \(\mathrm{DPLL}(T)\) architecture. We have implemented them in our SMT solver cvc4, expanding its already large set of built-in theories to include a theory of strings with concatenation, length, and membership in regular languages. This implementation makes cvc4 the first solver able to accept a rich set of mixed constraints over strings, integers, reals, arrays and algebraic datatypes. Our initial experimental results show that, in addition, on pure string problems cvc4 is highly competitive with specialized string solvers accepting a comparable input language.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abdulla PA, Atig MF, Chen YF, Holik L, Rezine A, Rummer P, Stenman J (2014) String constraints for verification. In: Biere A, Bloem R (eds) Proceedings of the 26th international conference on computer aided verification. Lecture notes in computer science, vol. 8559. Springer, Berlin · Zbl 0452.68013
[2] Barrett C, Nieuwenhuis R, Oliveras A, Tinelli C (2006) Splitting on demand in SAT modulo theories. In: Proceedings of LPAR’06. Lecture notes in computer science, vol. 4246. Springer, Berlin, pp 512-526 · Zbl 1165.68480
[3] Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories. In: Biere A, Heule MJH, van Maaren H, Walsh T (eds) Handbook of satisfiability, vol 185, chap 26. IOS Press, Amsterdam, pp 825-885
[4] Bjørner N, Tillmann N, Voronkov A (2009) Path feasibility analysis for string-manipulating programs. In: Proceedings of the 15th international conference on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science. Springer, pp 307-321 · Zbl 1234.68070
[5] Brumley D, Caballero J, Liang Z, Newsome J (2007) Towards automatic discovery of deviations in binary implementations with applications to error detection and fingerprint generation. In: Proceedings of the 16th USENIX security symposium, Boston, MA, USA, 6-10 August 2007 · Zbl 1326.68164
[6] Brumley D, Wang H, Jha S, Song DX (2007) Creating vulnerability signatures using weakest preconditions. In: 20th IEEE computer security foundations symposium, CSF 2007, 6-8 July 2007, Venice, Italy, pp 311-325
[7] Christensen AS, Møller A, Schwartzbach MI (2003) Precise analysis of string expressions. In: Proceedings of the 10th international conference on static analysis. Lecture notes in computer science. Springer, Berlin, pp 1-18 · Zbl 1067.68541
[8] De Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Proceedings of the theory and practice of software, 14th international conference on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science. Springer, Berlin, pp 337-340
[9] Egele M, Kruegel C, Kirda E, Yin H, Song D (2007) Dynamic spyware analysis. In: 2007 USENIX annual technical conference on proceedings of the USENIX annual technical conference, ATC’07. USENIX Association, Berkeley, CA, USA, pp 18:1-18:14
[10] Fu X, Li C (2010) A string constraint solver for detecting web application vulnerability. In: Proceedings of the 22nd international conference on software engineering and knowledge engineering, SEKE’2010. Knowledge Systems Institute Graduate School, Skokie
[11] Ganesh V, Minnes M, Solar-Lezama A, Rinard M (2013) Word equations with length constraints: what’s decidable? In: Proceedings of the 8th international conference on hardware and software: verification and testing, HVC’12. Springer, Berlin, pp 209-226
[12] Ghosh I, Shafiei N, Li G, Chiang W (2013) JST: an automatic test generation tool for industrial Java applications with strings. In: Proceedings of the 2013 international conference on software engineering, ICSE’13. IEEE Press, Piscataway, pp. 992-1001
[13] Hooimeijer P, Veanes M (2011) An evaluation of automata algorithms for string analysis. In: Proceedings of the 12th international conference on verification, model checking, and abstract interpretation. Springer, Berlin, pp 248-262 · Zbl 1317.68287
[14] Hooimeijer P, Weimer W (2009) A decision procedure for subset constraints over regular languages. In: Proceedings of the 2009 ACM SIGPLAN conference on programming language design and implementation. ACM, Dublin, pp 188-198
[15] Hooimeijer P, Weimer W (2010) Solving string constraints lazily. In: Proceedings of the IEEE/ACM international conference on automated software engineering. ACM, New York, pp 377-386
[16] Kiezun A, Ganesh V, Guo PJ, Hooimeijer P, Ernst MD (2009) HAMPI: a solver for string constraints. In: Proceedings of the eighteenth international symposium on Software testing and analysis. ACM, New York, pp 105-116 · Zbl 0452.68013
[17] Li G, Ghosh I (2013) PASS: string solving with parameterized array and interval automaton. In: Bertacco V, Legay A (eds) Hardware and software: verification and testing. Lecture notes in computer science, vol 8244. Springer, Berlin, pp 15-31
[18] Liang T, Reynolds A, Tinelli C, Barrett C, Deters M (2014) A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere A, Bloem R (eds) Proceedings of the 26th international conference on computer aided verification. Lecture notes in computer science, vol 8559. Springer, Berlin
[19] Liang T, Tsiskaridze N, Reynolds A, Tinelli C, Barrett C (2015) A decision procedure for regular membership and length constraints over unbounded strings. In: Frontiers of combining systems. Springer, Berlin, pp 135-150 · Zbl 1471.68119
[20] Makanin GS (1977) The problem of solvability of equations in a free semigroup. English transl. in Math USSR Sbornik, vol 32, pp 147-236 · Zbl 0371.20047
[21] Namjoshi KS, Narlikar GJ (2010) Robust and fast pattern matching for intrusion detection. In: INFOCOM 2010. 29th IEEE international conference on computer communications, joint conference of the IEEE computer and communications societies, 15-19 March 2010, San Diego, CA, USA, pp 740-748
[22] Nelson G, Oppen DC (1979) Simplification by cooperating decision procedures. ACM Trans Program Lang Syst 1(2):245-257 · Zbl 0452.68013 · doi:10.1145/357073.357079
[23] Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT Modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J ACM 53(6):937-977 · Zbl 1326.68164 · doi:10.1145/1217856.1217859
[24] Perrin, D.; Ait-Kaci, H. (ed.); Nivat, M. (ed.), Equations in words, No. 2, 275-298 (1989), Cambridge
[25] Plandowski W (2004) Satisfiability of word equations with constants is in PSPACE. J ACM 51(3):483-496 · Zbl 1192.68372 · doi:10.1145/990308.990312
[26] Saxena P, Akhawe D (2010) Kaluza web site. http://webblaze.cs.berkeley.edu/2010/kaluza/
[27] Saxena P, Akhawe D, Hanna S, Mao F, McCamant S, Song D (2010) A symbolic execution framework for JavaScript. In: Proceedings of the 2010 IEEE symposium on security and privacy. IEEE Computer Society, pp 513-528
[28] Stump A, Sutcliffe G, Tinelli C (2014) Starexec: a cross-community infrastructure for logic solving. In: Demri S, Kapur D, Weidenbach C (eds) Proceedings of the 7th international joint conference on automated reasoning. Lecture notes in artificial intelligence. Springer, Berlin · Zbl 06348250
[29] Tillmann N, Halleux J (2008) Pex—white box test generation for .NET. In Beckert B, Hähnle R (eds) Tests and proofs. Lecture notes in computer science, vol 4966. Springer, Berlin, pp 134-153 · Zbl 1326.68164
[30] Tinelli C, Harandi MT (1996) A new correctness proof of the Nelson-Oppen combination procedure. In: Baader F, Schulz KU (eds) Frontiers of combining systems: proceedings of the 1st international workshop (Munich, Germany). Applied logic. Kluwer Academic Publishers, Dordrecht, pp 103-120 · Zbl 0893.03001
[31] Trinh MT, Chu DH, Jaffar J (2014) S3: a symbolic string solver for vulnerability detection in web applications. In: Yung M, Li N (eds) Proceedings of the 21st ACM conference on computer and communications security. ACM, New York, pp 1232-1243
[32] Veanes M (2013) Applications of symbolic finite automata. In: Proceedings of the 18th international conference on implementation and application of automata, CIAA’13. Springer, Berlin, pp 16-23 · Zbl 1298.68160
[33] Veanes M, Bjørner N, De Moura L (2010) Symbolic automata constraint solving. In: Proceedings of the 17th international conference on logic for programming, artificial intelligence, and reasoning. Lecture notes in computer science. Springer, Berlin, pp 640-654 · Zbl 1306.68097
[34] Yu F, Alkhalaf M, Bultan T (2010) Stranger: an automata-based string analysis tool for php. In: Esparza J, Majumdar R (eds) Tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 6015. Springer, Berlin, pp 154-157
[35] Zheng Y, Zhang X, Ganesh V (2013) Z3-str: a Z3-based string solver for web application analysis. In: Proceedings of the 2013 9th joint meeting on foundations of software engineering, ESEC/FSE 2013. ACM, New York, pp 114-124
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.