Document Open Access Logo

On the Separability Problem of String Constraints

Authors Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, Shankara Narayanan Krishna

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.16.pdf
  • Filesize: 1.74 MB
  • 19 pages

Document Identifiers

Author Details

Parosh Aziz Abdulla
  • Uppsala University, Sweden
Mohamed Faouzi Atig
  • Uppsala University, Sweden
Vrunda Dave
  • IIT Bombay, India
Shankara Narayanan Krishna
  • IIT Bombay, India

Cite As Get BibTex

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna. On the Separability Problem of String Constraints. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.16

Abstract

We address the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation for string constraints. We first show that regular separability of straight line string constraints is undecidable. Our second result is the decidability of the separability problem for straight-line string constraints by piece-wise testable languages, though the precise complexity is open. In our third result, we consider the positive fragment of piece-wise testable languages as a separator, and obtain an ExpSpace algorithm for the separability of a useful class of straight-line string constraints, and a Pspace-hardness result.

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
  • Theory of computation → Verification by model checking
Keywords
  • string constraints
  • separability
  • interpolants

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, and Philipp Rümmer. Flatten and conquer: a framework for efficient analysis of string constraints. In PLDI. ACM, 2017. Google Scholar
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, and Philipp Rümmer. Trau: SMT solver for string constraints. In FMCAD. IEEE, 2018. Google Scholar
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. String constraints for verification. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 150-166. Springer, 2014. Google Scholar
  4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna. On the separability problem of string constraints. CoRR, abs/2005.09489, 2020. URL: http://arxiv.org/abs/2005.09489.
  5. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep, Lukás Holík, and Petr Janku. Chain-free string constraints. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 277-293. Springer, 2019. Google Scholar
  6. Parosh Aziz Abdulla and Richard Mayr. Priced timed petri nets. Logical Methods in Computer Science, 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:10)2013.
  7. Mohamed Faouzi Atig, Benedikt Bollig, and Peter Habermehl. Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete. Int. J. Found. Comput. Sci., 28(8):945-976, 2017. Google Scholar
  8. Félix Baschenis, Olivier Gauwin, Anca Muscholl, and Gabriele Puppis. Minimizing resources of sweeping and streaming string transducers. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 114:1-114:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  9. Murphy Berzish, Vijay Ganesh, and Yunhui Zheng. Z3str3: A string solver with theory-aware heuristics. In 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017, pages 55-59. IEEE, 2017. Google Scholar
  10. Murphy Berzish, Yunhui Zheng, and Vijay Ganesh. Z3str3: A string solver with theory-aware branching. CoRR, abs/1704.07935, 2017. URL: http://arxiv.org/abs/1704.07935.
  11. Luca Breveglieri, Alessandra Cherubini, Claudio Citrini, and Stefano Crespi-Reghizzi. Multi-push-down languages and grammars. Int. J. Found. Comput. Sci., 7(3):253-292, 1996. URL: https://doi.org/10.1142/S0129054196000191.
  12. Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu. What is decidable about string constraints with the replaceall function. PACMPL, 2(POPL):3:1-3:29, 2018. URL: https://doi.org/10.1145/3158091.
  13. Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290362.
  14. Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Decision procedures for path feasibility of string-manipulating programs with complex operations. PACMPL, 3(POPL):49:1-49:30, 2019. Google Scholar
  15. Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Regular separability of parikh automata. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 117:1-117:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  16. Wojciech Czerwinski and Slawomir Lasota. Regular separability of one counter automata. Logical Methods in Computer Science, 15(2), 2019. URL: https://lmcs.episciences.org/5563, URL: https://doi.org/10.23638/LMCS-15(2:20)2019.
  17. Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular separability of well-structured transition systems. In 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 35:1-35:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  18. Wojciech Czerwinski, Wim Martens, and Tomás Masopust. Efficient separability of regular languages by subsequences and suffixes. In Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 150-161. Springer, 2013. Google Scholar
  19. Wojciech Czerwinski, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, and Georg Zetzsche. A characterization for decidable separability by piecewise testable languages. Discrete Mathematics & Theoretical Computer Science, 19(4), 2017. Google Scholar
  20. Vijay Ganesh and Murphy Berzish. Undecidability of a theory of strings, linear arithmetic over length, and string-number conversion. CoRR, abs/1605.09442, 2016. URL: http://arxiv.org/abs/1605.09442.
  21. Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin C. Rinard. Word equations with length constraints: What’s decidable? In Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers, volume 7857 of Lecture Notes in Computer Science, pages 209-226. Springer, 2012. Google Scholar
  22. Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin C. Rinard. (Un)Decidability results for word equations with length and regular expression constraints. CoRR, abs/1306.6054, 2013. URL: http://arxiv.org/abs/1306.6054.
  23. Seymour Ginsburg and Sheila A. Greibach. Abstract families of languages. In 8th Annual Symposium on Switching and Automata Theory, Austin, Texas, USA, October 18-20, 1967. IEEE Computer Society, 1967. Google Scholar
  24. G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3), 2(7), 1952. Google Scholar
  25. Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, and Tomás Vojnar. String constraints with concatenation and transducers solved efficiently. PACMPL, 2(POPL):4:1-4:32, 2018. URL: https://doi.org/10.1145/3158092.
  26. Scott Kausler and Elena Sherman. Evaluation of string constraint solvers in the context of symbolic execution. In ASE '14. ACM, 2014. Google Scholar
  27. Adam Kiezun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. HAMPI: a solver for string constraints. In Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, ISSTA 2009, Chicago, IL, USA, July 19-23, 2009, pages 105-116. ACM, 2009. Google Scholar
  28. Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters. A DPLL(T) theory solver for a theory of strings and regular expressions. In CAV'14, volume 8559 of LNCS. Springer, 2014. Google Scholar
  29. Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark W. Barrett, and Morgan Deters. An efficient SMT solver for string constraints. Formal Methods in System Design, 48(3):206-234, 2016. URL: https://doi.org/10.1007/s10703-016-0247-6.
  30. Anthony Widjaja Lin and Pablo Barceló. String solving with word equations and transducers: towards a logic for analysing mutation XSS. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 123-136. ACM, 2016. Google Scholar
  31. MakePHPSites. Php tutorials. https://makephpsites.com/php-tutorials/user-management-tools/changing-passwords.php, 2015.
  32. Kenneth L. McMillan. Interpolation and SAT-based model checking. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, volume 2725 of Lecture Notes in Computer Science, pages 1-13. Springer, 2003. Google Scholar
  33. Kenneth L. McMillan. An interpolating theorem prover. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, volume 2988 of Lecture Notes in Computer Science, pages 16-30. Springer, 2004. Google Scholar
  34. Kenneth L. McMillan. Lazy abstraction with interpolants. In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 123-136. Springer, 2006. Google Scholar
  35. Christophe Morvan. On rational graphs. In Foundations of Software Science and Computation Structures, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. Google Scholar
  36. Thomas Place, Lorijn van Rooijen, and Marc Zeitoun. Separating regular languages by piecewise testable and unambiguous languages. In Mathematical Foundations of Computer Science 2013 - 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings, volume 8087 of Lecture Notes in Computer Science, pages 729-740. Springer, 2013. Google Scholar
  37. Wojciech Plandowski. An efficient algorithm for solving word equations. In Proceedings of the Thirty-eighth Annual ACM Symposium on Theory of Computing, STOC '06, pages 467-476, New York, NY, USA, 2006. ACM. URL: https://doi.org/10.1145/1132516.1132584.
  38. Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, and Cesare Tinelli. Scaling up DPLL(T) string solvers using context-dependent simplification. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 453-474. Springer, 2017. Google Scholar
  39. Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. A symbolic execution framework for javascript. In 31st IEEE Symposium on Security and Privacy, S&P 2010, 16-19 May 2010, Berleley/Oakland, California, USA, pages 513-528. IEEE Computer Society, 2010. Google Scholar
  40. Prateek Saxena, Steve Hanna, Pongsin Poosankam, and Dawn Song. FLAX: systematic discovery of client-side validation vulnerabilities in rich web applications. In Proceedings of the Network and Distributed System Security Symposium, NDSS 2010, San Diego, California, USA, 28th February - 3rd March 2010. The Internet Society, 2010. Google Scholar
  41. Imre Simon. Piecewise testable events. In Automata Theory and Formal Languages, 2nd GI Conference, Kaiserslautern, May 20-23, 1975, volume 33 of Lecture Notes in Computer Science, pages 214-222. Springer, 1975. Google Scholar
  42. Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. S3: A symbolic string solver for vulnerability detection in web applications. In CCS'14. ACM, 2014. Google Scholar
  43. Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. Progressive reasoning over recursively-defined strings. In CAV'16, volume 9779 of LNCS. Springer, 2016. Google Scholar
  44. Moshe Y. Vardi. A note on the reduction of two-way automata to one-way automata. Inf. Process. Lett., 30(5):261-264, 1989. URL: https://doi.org/10.1016/0020-0190(89)90205-6.
  45. Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, and Jie-Hong R. Jiang. String analysis via automata manipulation with logic circuit representation. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 241-260. Springer, 2016. Google Scholar
  46. Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Stranger: An automata-based string analysis tool for PHP. In Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 154-157. Springer, 2010. Google Scholar
  47. Yunhui Zheng, Xiangyu Zhang, and Vijay Ganesh. Z3-str: A Z3-based string solver for web application analysis. In ESEC/FSE'13. ACM, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact