research-article

Flatten and conquer: a framework for efficient analysis of string constraints

Authors:

Parosh Aziz Abdulla,

Mohamed Faouzi Atig,

Lukáš Holík,

Philipp RümmerAuthors Info & Claims

PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 602 - 617

https://doi.org/10.1145/3062341.3062384

Published: 14 June 2017 Publication History

Abstract

We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.

Supplementary Material

Auxiliary Archive (pldiae.tar.gz)

Supplemental file

Download
5357.66 MB

References

[1]

P. A. Abdulla, B. Jonsson, M. Nilsson, and M. Saksena. A survey of regular model checking. In CONCUR’04, volume 170 of LNCS, pages 348–360. Springer, 2004.

[2]

P. A. Abdulla, M. F. Atig, Y. Chen, L. Hol´ık, A. Rezine, P. Rümmer, and J. Stenman. String constraints for verification. In CAV’14, volume 8559 of LNCS, pages 150–166. Springer, 2014.

Digital Library

[3]

P. A. Abdulla, M. F. Atig, Y. Chen, L. Hol´ık, A. Rezine, P. Rümmer, and J. Stenman. Norn: An SMT solver for string constraints. In CAV’15, volume 9206 of LNCS, pages 462– 469. Springer, 2015.

[4]

M. F. Atig, A. Bouajjani, and T. Touili. On the reachability analysis of acyclic networks of pushdown systems. In CONCUR’08, volume 5201 of LNCS, pages 356–371. Springer, 2008.

Digital Library

[5]

M. F. Atig, K. N. Kumar, and P. Saivasan. Acceleration in multi-pushdown systems. In TACAS’16, volume 9636 of LNCS, pages 698–714. Springer, 2016.

Digital Library

[6]

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi´c, T. King, A. Reynolds, and C. Tinelli. CVC4. In TACAS’11, LNCS, pages 171–177. Springer, 2011.

Digital Library

[7]

A. Brillout, D. Kroening, P. Rümmer, and T. Wahl. An interpolating sequent calculus for quantifier-free Presburger arithmetic. Journal of Automated Reasoning, 47:341–367, 2011.

Digital Library

[8]

J. R. Büchi and S. Senger. Definability in the existential theory of concatenation and undecidable extensions of this theory. Z. Math. Logik Grundlagen Math., 34(4), 1988.

[9]

A. Cimatti, A. Griggio, B. J. Schaafsma, and R. Sebastiani. The MathSAT5 SMT solver. In TACAS’13, LNCS, pages 93– 107. Springer, 2013.

Digital Library

[10]

B. Courcelle. On constructing obstruction sets of words. Bulletin of the EATCS, (44):178–186, 1991.

[11]

L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS’08, volume 4963 of LNCS, pages 337–340. Springer, 2008.

Digital Library

[12]

B. Dutertre. Yices 2.2. In CAV’14, volume 8559 of LNCS, pages 737–744. Springer, July 2014.

Digital Library

[13]

J. Esparza and P. Ganty. Complexity of pattern-based verification for multithreaded programs. In POPL’11, pages 499–510. ACM, 2011.

Digital Library

[14]

J. Esparza, P. Ganty, S. Kiefer, and M. Luttenberger. Parikh’s theorem: A simple and direct automaton construction. Inf. Process. Lett., 111(12):614–619, 2011.

Digital Library

[15]

J. Esparza, P. Ganty, and R. Majumdar. A perfect model for bounded verification. In LICS’12, pages 285–294. IEEE Computer Society, 2012.

Digital Library

[16]

J. Esparza, P. Ganty, and T. Poch. Pattern-based verification for multithreaded programs. ACM Trans. Program. Lang. Syst., 36(3):9:1–9:29, 2014.

Digital Library

[17]

V. Ganesh and M. Berzish. Undecidability of a theory of strings, linear arithmetic over length, and string-number conversion. CoRR, abs/1605.09442, 2016.

[18]

V. Ganesh, M. Minnes, A. Solar-Lezama, and M. Rinard. Word equations with length constraints: What’s decidable? In A. Biere, A. Nahir, and T. Vos, editors, Hardware and Software: Verification and Testing, volume 7857 of LNCS, pages 209–226. 2013.

Digital Library

[19]

P. Ganty, R. Majumdar, and B. Monmege. Bounded underapproximations. Formal Methods in System Design, 40(2): 206–231, 2012.

Digital Library

[20]

S. Ginsburg. The Mathematical Theory of Context-Free Languages. McGraw-Hill, Inc., 1966.

Digital Library

[21]

S. Ginsburg and E. H. Spanier. Bounded algol-like languages. Transactions of the American Mathematical Society, 113(2): 333–368, 1964.

[22]

P. Godefroid, A. Kiezun, and M. Y. Levin. Grammar-based whitebox fuzzing. SIGPLAN Not., 43(6):206–215, June 2008.

