Projects per year
Abstract
The theory of strings with concatenation has been widely argued as the basis of constraint solving for verifying stringmanipulating programs. However, this theory is far from adequate for expressing many string constraints that are also needed in practice; for example, the use of regular constraints (pattern matching against a regular expression), and the stringreplace function (replacing either the first occurrence or all occurrences of a ``pattern'' string constant/variable/regular expression by a ``replacement'' string constant/variable), among many others. Both regular constraints and the stringreplace function are crucial for such applications as analysis of JavaScript (or more generally HTML5 applications) against crosssite scripting (XSS) vulnerabilities, which motivates us to consider a richer class of string constraints. The importance of the stringreplace function (especially the replaceall facility) is increasingly recognised, which can be witnessed by the incorporation of the function in the input languages of several string constraint solvers.
Recently, it was shown that any theory of strings containing the stringreplace function (even the most restricted version where pattern/replacement strings are both constant strings) becomes undecidable if we do not impose some kind of straightline (aka acyclicity) restriction on the formulas. Despite this, the straightline restriction is still practically sensible since this condition is typically met by string constraints that are generated by symbolic execution. In this paper, we provide the first systematic study of straightline string constraints with the stringreplace function and the regular constraints as the basic operations. We show that a large class of such constraints (i.e. when only a constant string or a regular expression is permitted in the pattern) is decidable. We note that the stringreplace function, even under this restriction, is sufficiently powerful for expressing the concatenation operator and much more (e.g. extensions of regular expressions with string variables). This gives us the most expressive decidable logic containing concatenation, replace, and regular constraints under the same umbrella. Our decision procedure for the straightline fragment follows an automatatheoretic approach, and is modular in the sense that the stringreplace terms are removed one by one to generate more and more regular constraints, which can then be discharged by the stateoftheart string constraint solvers. We also show that this fragment is, in a way, a maximal decidable subclass of the straightline fragment with stringreplace and regular constraints. To this end, we show undecidability results for the following two extensions: (1) variables are permitted in the pattern parameter of the replace function, (2) length constraints are permitted.
Recently, it was shown that any theory of strings containing the stringreplace function (even the most restricted version where pattern/replacement strings are both constant strings) becomes undecidable if we do not impose some kind of straightline (aka acyclicity) restriction on the formulas. Despite this, the straightline restriction is still practically sensible since this condition is typically met by string constraints that are generated by symbolic execution. In this paper, we provide the first systematic study of straightline string constraints with the stringreplace function and the regular constraints as the basic operations. We show that a large class of such constraints (i.e. when only a constant string or a regular expression is permitted in the pattern) is decidable. We note that the stringreplace function, even under this restriction, is sufficiently powerful for expressing the concatenation operator and much more (e.g. extensions of regular expressions with string variables). This gives us the most expressive decidable logic containing concatenation, replace, and regular constraints under the same umbrella. Our decision procedure for the straightline fragment follows an automatatheoretic approach, and is modular in the sense that the stringreplace terms are removed one by one to generate more and more regular constraints, which can then be discharged by the stateoftheart string constraint solvers. We also show that this fragment is, in a way, a maximal decidable subclass of the straightline fragment with stringreplace and regular constraints. To this end, we show undecidability results for the following two extensions: (1) variables are permitted in the pattern parameter of the replace function, (2) length constraints are permitted.
Original language  English 

Title of host publication  Proceedings of the ACM on Programming Languages 
Publisher  ACM 
Pages  129 
Number of pages  29 
Volume  2 
DOIs  
Publication status  Epub ahead of print  27 Dec 2017 
Event  Principles of Programming Languages  Los Angeles, United States Duration: 10 Jan 2018 → 12 Jan 2018 
Conference
Conference  Principles of Programming Languages 

Abbreviated title  POPL 
Country/Territory  United States 
City  Los Angeles 
Period  10/01/18 → 12/01/18 
Keywords
 String Constraints, ReplaceAll, Decision Procedures, Constraint Solving, StraightLine Programs
Projects
 1 Finished

Verification of Concurrent and HigherOrder Recursive Programs
Hague, M. (PI)
Eng & Phys Sci Res Council EPSRC
1/05/13 → 30/04/18
Project: Research