Abstract
In this chapter, we discuss using automata as a symbolic representation for string analysis. To compute forward and backward reachability for string manipulating programs, we can use automata-based symbolic string analysis where automata are used as a symbolic representation to represents sets of states of the program. We can iteratively compute an approximation of the least fixpoint that corresponds to the reachable values of the string expressions. Assume that we use one Deterministic Finite Automaton (DFA) per string variable, per program point. I.e., each DFA represents the set of values that a string variable can take at a particular program point. In each iteration, given the current state DFA for a variable, we can compute the pre- and post-state DFA. In order to implement this approach we have to develop automata based algorithms for computing pre- and post-state computation for common string operations such as concatenation, and replacement as we discuss later in this chapter.
This is a preview of subscription content, log in via an institution to check access.
References
Masahiro Fujita, Patrick C. McGeer, and Jerry Chih-Yuan Yang. Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. Formal Methods in System Design, 10(2/3):149–169, 1997.
Yuto Sakuma, Yasuhiko Minamide, and Andrei Voronkov. Translating regular expression matching into transducers. J. Applied Logic, 10(1):32–51, 2012.
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, pages 241–260, 2016.
Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Generating vulnerability signatures for string manipulating programs using automata-based forward and backward symbolic analyses. In ASE, 2009.
Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Stranger: An automata-based string analysis tool for php. In TACAS, 2010.
Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Patching vulnerabilities with sanitization synthesis. In Proceedings of the 33rd International Conference on Software Engineering (ICSE), pages 251–260, 2011.
Fang Yu, Muath Alkhalaf, Tevfik Bultan, and Oscar H. Ibarra. Automata-based symbolic string analysis for vulnerability detection. Formal Methods in System Design, 44(1):44–70, 2014.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Bultan, T., Yu, F., Alkhalaf, M., Aydin, A. (2017). Automata Based String Analysis. In: String Analysis for Software Verification and Security. Springer, Cham. https://doi.org/10.1007/978-3-319-68670-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-68670-7_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68668-4
Online ISBN: 978-3-319-68670-7
eBook Packages: Computer ScienceComputer Science (R0)