Digital Library

[23]

S. Kausler and E. Sherman. Evaluation of string constraint solvers in the context of symbolic execution. In ASE ’14, pages 259–270. ACM, 2014.

Digital Library

[24]

A. Kiezun, V. Ganesh, P. J. Guo, P. Hooimeijer, and M. D. Ernst. HAMPI: A Solver for String Constraints. In ISSTA’09, pages 105–116. ACM, 2009.

Digital Library

[25]

T. Liang, A. Reynolds, C. Tinelli, C. Barrett, and M. Deters. A DPLL(T) theory solver for a theory of strings and regular expressions. In CAV’14, volume 8559 of LNCS, pages 646– 662. Springer, 2014.

Digital Library

[26]

T. Liang, A. Reynolds, C. Tinelli, C. Barrett, and M. Deters. CVC4, 2016.

[27]

A. W. Lin and P. Barcel´o. String solving with word equations and transducers: towards a logic for analysing mutation XSS. In POPL’16, pages 123–136. ACM, 2016.

Digital Library

[28]

Z. Long, G. Calin, R. Majumdar, and R. Meyer. Languagetheoretic abstraction refinement. In FASE’12, volume 7212 of LNCS, pages 362–376. Springer, 2012.

Digital Library

[29]

R. Madhavan, M. Mayer, S. Gulwani, and V. Kuncak. Automating grammar comparison. SIGPLAN Not., 50(10):183– 200, Oct. 2015.

Digital Library

[30]

G. Makanin. The problem of solvability of equations in a free semigroup. Mathematics of the USSR-Sbornik, 32(2): 129–198, 1977.

[31]

Y. Matiyasevich. Computation paradigms in light of hilberts tenth problem. In New Computational Paradigms, pages 59– 85. Springer, New York, 2008.

[32]

M. Mohri and M.-J. Nederhof. Regular Approximation of Context-Free Grammars through Transformation, pages 153– 163. Springer Netherlands, Dordrecht, 2001.

[33]

R. Parikh. On context-free languages. J. ACM, 13(4), 1966.

Digital Library

[34]

W. Plandowski. Satisfiability of word equations with constants is in PSPACE. In FOCS, pages 495–500, 1999.

Digital Library

[35]

W. Plandowski. An efficient algorithm for solving word equations. In STOC, pages 467–476, 2006.

Digital Library

[36]

W. V. Quine. Concatenation as a basis for arithmetic. The Journal of Symbolic Logic, 11(4):105–114, 1946.

[37]

J. M. Robson and V. Diekert. On quadratic word equations. In STACS, pages 217–226, 1999.

Digital Library

[38]

P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song. A Symbolic Execution Framework for JavaScript. In IEEE Symposium on Security and Privacy, pages 513–528. IEEE Computer Society, 2010.

Digital Library

[39]

P. Saxena, S. Hanna, P. Poosankam, and D. Song. FLAX: Systematic discovery of client-side validation vulnerabilities in rich web applications. In NDSS. The Internet Society, 2010.

[40]

K. U. Schulz. Makanin’s algorithm for word equations - two improvements and a generalization. In IWWERT, pages 85– 150, 1990.

Digital Library

[41]

Z. Su and G. Wassermann. The essence of command injection attacks in web applications. SIGPLAN Not., 41(1):372–382, Jan. 2006.

Digital Library

[42]

M. Trinh, D. Chu, and J. Jaffar. Progressive reasoning over recursively-defined strings. In CAV’16, volume 9779 of LNCS, pages 218–240. Springer, 2016.

[43]

M.-T. Trinh, D.-H. Chu, and J. Jaffar. S3: A symbolic string solver for vulnerability detection in web applications. In CCS’14, pages 1232–1243. ACM, 2014.

Digital Library

[44]

J. van Leeuwen. A generalisation of parikhs theorem in formal language theory. In ICALP, volume 14 of LNCS, pages 17–26, 1974.

Digital Library

[45]

J. van Leeuwen. Effective constructions in well-partiallyordered free monoids. Discrete Mathematics, 21(3):237 – 252, 1978.

Digital Library

[46]

H. Wang, T. Tsai, C. Lin, F. Yu, and J. R. Jiang. String analysis via automata manipulation with logic circuit representation. In CAV’16, volume 9779 of LNCS, pages 241–260. Springer, 2016.

[47]

G. Wassermann and Z. Su. Sound and precise analysis of web applications for injection vulnerabilities. SIGPLAN Not., 42 (6):32–41, June 2007.

Digital Library

[48]

F. Yu, M. Alkhalaf, and T. Bultan. Stranger: An automatabased string analysis tool for PHP. In TACAS’10, volume 6015 of LNCS, pages 154–157. Springer, 2010.

Digital Library

[49]

Y. Zheng, X. Zhang, and V. Ganesh. Z3-str: a z3-based string solver for web application analysis. In ESEC/FSE’13, pages 114–124. ACM, 2013.

Digital Library

[50]

Y. Zheng, X. Zhang, and V. Ganesh. Z3-str: A Z3-based string solver for web application analysis. In ESEC/FSE’13, pages 114–124. ACM, 2013.

Digital Library

[51]

Y. Zheng, V. Ganesh, S. Subramanian, O. Tripp, J. Dolby, and X. Zhang. Effective search-space pruning for solvers of string equations, regular expressions and length constraints. In CAV’15, volume 9206 of LNCS, pages 235–254. Springer, 2015.

Cited By

Stjerna ARümmer P(2024)A Constraint Solving Approach to Parikh Images of Regular LanguagesProceedings of the ACM on Programming Languages10.1145/36498558:OOPSLA1(1235-1263)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649855
Hague MJeż ALin A(2024)Parikh’s Theorem Made SymbolicProceedings of the ACM on Programming Languages10.1145/36329078:POPL(1945-1977)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632907
Wu HChen YWu ZXia BZhan N(2024)A decision procedure for string constraints with string/integer conversion and flat regular constraintsActa Informatica10.1007/s00236-023-00446-461:1(23-52)Online publication date: 1-Mar-2024
https://dl.acm.org/doi/10.1007/s00236-023-00446-4
Show More Cited By

Index Terms

Flatten and conquer: a framework for efficient analysis of string constraints
1. Security and privacy
  1. Formal methods and theory of security
    1. Logic and verification
2. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Flatten and conquer: a framework for efficient analysis of string constraints
PLDI '17

We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated ...
Abstract Regular Tree Model Checking

Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word ...
Compositional reachability analysis for efficient modular verification of asynchronous designs

Compositional verification is essential to address state explosion in model checking. Traditionally, an over-approximate context is needed for each individual component in a system for sound verification. This may cause state explosion for the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2017

708 pages

ISBN:9781450349888

DOI:10.1145/3062341

General Chair:
Albert Cohen
Inria, France
,
Program Chair:
Martin Vechev
DeepCode, Switzerland / ETH Zurich, Switzerland

ACM SIGPLAN Notices Volume 52, Issue 6
PLDI '17
June 2017
708 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3140587
Editor:
Matthew Fluet
Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 June 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '17

Sponsor:

SIGPLAN

PLDI '17: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 18 - 23, 2017

Barcelona, Spain

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

45
Total Citations
View Citations
470
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)5

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Stjerna ARümmer P(2024)A Constraint Solving Approach to Parikh Images of Regular LanguagesProceedings of the ACM on Programming Languages10.1145/36498558:OOPSLA1(1235-1263)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649855
Hague MJeż ALin A(2024)Parikh’s Theorem Made SymbolicProceedings of the ACM on Programming Languages10.1145/36329078:POPL(1945-1977)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632907
Wu HChen YWu ZXia BZhan N(2024)A decision procedure for string constraints with string/integer conversion and flat regular constraintsActa Informatica10.1007/s00236-023-00446-461:1(23-52)Online publication date: 1-Mar-2024
https://dl.acm.org/doi/10.1007/s00236-023-00446-4
Chen YChocholatý DHavlena VHolík LLengál OSíč J(2023)Solving String Constraints with Lengths by StabilizationProceedings of the ACM on Programming Languages10.1145/36228727:OOPSLA2(2112-2141)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622872
Chen YHavlena VLengál OTurrini A(2023)A symbolic algorithm for the case-split rule in solving word constraints with extensionsJournal of Systems and Software10.1016/j.jss.2023.111673201:COnline publication date: 1-Jul-2023
https://dl.acm.org/doi/10.1016/j.jss.2023.111673
Blahoudek FChen YChocholatý DHavlena VHolík LLengál OSíč J(2023)Word Equations in Synergy with Regular ConstraintsFormal Methods10.1007/978-3-031-27481-7_23(403-423)Online publication date: 3-Mar-2023
https://doi.org/10.1007/978-3-031-27481-7_23
Chen TFlores-Lamas AHague MHan ZHu DKan SLin ARümmer PWu Z(2022)Solving string constraints with Regex-dependent functions through transducers with priorities and variablesProceedings of the ACM on Programming Languages10.1145/34987076:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498707
Kammar OKatsumata SSaville P(2022)Fully abstract models for effectful λ-calculi via category-theoretic logical relationsProceedings of the ACM on Programming Languages10.1145/34987056:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498705
Müller MMakarchuk GSingh GPüschel MVechev M(2022)PRIMA: general and precise neural network certification via scalable convex hull approximationsProceedings of the ACM on Programming Languages10.1145/34987046:POPL(1-33)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498704
Yuan CMcNally CCarbin M(2022)Twist: sound reasoning for purity and entanglement in Quantum programsProceedings of the ACM on Programming Languages10.1145/34986916:POPL(1-32)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498691
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents