String Solving with Word Equations and Transducers:
Towards a Logic for Analysing Mutation XSS (Full Version)
Anthony W. Lin

Pablo Barceló

Yale-NUS College, Singapore
anthony.w.lin@yale-nus.edu.sg

Center for Semantic Web Research& Dept. of Comp. Science, Univ. of Chile, Chilepbarcelo@dcc.uchile.cl

Abstract
We study the fundamental issue of decidability of satisfiability
over string logics with concatenations and finite-state transducers
as atomic operations. Although restricting to one type of operations yields decidability, little is known about the decidability of
their combined theory, which is especially relevant when analysing
security vulnerabilities of dynamic web pages in a more realistic browser model. On the one hand, word equations (string logic
with concatenations) cannot precisely capture sanitisation functions (e.g. htmlescape) and implicit browser transductions (e.g. innerHTML mutations). On the other hand, transducers suffer fromthe reverse problem of being able to model sanitisation functions
and browser transductions, but not string concatenations. Naively
combining word equations and transducers easily leads to an undecidable logic. Our main contribution is to show that the “straightline fragment” of the logic is decidable (complexity ranges fromPSPACE to EXPSPACE). The fragment can express the programlogics of straight-line string-manipulating programs with concatenations and transductions as atomic operations, which arise when
performing bounded model checking or dynamic symbolic executions. We demonstrate that the logic can naturally express constraints required for analysing mutation XSS in web applications.
Finally, the logic remains decidable in the presence of length, lettercounting, regular, indexOf, and disequality constraints.
Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about
Programs—Logics of Programs
Keywords String analysis, XSS, word equations, transducers

1.

Introduction

The past decade has witnessed a significant amount of progress inconstraint solving technologies, thanks to the emergence of highly
efficient SAT-solvers (e.g. see [15, 43, 46]) and SMT-solvers (e.g.
see [11, 25, 43]). The goal of SAT-solvers is to solve constraint
satisfaction problem in its most basic form, i.e., satisfiability of
propositional formulas. Nowadays there are numerous highly efficient solvers including Chaff, Glucose, Lingeling, and MiniSAT,

to name a few (e.g. see [3] for others). Certain applications, however, require more expressive constraint languages. The frameworkof satisfiability modulo theories (SMT) builds on top of the basic
constraint satisfaction problem by interpreting atomic propositions
as a quantifier-free formula in a certain “background” logical theory, e.g., linear arithmetic. Today fast SMT-solvers supporting a
multitude of background theories are available including Boolector,
CVC4, Yices, and Z3, to name a few (e.g. see [4] for others). The
backbones of fast SMT-solvers are usually a highly efficient SATsolver (to handle disjunctions) and an effective method of dealing
with satisfiability of formulas in the background theory.
In the past seven years or so there have been a lot of works
on developing robust SMT-solvers for constraint languages overstrings (a.k.a. string solvers). The following (incomplete) list of
publications indicates the amount of interests in string solving(broadly construed): [7, 8, 16, 22, 24, 29–32, 35, 36, 39, 44, 48,
53, 55, 57, 65–69, 71–76]. One main driving force behind this research direction — as argued by the authors of [8, 24, 30, 36, 39,
39, 48, 48, 57, 65–69, 75, 76] among others — is the application
to analysis of security vulnerabilities in web applications against
code injections and cross-site scripting (XSS), which are typicallycaused by improper handling of untrusted strings by the web applications, e.g., leading to an execution of malicious JavaScript in theclients’ browsers.
Despite the amount of recent progress in developing practicalstring solvers, little progress has been made on the foundational issues of string solving including decidability, which is particularly
important since it imposes a fundamental limit of what we can expect from a solver for a given string constraint language (especiallywith respect to soundness and completeness). Perhaps the most important theoretical result in string solving is the decidability of satisfiability for word equations (i.e. string logic with the concatenation operator) by Makanin [45] (whose computational complexity
was improved to PSPACE by Plandowski [51, 52]). It is known
that adding regular constraints (i.e. regular-expression matching)preserves decidability without increasing the complexity [26, 52].
Very few decidability results extending this logic are known.
For such an application as detecting security vulnerabilities in
web applications in a realistic browser model (e.g. see [70]), word
equations with regular constraints alone are insufficient. Firstly,browsers regularly perform implicit transductions. For example,
upon innerHTML assignments or document.write invocations,browsers mutate the original string values by HTML entity decoding, e.g., each occurrence of &#34; will be replaced by ". [Modern browsers admit some exceptions including the HTML entity
names &amp;, &lt;, and &gt; (among others), which will not
be decoded.] Since such transductions involve only conversionsof one character-set encoding to another, they can be encoded as
finite-state (input/output) transducers, as has already been noted in[24, 36, 66, 70] (among others). Secondly, in an attempt to prevent code injection and XSS attacks, most web applications will
first sanitise untrusted strings (e.g. obtained from an untrusted application) before processing them. Common sanitisation functions
include JavaScript-Escape and HTML-Escape (an implementation
can be found in The Closure Library [5]). HTML-Escape converts
reserved characters in HTML such as &, <, and ' to their respective HTML entity names &amp;, &lt; and &#39;. On the other
hand, JavaScript-Escape will backslash-escape certain metacharacters, e.g., the character ' and " are replaced by \' and \". Again,such sanitisation functions can be encoded as finite-state transducers, as has been noted in [36] (among others).
Example 1. The following JavaScript code snippet adapted froma recent CACM article [38] is a simple example that uses bothconcatenations and finite-state transducers (both explicitly and implictly):
var x = goog.string.htmlEscape(cat);var y = goog.string.escapeString(x);catElem.innerHTML = '<button onclick="createCatList(\'' + y + '\')">' + x + '</button>';The code assigns an HTML markup for a hyperlink to the DOM element catElem. The hyperlink creates a category cat whose value
is provided by an untrusted third party. For this reason, the code
attempts to first sanitise the value of cat. This is done via The Closure Library [5] string functions htmlEscape and escapeString(implementing JavaScript-Escape). Inputting the value Flora &Fauna into cat gives the desired HTML markup:<button onclick="createCatList('Flora &amp; Fauna')">Flora &amp; Fauna</button>

On the other hand, inputting the value ');alert(1);// to cat,results in the HTML markup:<button onclick="createCatList('&#39;);alert(1);//')">&#39;);alert(1);//')</button>

When this is inserted into the DOM via innerHTML, an implicit
browser transduction will take place, i.e., first HTML-unescaping
the value inside the onclick attribute and invoking the attacker’s
script alert(1) after createCatList. This subtle XSS bug (atype of mutation XSS [33]) is due to calling the appropriate escaping functions in the wrong order.
It is well-known (e.g. see [8, 57, 75]) that string solving canbe applied to detecting security vulnerabilities against a given injection and XSS attack pattern1 P in the form of a regular expression. After identifying certain “hot spot” variables in the program where attacks can be performed (e.g. possibly via taint analysis), a string constraint will be generated that is satisfiable iff
the program is vulnerable against a given attack pattern. In theabove example, to analyse security vulnerabilities in the variable
catElem.innerHTML against the following attack pattern (given
in JavaScript regex notation; blank space inserted for readability):
e1 = /<button onclick="createCatList\(' ( ' | [^']*[^'\\] ' ) \);[^']*[^'\\]' )">.*<\/button>/

one would express the program logic as a conjunction of:• x = R1 (cat)• y = R2 (x)• z = w1 · y · w2 · x · w3 for some constant strings w1 , w2 , w3 ,e.g., w1 is <button onclick="createCatList('• catElem.innerHTML = R3 (z)• catElem.innerHTML matches e1.

Here, R1 and R2 are, respectively, transducers implementing
htmlEscape and escapeString, while R3 is a transducer implementing the implicit browser transductions upon innerHTML
assignments. Note that the above string constraint cannot be written as word equations with regular constraints alone since thefinite-state transducers replace each occurrence of a substring (e.g.
&#39;) in a string by another string (e.g. the single character "). To
the best of our knowledge, there is no known decidable logic which
can express the above string constraint.
Contribution: We study the decidability of satisfiability overstring logics with concatenations, finite-state transductions, andregex matching as atomic operations. Naively combining concatenations and transducers easily leads to an undecidable logic (e.g.
see [10, 16]). In fact, it was shown in [10] that restricting to string
constraints of the form x = y · z ∧ x = R(z), where R ranges
over finite-state transducers, is undecidable. [Actually, R can be
restricted to a relatively weak class of finite-state transducers that
express only regular relations (a.k.a. automatic relations [18]).]
Our main contribution is to show that the “straight-line fragment”
of the logic is decidable (in fact, is EXPSPACE-complete, but
under a certain reasonable assumption the complexity reduces to
PSPACE). In fact, our decidability results provide an upper boundfor the maximum size of solutions that need to be explored toguarantee completeness for bounded-length string solvers whenever the input constraint falls within our straight-line fragment. The
fragment can express the program logics of straight-line stringmanipulating programs with concatenations and transductions as
atomic operations. This includes the program logic of Example
1. In fact, straight-line programs naturally arise when performing
bounded model checking2 or dynamic symbolic executions, which
unrolls loops in the programs (up to a given depth) and converts
the resulting programs into static single assignment form (i.e. eachvariable defined once). Please consult [27, 43, 65] for more details.
Example 1 is one example of analysis of mutation XSS vulnerabilities that can be expressed in our logic. In this paper, we provide
three other mutation XSS examples that can be expressed in our
logic (adapted from [33, 38, 62]).
Finally, the case study of [57] suggested that the use of length
constraints (comparing lengths of different strings) and IndexOf
constraints (IndexOf(x, y) outputs the position of an occurrenceof a given string x in another string y) is prevalent in JavaScript
programs. To this end, we show that our logic is still decidable(with the same complexity) when extended with:
1. (linear) arithmetic constraints whose free variables are interpreted as one of the following: integer variables in the program,length of a string variable, or the number of occurrences of acertain letter in a string variable.
2. IndexOf constraints of the form h = IndexOf(w, y), where w
is a constant string and h is an integer variable. This is the mostfrequent usage of IndexOf operator in JavaScript.
All the examples in the benchmark examples of [57] were observed
to belong to a class called solved forms [31], which is a subset
of our string logic with linear arithmetic constraints. Lastly, we
can also add unrestricted disequality constraints between string
variables, while still preserving decidability.
Organisation: Section 2 fixes general mathematical notations
and reviews the necessary concepts on automata and transducers
that will be used throughout the paper. In Section 3, we define a

1 Attack patterns are identified from previous vulnerabilities, some of whichhave been well-documented, e.g., see [2, 6].

2 Note that this does not mean restrictions to strings of bounded length.

general string constraint language that combines concatenations,finite-state transductions, and regex matching. The language is undecidable even after imposing various restrictions that have been
proposed in the literature. In Section 4, we recover decidability forthe straight-line fragment. In Section 5, we show that decidability can be retained even when length and IndexOf constraints areincorporated. We conclude with the related work and possible future works in Section 6. Additional material can be found in the
appendix.

2.

Preliminaries

General notations: Given two integers i, j, we write [i, j] todenote the set {i, . . . , j} of integers in between i and j. For each
integer k, we write [k] to denote [0, k]. Given a binary relation
R ⊆ S × S and a set A ⊆ S, we use R(A) to denote the set{s′ ∈ S | (s, s′ ) ∈ R for some s ∈ A}. In other words, R(A) isthe post-image of A under R. We use R−1 to denote the reverse
relation, i.e., (s, s′ ) ∈ R−1 iff (s′ , s) ∈ R for each s, s′ ∈ S.
Notice then that R−1 (A) is the pre-image of A under R. The term
DAG stands for directed acylic graphs.
Regular languages: Fix a finite alphabet Σ. Elements in Σ∗
are interchangeably called words or strings. For each finite word
w = w1 . . . wn ∈ Σ∗ , we write w[i, j], where 1 ≤ i ≤ j ≤ n, todenote the segment wi . . . wj . We use w[i] to denote w[i, i] = wi .
In addition, the symbol |w| denotes the length n of w, while thesymbol |w|a (a ∈ Σ) denotes the number of occurrences of a in w.
Recall that a nondeterministic finite-state automaton (NFA) is
a tuple A = (Σ, Q, δ, q0 , F ), where Q is a finite set of states,δ ⊆ Q × Σ × Q is the transition relation, q0 ∈ Q is the initial state,and F ⊆ Q is the set of final states. A run of A on w is a function
ρ : {0, . . . , n} → Q with ρ(0) = q0 that obeys the transition
relation δ, i.e., (ρ(i), wi , ρ(i+1)) ∈ δ for each i ∈ {0, . . . , n−1}.
We write A[q,q′ ] to denote A but the initial state (resp. set of final
states) is replaced by q (resp. {q ′ }). We may also denote the run ρby the word ρ(0) · · · ρ(n) over the alphabet Q. The run ρ is said
to be accepting if ρ(n) ∈ F , in which case we say that the word
w is accepted by A. The language L(A) of A is the set of wordsin Σ∗ accepted by A. Such a language is said to be regular. Recall
that regular languages are precisely the ones that can be definedby regular expressions. In the sequel, when the meaning is clear
from the context, we will sometimes confuse an NFA or a regularexpression with the regular language that it recognises/generates.
Transducers and rational relations: A transducer (short for“finite-state input output transducer”) is a two-tape automaton thathas two heads for the tapes and one additional finite control; at every step, based on the state and the letters it is reading, the automaton can enter a new state and move some (but not necessarily all)tape heads. Each transducer generates a binary relation over strings
called rational relation.
We will now make this definition more precise. A transducer
over the alphabet Σ is a tuple A = (Γ, Q, δ, q0 , F ), where Γ := Σ2ϵand Σϵ := Σ ∪ {ϵ}, such that A is syntactically an NFA over Γ.
The transducer A is said to be synchronised if A (viewed as anNFA) does not accept words w = (a1 , b1 ) · · · (an , bn ) ∈ (Σ2ϵ )∗such that there exist i, j ∈ [n] with i < j such that one of thefollowing conditions holds: (1) (ai , bi ) ∈ Σ × {ϵ} and bj ∈ Σ,(2) (ai , bi ) ∈ {ϵ} × Σ and aj ∈ Σ. Intuitively, as soon as thetwo heads go out of sync, the head that is lagging behind is nolonger allowed to move forward. The relation R ⊆ (Σ∗ )2 that A
recognises consists of all tuples w̄ for which there is a run
σ

σ

σ

1
2
n
π := q0 −→q1 −→· · · −→
qn

of A (treated as an NFA) such that w̄ = σ1 ◦ σ2 ◦ · · · ◦ σn , where
the string concatenation operator ◦ is extended to tuples over words

component-wise (i.e. (v1 , v2 )◦(w1 , w2 ) = (v1 w1 , v2 w2 )). A relation is said to be rational if it is recognised by a transducer. A relation is said to be synchronised rational (a.k.a. regular or automatic;see [10, 16, 17]) if it is recognised by a synchronised transducer.
Rational relations satisfy some nice properties (e.g. see [14, 54]):(1) closure under union and concatenation, and (2) the pre/post image of a regular language under a rational relation is regular. The
transducers/automata witnessing the above two properties can also
be constructed efficiently: taking union can be done in linear-time,
while taking concatenation and pre/post image of a regular language can be done in quadratic time (e.g. see [12–14]). Synchronised rational relations are adequate for certain applications (e.g.
see [9, 17, 64, 74]), while also satisfying effective closure underintersection and complementation (cf. [17]).
Example 2. The operator replace-all replaces all occurrencesof subwords matched by a regular expression e by a word in a
regular expression e′ , which in a Vim-like notation can be written
as s/e/e′ /g. There are various matching strategies that are usedby real-world programming languages, e.g., first match, longest
match, etc. They can all be encoded as transducers (e.g. see [55]).
One particular use of replace-all is to replace words that matcha regular language L by ϵ (i.e. an erase operation). Such usage of
replace-all can be found in sanitisation of PHP scripts, e.g., see[8, 29, 30, 73, 75]. For example, to thwart XSS attack patterns of theform <script>Σ∗ </script> from a string variable x, one could
erase each occurrence of < from x (e.g. see [8, 73, 75]).
Let y = replace-all(x, ϵ/A) denote the operation of erasing
each occurrence of letters a ∈ A (e.g. A = {<}) from x and assign
it to y. The transducer T for this is simple. It has one state q, which
is both an initial and final state. It has |A| transitions, i.e., for eacha ∈ A the transducer T has the transition (q, (a, ϵ), q).
Computational complexity: In this paper, we study not only decidability but also the complexity of string logics. Pinpointing the
precise complexity of verification problems is not only of fundamental importance, but also it often suggests algorithmic techniques that are most suitable for attacking the problem in practice. In this paper, we deal with the following computational complexity classes (see [61] for more details): P (problems solvablein polynomial-time), PSPACE (problems solvable in polynomial
space and exponential time), and EXPSPACE (problems solvablein exponential space and double exponential time). Verification
problems that have complexity PSPACE or beyond — see [40, 60]
for a few examples — have substantially benefited from techniques
like symbolic model checking [47]. As we shall see later, our complexity upper bound also suggests the maximum lengths of words
that need to be explored to guarantee completeness.

3. The Core Constraint Language
We start by defining a general string constraint language that supports concatenations, finite-state transducers, and regex matching.
The language is a natural generalisation of three decidable string
constraint languages: word equations, finite-state transducers, andregex matching. The generality of the language, however, quickly
makes it undecidable. To delineate the border of undecidability, we
shall show that the undecidability already holds for various restrictions that have been proposed in the literature (e.g. restricting finitestate transducers to replace-all). We will recover decidability inthe next section.
3.1 Language Definition
We assume a finite alphabet Σ and countably many string variables x, y, z, . . . ranging over Σ∗ . We start by defining relational
constraints.

Definition 1 (Relational constraints). An atomic relational constraint over Σ is an expression φ defined by the following grammar:
φ ::= y = x1 ◦ · · · ◦ xn (n ∈ N) | y = w | R(x, y)∗

where y, xi are string variables, w ∈ Σ is a constant word, and R
is a rational relation over Σ given as a transducer. Here, ◦ is used
to denote the string concatenation operator, which we shall often
omit (or simply replace by ·) to avoid notational clutter. A relational
constraint is a conjunction of atomic relational constraints.
In other words, an atomic relational constraint allows us totest equality of a string variable y with either a concatenation ofstring variables or a constant string, or whether the transducer R
can transform x into y. Notice that the atomic constraint y =x1 ◦ · · · ◦ xn cannot be defined as a rational relation R(x, y) (orin fact any binary relation) when n > 1. We now define regularconstraints (i.e. regex matching constraints), which check whether
a word belongs to a boolean combination of regular languages.
Definition 2 (Regular constraints). An atomic regular constraint
over Σ is an expression of the form P (x), for P a regular language
over Σ given as an NFA and x a variable. A regular constraint over
Σ is a boolean combination of atomic regular constraints over Σ
defined by the following grammar:
φ ::= P (x) | φ ∧ φ | φ ∨ φ | ¬φ
We finally define the class of string constraints by taking the
conjunction of relational and regular constraints.
Definition 3 (String constraints). A string constraint over finite
alphabet Σ is a conjunction of a relational constraint and a regularconstraint over Σ.
String constraints allow us to express general word equations(i.e., x1 . . . xn = y1 . . . yn for not necessarily distinct variables)by a conjunction of y = x1 . . . xn and y = y1 . . . yn . In addition,
when the word equation asserts that one of the xi ’s or yj ’s is theconstant string w ∈ Σ∗ , we simply add a regular constraint thatenforces the variable to belong to the language {w}.
An assignment for a string constraint φ over Σ is simply amapping ι from the set of string variables mentioned in φ to Σ∗ .
It satisfies φ if the constraint φ becomes true under the substitutionof each variable x by ι(x). We formalise this for atomic relationaland regular constraints (boolean connectives are standard):
1. ι satisfies the relational constraint y = x1 · · · xn , for string
variables y, x1 , . . . , xn , if and only if ι(y) = ι(x1 ) · · · ι(xn ).
2. ι satisfies the relational constraint y = w, for string variable y
and word w ∈ Σ∗ , if and only if ι(y) = w.
3. ι satisfies the relational constraint R(x, y), for a rational relation R, if and only if the pair (ι(x), ι(y)) belongs to R.

The generality of the constraint language makes it undecidable,
even in very simple cases.
Proposition 1. S ATISFIABILITY is undecidable.
This is because checking satisfiability of constraints of the form
R(x, x) is already undecidable by a simple reduction from the Post
Correspondence Problem (PCP), e.g., see [49, Proof of Proposition
2.14]. For this reason, an acyclicity constraint is often imposed(e.g. see [10, 12, 13]) to obtain decidability for formulas that are
conjunctions of constraints of the form P (x) or R(x, y), where P
is a regular language and R is a rational constraint. This condition isdefined as follows. Let φ be a formula of the form above and G(φ)
the undirected graph whose nodes are the variables in φ and there
is an edge {x, y} if R(x, y) is a constraint in φ. Further, let AC be
the class of those formulas φ such that G(φ) is acyclic. Then:
Proposition 2 ([10]). Checking satisfiability of formulas in AC is
PSPACE-complete. In fact, if a formula φ ∈ AC is satisfiable, thenit has a solution of size at most exponential in |φ|.
The authors of [10] refer to this problem as the generalised intersection problem with acyclic queries (see Theorem 6.7 in [10]).
[Decidability (in fact, in exponential time) of such a restriction already follows from the classic result by Nivat in the study of rational relations (e.g. see the textbook [14]) that the pre/post images ofregular languages under a rational transducer is effectively regularand the complexity analysis in [12, 13].]
Unfortunately, the positive result in Proposition 2 cannot be easily extended to our constraint language, as taking the conjunctionof a formula in AC (in particular, of a single rational constraint
R(x, y)) with the very simple word equation x = y turns the satisfiability problem undecidable. This is because the undecidable constraint R(x, x) can be expressed as: x = y ∧ R(x, y). Restricting
R to synchronised rational relations does not help either: satisfiability of string constraints of the form x = yz ∧ R(x, z), where R
is a synchronised rational relation, is undecidable [10].
Another option is to restrict the use of finite-state transducers to the replace-all operators. As we have argued in Example 2 this might be sufficient to model some sanitisation functions
that arise in practice. In fact, some string constraint languages thathave been proposed in the literature (e.g. see [65, 75]) permit theuse of the replace-all operator, but not finite-state transductions in general. It turns out that this restriction is still undecidable even for the very restricted use of replace-all of the form
replace-all(x, ϵ/A) (defined in Example 2) which erase all occurrences of characters a ∈ A in x. The proof (see Appendix) is
via a simple but tedious reduction from PCP.
Proposition 3. Checking satisfiability of a constraint of the form
x = yz ∧ φ, where φ is a formula in AC that only mentions transducers R(x, y) of the form replace-all(x, ϵ/A), is undecidable.

4. ι satisfies the atomic regular constraint P (x), for P a regular
language, if and only if ι(x) ∈ P .
A satisfying assignment for φ is also called a solution for φ. If
φ has a solution, then it is said to be satisfiable.
Example 3. In Introduction, we have expressed the program logicof the script in Example 1 and the attack pattern as a conjunction offour atomic relational constraints and one regular constraint.
3.2

The Satisfiability Problem

The definition of the problem is given as follows.
PROBLEM :INPUT :QUESTION :S ATISFIABILITY.
A string constraint φ over Σ.
Is φ satisfiable?

4.

The Straight-Line Fragment

In Section 3, we have explored various syntactic restrictions of
the core constraint language that still permit both concatenationand transducers, and saw that undecidability still held. In this section, we will show that the “straight-line fragment” of the language is decidable (in fact, solvable in exponential space). This
straight-line fragment captures the structure of straight-line manipulating programs with concatenations and finite-state transductions as atomic string operations. Note that straight-line programs
naturally arise when verifying string-manipulating programs using
bounded model checking and dynamic symbolic executions (e.g.
see [27, 43, 65]), which unrolls loops in the programs (up to a given
depth) and converts the resulting programs into static single assign-ment form (i.e. each variable defined only once). For applications
to detecting mutation XSS [33], we will see that the formula for
analysing mutation XSS from Example 1 in Introduction can be
expressed in the straight-line fragment. We will also see other such
examples in this section.
Convention. In the sequel, we will treat an atomic relational
constraint of the form y = w, for a word w ∈ Σ∗ , as an atomic
regular constraint, i.e., simply treat w as regular expression andassert y ∈ L(w).
To define the straight-line fragment of the core constraint language, we first write R(x, y) as y = R(x). This notation is quite
natural since R can be viewed as a string transformation from the
input x to the output y. [However, a word of caution is necessary:it is important to remember that R is a relation that need not be afunction in general.] We also say that a variable x is a source variable in the relational constraint φ if there is no conjunct in φ of theform x = x1 · · · xn or x = R(y) for some transducer R.
Definition 4 (Straight-line constraints). A relational constraint φis said to be straight-line if it can be rewritten (by∧reordering the
conjuncts) as a relational constraint of the form m
i=1 xi = Pisuch that:(SL1) x1 , . . . , xm are different variables(SL2) Each Pi uses only source variables in φ or variables from{x1 , . . . , xi−1 }.
We say that a string constraint is straight-line if it is a conjunctionof a straight-line relational constraint with a regular constraint. Let
SL be the set of all straight-line string constraints.
An example of a straight-line string constraint is y = R(x) ∧z = yyz ′ . Another example is the constraint from Example 1.
Straight-line restrictions also rule out all the undecidable constraints from Section 3, e.g., formulas of the form x = y ∧ R(x, y)and x = yz ∧ R(z, x).
The literal definition of straight-line constraints does not givean efficient algorithm for checking whether a constraint is straightline. This, however, can be done efficiently.
Proposition 4. There is a linear-time algorithm for checking
whether a relational constraint φ can be made a straight-line constraint (by ∧reordering equations) and, if so, outputs the reordered
constraint m
i=1 xi = Pi satisfying (SL1) and (SL2).
The proof of this proposition is standard. Straight-line relational
constraints can be visualised by drawing a “dependency graph”
of the variables in the constraints. Formally, given a relational
constraint φ, the dependency graph G(φ) of φ is the directed graphwhose nodes are the string variables appearing in φ and there is anedge from variable x to y iff (a) φ contains a conjunct of the form
R(x, y), for a rational relation R, or (b) an equation of the form y =x1 . . . xn for some string variables x1 . . . xn which include x. It iseasy to see that straight-line constraints have acyclic dependency
graphs. In fact, the converse is also true provided that the relational
constraint φ is uniquely definitional (i.e. there are no two conjuncts
x = P and x = P ′ in φ with the same left-hand side variable).
A linear-time algorithm for Proposition 4, then, first checks if thegiven constraint φ is uniquely definitional by sequentially going
through each conjunct while maintaining m bits in memory (onefor each variable in the left-hand side of an equation). Once uniquedefinitionality has been checked, the algorithm checks whether the
directed graph G(φ) is acyclic and, if so, output a topological sort,which is well-known to be solvable in linear-time (e.g. see [23]).
The topological sort corresponds to a reordering of the conjuncts in
φ so that (SL1) and (SL2) are both satisfied.
Our main result states that satisfiability for SL is decidable.

Theorem 5. S ATISFIABILITY for the class SL is EXPSPACEcomplete.
Recall that EXPSPACE problems require double-exponential
time algorithms in the worst case. An important corollary of theproof of Theorem 5 is a bounded model property.
Theorem 6. If a string constraint φ in SL is satisfiable, then it
p(|φ|), for somehas a solution with each word of length at most 22
polynomial p(x).
In Theorem 10 and Theorem 11 below, we identify a natural
restriction of SL that yields an upper bound for satisfiability —PSPACE (i.e., a single-exponential time) and satisfying models of
size at most single-exponential — and seems sufficiently expressive
in practice (e.g. it subsumes all our examples).
Remark. The reader might be wondering whether Theorem 5 andTheorem 6 immediately follow from Proposition 2? This is not
the case since AC does not permit equalities and concatenations(therefore, expressions of the form x = y.z cannot be expressed).
Similarly, the theorems also do not immediately follow from theeffective closure of regular languages under (1) pre/post images
under rational relations (see discussion below Proposition 2), and(2) concatenation. For example, consider the constraint x = yy ∧y ∈ L(a∗ + b∗ ) ∧ x ∈ L(ab) over the alphabet Σ = {a, b}. Thisis unsatisfiable. Instead, naively applying the two aforementioned
closure, we would deduce that x matches (a∗ + b∗ ).(a∗ + b∗ ),which can be matched by ab, i.e., a false positive. As we shallsee later, multiple occurrences of variables in an assignment yield
constraints with “dimensions” > 1 (definition below), instances ofwhich include all the mutation XSS examples in the paper.
4.1

Application to Detecting Mutation XSS

Before proving Theorems 5 and Theorem 6, we will mention thatthe logic SL is sufficiently powerful for expressing string constraints that arise from analysis of mutation XSS vulnerability in
web applications. By Theorem 5, such a vulnerability analysis canbe performed automatically. We have seen one such example (i.e.
Example 1). We will now provide other examples of mutation XSS
attacks that can be expressed within the framework of SL.
Example 4. We have seen that the script in Example 1 contains an
XSS bug. As suggested in [38], the corrected version of the script
swaps the order of the sanitisation functions escapeString andhtmlEscape resulting in the following script:
var x = goog.string.escapeString(cat);var y = goog.string.htmlEscape(x);catElem.innerHTML = '<button onclick="createCatList(\'' + y + '\')">' + x + '</button>';This script is no longer vulnerable to the attack pattern e1 provided
in Example 1. The program logic of the corrected script can be
expressed in SL using the same formula as for Example 1 (seeIntroduction) except that the transducers R1 and R2 are swapped.
The algorithm from Theorem 5 will be able to automatically pointout that the script is secure against the attack pattern e1.
Example 5. This example is an adaptation of vulnerable code
patterns from [33, Listing 1.12] applied to the previous example.
After the JavaScript from Example 1 has been corrected in Example
4, suppose now that a programmer wishes to introduce a new“title” HTML element into the HTML document in which the newcatalogue category name will be displayed. The following codesnippet contains two lines in this HTML file:<h1>New catalogue category:<span id="node1">TBA</span></h1><div id="node2"></div>

The following JavaScript code snippet is a modification of the
JavaScript from Example 4 which additionally puts the new catalogue category name in the title (i.e. ID node1):
var titleElem = document.getElementById("node1");
var catElem = document.getElementById("node2");
var x = goog.string.escapeString(cat);titleElem.innerHTML = x;
var y = goog.string.htmlEscape(titleElem.innerHTML);
catElem.innerHTML = '<button onclick="createCatList(\'' + y + '\')">' + x + '</button>';This JavaScript now contains a subtle mXSS vulnerability. Consider the value cat = '&#39;);alert(1);//'. The value x
will be the same as cat since the metacharacters ' and " donot occur in cat. The value of titleElem.innerHTML is, however, ');alert(1);// since an implicit browser transduction occurs upon writing into the DOM via innerHTML. HTMLescaping ');alert(1);// results in the string &#39;);alert(1);//,
which is the value of y. Another implicit browser transduction takes
place when assigning a value to catElem.innerHTML. The DOM
element catElem now contains the HTML markup:<button onclick="createCatList('');alert(1);//')">');alert(1);//')</button>

Upon clicking the button, the browser executes the attacker’s script
alert(1) after createCatList has been invoked. The XSS bug
is due to the programmer’s wrong assumption that the value of
titleElem.innerHTML is the same as x after the assignment.
Let us now encode the program logic of the above JavaScript
as a straight-line string constraint. Let e1 be the attack patternfrom Example 1. As in Example 1, let R1 and R2 be transducers
implementing htmlEscape and escapeString, and let R3 be thetransducer implementing the implicit browser transductions upon
innerHTML assignments. The desired formula can now be written
as a conjunction of• x = R2 (cat)• titleElem.innerHTML = R3 (x)• y = R1 (titleElem.innerHTML)• z = w1 · y · w2 · x · w3 for some constant strings w1 , w2 , w3
• catElem.innerHTML = R3 (z)• catElem.innerHTML matches e1.

Observe that this is a straight-line string constraint. Therefore, thealgorithm from Theorem 5 will be able to automatically detect avulnerability against the attack pattern e1.
In the appendix, we will provide another example of mXSS bugfrom adapted from [62] and show how it can be analysed within theframework of SL.
Remark. At this stage, the reader might be wondering about
the security implication when the above formulas φ are satisfiable or unsatisfiable. Unsatisfiability rules out specific vulnerability pattern. In the case of satisfiability, since attack patterns(including e1) generally overapproximate a set of bad strings, asolution to φ might not correspond to an actual attack. There
are multiple proposals to address this problem (e.g. see [8, 75]).
One method (e.g. see [8]) is to supply each attack pattern (e.g.
Σ∗ <script>Σ∗ ) with a set of test cases in the form of actual
strings (e.g. <script>alert(1);</script>). Replacing e1 by
a specific test case, φ can be checked again for satisfiability.
4.2

Proofs of Theorem 5 and Theorem 6

We start by proving the upper bound of Theorem 5. Then we
explain how Theorem 6 follows from it. Finally, we sketch theproof of the lower bound of Theorem 5.

4.2.1

Upper Bound of Theorem 5

Let SLr denote the restriction of SL to formulas which do not involve any concatenation, i.e., constraints of the form y = y1 . . . yn .
The crux of the algorithm witnessing Theorem 5 is that we transform the input constraint φ in SL into one in the class SLr . After
this, in Step 3 we will apply a classic result in the theory of rational
relations to obtain decidability (or a recent result [10] for a better
complexity). We now provide the details of our algorithm for thesatisfiability problem for SL.
Step 1: simplification of regular constraints Recall that a regular constraint is a boolean combination of constraints of the form
P (x), where P is a regular language given as an NFA over a finite
alphabet Σ. Given a regular constraint ψ, there exists an equivalent constraint in disjunctive normal form (DNF) of exponential
size, where each disjunct θ is a conjunction of literals involving
the atoms from ψ of the form P (x) (so θ has size linear in |ψ|).
From propositional logic, we know that there is a standard enumeration of these disjuncts, i.e., enumerate satisfying assignments ofψ treated as a propositional formula (i.e. each atom P (x) is now
a proposition). Such an enumeration runs in polynomial space andexponential time.
Next, each disjunct θ in the aforementioned enumeration can
now be converted into a conjunction
P1 (x1 ) ∧ · · · ∧ Pn (xn )(1)of positive literals, where each string variable xi is constrained only
by precisely one atomic regular constraint Pi . This can be doneby complementing each NFA that occurs as a negative literal inθ, and by computing a single NFA for the intersection of regular
languages by a standard product automata construction in the casewhen a string variable is constrained by several literals in θ. This
construction runs in exponential time.
Let φ be the given constraint in SL, consisting of the conjunction of a relational constraint χ and a regular constraint ψ. In orderfor φ to be satisfiable, it is sufficient and necessary that χ ∧ θ issatisfiable, for some disjunct θ in the enumeration of disjuncts of
ψ in DNF. In this step, our algorithm simply guesses such disjunctθ (which is of polynomial size). The remaining steps of the algorithm then check whether χ ∧ θ is satisfiable. From our previous
remarks, we may assume then that θ is of the form (1), where eachstring variable xi is uniquely constrained by a literal Pi (xi ). We
also assume, without loss of generality, that each variable y in χ isconstrained by some literal P (y) in θ. Otherwise, we simply add toθ a literal which states that y belongs to Σ∗ .
Step 2: Removing concatenation For this step, we will transforma given constraint φ in SL into a constraint φ′ that uses only
atomic string constraints of the form x = R(y), i.e., all string
constraints of the form x = y1 . . . yn are removed. Since word
equations of the form w = yy cannot in general be expressed asa transducer, our transformation cannot possibly express the same
property that φ expresses, i.e., it is impossible that φ and φ′ havethe same set of satisfying assignments in general. However, as weshall see later, by introducing extra variables and allowing bothconjunctions/disjunctions for our string constraints it is possible
to produce the formula φ′ without concatenation operators whose
satisfying assignments can be easily transformed into satisfying
assignments of φ and vice versa (see Lemma 7 below).
The structure of the straight-line relational constraint φ immediately gives us a topological sort x1 ≺ . . . ≺ xm on G(φ). We
may assume without loss of generality that all the source nodes areat the beginning of the topological sort, i.e., it is not the case thatxi ≺ xi+1 for some non-source node xi and some source nodexi+1 (which might happen if they are incomparable in G(φ) construed as a partial order). Next, for each variable y in φ, we will

define a relational constraint λrel (y) involving only rational relations (but with conjunctions and disjunctions), a regular constraint
λreg (y), and fresh variables y(1), . . . , y(maxy ), where maxy is apositive integer. We will define these by induction on the positionof y with respect to the order ≺.
Base cases: A source node y with a regular constraint P (y).
For this, we set λrel (y) := ⊤ and λreg (y) := P (y). We also set
maxy = 1 and define a fresh variable y(1).
First inductive case: A non-source node y with an assignment y = y1 . . . yn and a regular constraint P (y), for somey1 , . . . , yn ≺ y. By induction, we assume that maxyi ∈ Z>0
and new string variables yi (1), . . . , yi (maxyi ) have all been defined (for each 1 ≤ i ≤ n). The main idea behind our construction
is to interpret each assignment for yi (1 ≤ i ≤ n) as the “concatenation” of an assignment for∑yi (1), . . . , yi (maxyi ), respectively.
Formally, let maxy = n
j=1 maxyj and S = {1, . . . , maxy }.
We define a selector function ν : S → Z2>0 as follows: Foreach k ∈ S it is the case that ν(k) is a pair ∑of numbers (i, l),where i is the smallest number i such that k ≤ ij=1 maxyj and∑i−1
l := k− j=1
maxyj . Intuitively, if ν(k) = (i, l), then ν “selects”
the variable yi for the fresh variable y(k), and l further “refines”
this selection to yi (l).
In the set λrel (y) we “define” the fresh variables y(k), for eachk ∈ S. We do so by setting λrel (y) to be the conjunction of all
formulas of the form y(k) = yi (l), where k ∈ S and (i, l) = ν(k).
Notice that we can express each such conjunct as a transducer
R(yi (l), y(k)), where R is the identity transducer, i.e., the one that
outputs its input without modification.
We now define λreg (y). To this end, we first observe that an
accepting run of the automaton P on a word w = w1 · · · wN ,can be split into N subruns. To make this notion more precise, we
define an N -splitting σ of an automaton A with states Q to be asequence q0 , . . . , qN ∈ Q such that each state qi (i ∈ {1, . . . , N })is reachable from the state qi−1 in A. Recall that A[q,q′ ] is the NFA
A whose initial (resp. set of final states) is replaced by q (resp.
{q ′ }). Then λreg (y) is defined as:∨
P[q0 ,q1 ] (y(1)) ∧ · · · ∧ P[qmaxy −1 ,qmaxy ] (y(maxy )),σ=q0 ,...,qmaxy

where σ ranges over maxy -splittings of P . That is, λreg (y) statesthat there is some maxy -splitting q0 , . . . , qmaxy of P such thateach y(k) (1 ≤ k ≤ maxy ) is accepted by P[qk−1 ,qk ] . This
amounts to y being accepted by P (since y is interpreted as the“concatenation” of y(1), . . . , y(maxy ), respectively).
Second inductive case: A non-source node y with an assignment y = R(x) and a regular constraint P (y), for some x ≺ y.
By induction, we assume that maxx ∈ Z>0 and new string variables x(1), . . . , x(maxx ) have all been defined. The crux of theconstruction is to replace y = R(x) by “splitting” it into maxx
different constraints. This is achieved by splitting the transducer R(syntactically seen as an NFA over Σε × Σe ). More precisely, letmaxy = maxx . Then λrel (y) is:
∨

∧

maxy

y(i) = R[pi−1 ,pi ] (x(i)),σ=p0 ,...,pmaxy i=1

where σ ranges over all maxy -splittings of R. We may define
λreg (y) precisely in the same way as in the first inductive case.
The output formula φ′ : We have now defined λrel (y) andλreg (y) for each node y in G(φ). The output of our transformation is the formula∧φ′ :=(λrel (y) ∧ λreg (y)),
ywhere y ranges over all variables in φ.
Notice that φ′ is not necessarily a string constraint, as λrel (y)might be a disjunction of relational constraints for some y’s. The
notion of satisfiability extends to this class of formulas in thestandard way. In particular, an assignment ι for the variables inλrel (y) satisfies this formula iff it satisfies one of its disjuncts. The
formula φ′ is satisfiable iff there is an assignment ι for the variablesof φ′ that satisfies λrel (y) ∧ λreg (y) for each string variable y in φ.
Correctness: The following lemma shows that our transformation is satisfiability preserving; in fact, there is an easy way to obtain satisfying assignments for φ from those of φ′ and vice versa.
Lemma 7 (Correctness). φ is satisfiable iff φ′ is satisfiable.
The proof is done by induction on the position of nodes in the
topological sort ≺ of G(φ). To this end, given a node y in G(φ),
we define φy to be the set of conjuncts in φ involving only y andvariables that precede y in ≺. That is, the conjuncts in φy are theones that only mention variables in the set Zy := {x : x ⪯ y}. For
example, if φ contains the constraint z = yy, then this constraint
cannot be a conjunct∧ of φy (but it is a conjunct of φz ). Similarly,
we define φ′y := x∈Zy λrel (x) ∧ λreg (x). That is, φ′y is the setof conjuncts in φ′ of the form λrel (x) ∧ λreg (x) involving only
variables in the set Zy′ := {x(i) : x ∈ Zy , 1 ≤ i ≤ maxx }.
We will prove the following technical lemma, which is a stronger
formulation of Lemma 7.
Lemma 8. For each node y in G(φ) and every assignment ι :Zy → Σ∗ of variables in φy , the following are equivalent:(i) ι is a satisfying assignment for the formula φy .
(ii) There is a satisfying assignment ι′ : Zy′ → Σ∗ for φ′y such that
ι(x) = ι′ (x(1)) ◦ · · · ◦ ι′ (x(maxx )) for each x ⪯ y.
The proof of Lemma 8 is by induction on the position of y in the
topological sort ≺ of G(φ). Due to lack of space we relegate thisproof to the appendix. Since Lemma 8 is a stronger formulation ofLemma 7, the correctness of our construction in Step 2 follows.
Step 3: Solving the final formula After applying the transformation from Step 2, the size of the resulting formula φ′ could be
exponential in |φ| due to repeated applications of constraints of theform y = y1 . . . yn , where some variable yi occurs several times
on the right-hand side of the equation. In particular, there are exponentially many conjuncts of the form λrel (x) ∧ λreg (x) in φ′ , Moreprecisely, the resulting formula φ′ is a conjunction of multiple formulas of two types:• conjunctions of atomic formulas of the form R(x, y), for sometransducer R, or a disjunction of several such formulas.
• atomic formulas of the form P (x), for some regular language

P , or a disjunction of several such formulas.
So, except for the disjunctions, the formula φ′ satisfies the shapeof the fragment SLr of SL. In fact, it is not difficult to remove
these disjunctions without too much additional computational overhead. Recall that disjunctions were caused by splitting automata ortransducers. Although in this case a conjunct can have exponentially many disjuncts, we may simply nondeterministically guess
one of the disjuncts (in effect, guessing one of the splittings of theautomata/transducers). Nondeterministic algorithms can be determinised at the cost of quadratically extra space [56]. The resulting
formula φ′′ is now a conjunction of atomic formulas of the form
R(x, y) or P (x). Moreover, it is easy to prove that the undirected
graph G(φ′′ ) defined in Section 3 is acyclic:
Lemma 9. G(φ′′ ) is acyclic. Thus, φ′′ ∈ AC.

∧
Proof. By construction of φ′ = y (λrel (y) ∧ λreg (y)), for each′variable y in φ there is at most one x such that λrel (y) (and,therefore, φ′ ) contains an atom of the form y = R(x), for R arational transducer. From this it is clear that G(φ′′ ) is acyclic.
Decidability in EXPSPACE can now be easily obtained by
Proposition 2, i.e., we apply Proposition 2 on the formula φ′′ ofsize at most exponential in |φ| and so our resulting algorithm runs
in exponential space, as desired.
4.2.2

Proof of Theorem 6

Suppose that φ ∈ SL is satisfiable. The previous algorithm computes a formula φ′′ in AC such that φ is satisfiable iff φ′′ is satisfiable (cf. Lemma 7). This implies that φ′′ is satisfiable and, so by thebounded model property from Proposition 2, φ′′ has a solution ofsize at most exponential in |φ′′ |. Now, the size |φ′′ | is O(Dim(φ)×|φ|), where Dim(φ) is the dimension of φ which is defined to be
the maximum maxx over all string variables x in φ. The value
Dim(φ) is at most exponential in |φ|. This implies that φ′′ has aO(1)|φ|O(1)solution of size at most F (|φ|) := 2(Dim(φ)×|φ|)= 22.
Then, by Lemma 8, φ has a solution of size Dim(φ) × F (|φ|) =O(1)|φ|O(1)2(Dim(φ)×|φ|)= 22, giving us the desired upper boundon the maximum solution size for φ that we need to explore.
4.2.3

Lower Bound of Theorem 5

In order to prove that checking satisfiability of string constraints in
SL is EXPSPACE-hard, we reduce from the acceptance problem
for a deterministic Turing machine M that works in space 2cn , forc > 1. That is, we provide a polynomial time reduction that, given
an input w to M, it constructs a constraint φ(w) in SL such thatw is accepted by M if and only if φ(w) is satisfiable. Due to lackof space, the complete proof is relegated to the appendix. We only
sketch the main ideas below.
The reduction starts by constructing a regular constraint of theform P1 (x) ∧ · · · ∧ Pm (x), in such a way that a word w satisfies
this constraint if and only if it codifies a sequence of configurations of M, the first such configuration corresponds to the initialconfiguration of M on input w, and the final such configuration
corresponds to a final configuration of M. The we only require tocheck that each non-initial configuration in w is obtained from its
preceding configuration by applying the transition function of M.
This is done by adding a set of relational constraints that creates
an exponential number of copies of x (with equations of the formy = xx), but deletes certain distinguished parts of each such copy
(with suitable transducers).
4.3

A PSPACE Restriction

We mention a natural restriction of SL that yields a PSPACE upperbound and seems to be sufficiently expressive in practice. Recall
that the dimension of a string constraint φ is the maximum maxx
over all string variables x in φ. [Incidentally, this notion is closely
related to the notion of dimension from the study of context-freegrammars (e.g. see [28]).]
Theorem 10. For any fixed k ∈ N, satisfiability for the class of
formulas in SL of dimension k is PSPACE-complete.
The lower bound follows since our logic can easily encode indimension one the PSPACE-complete problem of checking emptiness of the intersection of m regular languages given as NFA [42].
[In fact, when k = 1, the logic still subsumes SLr .] An easy corollary of the proof of Theorem 6 is the following improved bound.
Theorem 11. For any fixed k ∈ N, if a formula φ of dimension
k is satisfiable, then it has a solution with each word of length at
most 2p(|φ|) for some polynomial p(x).

This bound can be derived by noticing from the proof of Theorem 6 that the maximal solution size of φ that one needs to exO(1)plore is F (x) := 2(Dim(φ)×|φ|), which is exponential in |φ| if
Dim(φ) is a fixed constant. Note that the dimension of the scripts
in all our examples is 2 (in fact the dimensions of the examples inthe benchmark of [72] are all 1, except for one with dimension 4).

5. Adding Integer and Character Constraints
In this section we extend the language SL from Section 4 withinteger and character constraints, and show that the satisfiability
problem remains decidable in EXPSPACE. We also show that thisbound continues to hold in the presence of two other importantfeatures: the IndexOf constraints and disequalities between strings.
Our language will use two types of variables, str and int. The
type str consists of the string variables we considered in the previous sections. In particular, a constraint in SL only uses variablesfrom str. On the other hand, a variable of type int (also called an
integer variable) ranges over the set N of all natural numbers. The
choice of omitting negative integers is only for simplicity, but our
results easily extend to the case when int includes negative integers. For each T ∈ {str, int}, we use V(T ) to denote the set ofvariables of type T .
We start by defining integer constraints, which allow us toexpress bounds for linear combinations of lengths or number ofoccurences of symbols in words.
Definition 5 (Integer constraints). An atomic integer constraint
over Σ is an expression of the form
a1 t1 + · · · + an tn ≤ d,where a1 , . . . , an , d ∈ Z are constant integers (represented inbinary) and each ti is either (i) an integer variable u ∈ V(int),(ii) |x| for a string variable x ∈ V(str), or (iii) |x|a for x ∈V(str) and some constant letter a ∈ Σ. Here, |x| (resp. |x|a )denotes the length of x (resp. the number of occurrences of a in x).
An integer constraint over Σ is a Boolean combination af atomic
integer constraints over Σ.
Character constraints, on the other hand, allow us to compare
symbols from different strings. They are formally defined below.
Definition 6 (Character constraints). A atomic character constraint
over Σ is an expression of the form x[u] = y[v], where: (1)x and y are either a variable in V(str) or a word in Σ∗ , and(2) u and v are either integer variables in V(int) or constantpositive integers. Here, the interpretation of the symbol x[u] isconsistent with our notation from Section 2, i.e., the u-th letter in x.
A character constraint over Σ is a Boolean combination af atomic
character constraints over Σ.
Next, we define the extension of the class SL with integer andcharacter constraints.
Definition 7 (The class SLe ). The class SLe consists of all formulas φ ∧ θint ∧ θchar such that (i) φ is a constraint in SL, (ii) θint is
an integer constraint, and (iii) θchar is a character constraint.
Since constraints in SLe are two-sorted, we have to slightly
refine the notion of assignment. Formally, an assignment for aconstraint φ in SLe is a mapping ι from each variable x ∈ V(T )in φ to an object of type T (i.e. either a string or an integer). We
also assume for safety that for each term of the form x[u] in φ
it is the case that ι(u) ≤ |ι(x)| (i.e., ι(u) is in fact a positionin ι(x)). [If this assumption is not met, we can simply definethat the assignment does not satisfy the formula φ.] As before, ιsatisfies φ if the constraint φ becomes true under the substitutionof each variable x by ι(x). We formalise this for atomic integer andcharacter constraints (as Boolean connectives are standard):∑
1. ι satisfies
atomic integer constraint n
i=1 ai ti ≤ d if and∑thenonly if i=1 ai ι(ti ) ≤ d, where for each 1 ≤ i ≤ n wehave that (i) ι(ti ) = |ι(x)|, if t = |x| for x ∈ V(str), and (ii)
ι(ti ) = |ι(x)|a , if t = |x|a for x ∈ V(str) and a ∈ Σ.
2. ι satisfies the atomic character constraint x[u] = y[v] if andonly if ι(x)[ι(u)] = ι(y)[ι(v)], where (i) ι(x) = x (resp.,
ι(y) = y), if x (resp., y) is a constant word over Σ, and (ii)
ι(u) = u (resp., ι(v) = v), if u (resp., v) is a positive integer.
The constraint φ is satisfiable if there exists a satisfying assignment for it. The satisfiability problem for SLe is the problem ofdeciding if φ is satisfiable, for a given constraint φ in SLe .
5.1

The Satisfiability Problem for SLe

In this section, we will show that our EXPSPACE upper bound forthe satisfiability of SL extends to SLe .
Theorem 12. The satisfiability problem for the class SLe is solvable in EXPSPACE. Furthermore, if SLe has a solution, then it hasp(x)a solution of size at most 22, for some polynomial p(x).
The rest of the section is dedicated to proving the theorem. Let
SLer be the extension of SLr with integer constraints and character
constraints. Given a formula φ ∈ SLe , we first transform φ into
a constraint φ′ in SLer by using (an extension of) the satisfiabilitypreserving transformation from Section 4.2. We will then show thatthe formula φ′ has a bounded model property (cf. Lemma 13 below). More precisely, if φ′ is satisfiable, then it has a satisfying assignment of size at most exponential in |φ′ |. This immediately provides a decision procedure for checking satisfiability of φ, though anaive algorithm only yields a triple-exponential procedure. We willshow, however, that this yields a polynomial-space procedure forchecking satisfiability of φ′ , and hence a single exponential spaceprocedure for checking satisfiability for φ.
5.1.1 Transforming SLe into SLer
Suppose that φ = φstr ∧ φint ∧ φchar ∧ φreg ∈ SLe , where φstr is arelational constraint in SL, φreg a regular constraint, φint an integer
constraint, and φchar a character constraint.
We apply the transformations from Step 1 and 2 in Section
4.2 on the formula ψ := φstr ∧∧ φreg ∈ SL, yielding an acyclic
string/regular constraint ψ ′ = y λrel (y) ∧ λreg (y) with no concatenation (but possibly some disjunctions), where each variable
x in ψ is replaced by several variables x(1), . . . , x(maxx ) in ψ ′ .
Recall that Lemma 7 states that ψ is satisfiable iff ψ ′ is satisfiable. In fact, following the notation in Step 2 of Section 4.2,
Lemma 8 shows that for each node y in G(ψ) and every assignment ι : Zy → Σ∗ of (string) variables in the constraint ψy (associated with the node y in G(ψ)), the following two conditions areequivalent:• ι is a satisfying assignment for the formula ψy .
• There exists a satisfying assignment ι′ : Zy′ → Σ∗ for the∧formula ψy′ := y∈Zy λrel (y) ∧ λreg (y) such that for eachx ⪯ y:
ι(x) = ι′ (x(1)) ◦ · · · ◦ ι′ (x(maxx )).
(*)

Handling the integer constraint is now easy. Because of (*),
we simply replaceeach occurrence of(resp. |y|a , where a ∈
∑max
∑|y|
maxy
y
′
Σ) in φint by|y(i)|(resp.
i=1
i=1 |y(i)|a ). Let ψint be
the resulting formula. [Note that y is not a variable in ψ ′ .] Thistransformation preserves satisfiability, even in the above stronger
sense.
Let us now show how to deal with the character constraint φchar .
Without loss of generality, we may assume that the term t which

occurs on left/right hand side of atomic character constraint is of
the form x[u] (for an integer variable u), which denotes the u-th
character in x. [If t is a string variable x, we can replace x by
x[u], where u is a fresh int variable, and add the integer constraint|x| = 1 ∧ u = 1. Similarly, if t is of the form x[c], where c isan integer constant, we could simply replace this by x[u], for a
fresh int variable u, and add the integer constraint u = c.] Now
the u-th character x[u] in x must fall within precisely one of theword segments x(1), . . . , x(maxx ). Therefore, we simply make anondeterministic guess on which segment x(i) the position x[u]belongs to, and replace every occurrence of x[u] by x(i)[u′ ], where
u′ is a fresh ∑int variable, and add an integer constraint of the formu = u′ + i−1
j=1 |x(j)|. Observe that the constraint θ that we
generate from φchar involves both integer constraint and character
constraints. Then, the formula φ is satisfiable iff, for some formulaθ obtained from the aforementioned nondeterministic construction,′
the formula ψ ′ ∧ ψint
∧ θ is satisfiable.
Note, however, that ψ ′ still has some disjunctions and so strictly
speaking it is not a formula in SLr . So, to complete our transformation of φ into SLer , we use Step 3 from Section 4.2 on ψ ′ to makefurther nondeterministic guesses to eliminate the disjunctions. Let
us call a possible resulting formula ψ ′′ . Therefore, φ is satisfiable′∧ θ is satisfiable.
iff, for some ψ ′′ and θ, the formula ψ ′′ ∧ ψint
5.1.2

Bounded Model Property for SLer

We will prove a bounded model property for SLer .
Lemma 13 (Bounded Model). Given a formula φ in SLer , if it
is satisfiable, then there exists a satisfying assignment of whose
strings are of length at most exponential in |φ| and whose integers
are of size (in binary) at most polynomial in |φ|.
Before proving this lemma, we will first show how this can beused to obtain Theorem 12.
5.1.3

Lemma 13 Implies Theorem 12

As mentioned in Section 5.1.1, the problem of checking whether
an SLe formula φ is satisfiable can be reduced in nondeterministic
exponential time to checking whether an SLer formula φ′ is satisfiable. Next we construct an algorithm that solves this problem in
PSPACE in the size of φ′ , and, therefore, in EXPSPACE in the sizeof φ (since φ′ might be exponentially bigger than φ). Theorem 12then follows from the fact that nondeterministic exponential time iscontained in EXPSPACE and EXPSPACE computable functions
are closed under composition.
In order to do this, the first step is to restate a stronger form of
Proposition 2. To this end, we first recall the standard generalisationof the notion of transducers to allow an arbitrary number of tracks(e.g. see [21]). An m-track (rational) transducer over the alphabetΣ is a tuple A = (Γ, Q, δ, q0 , F ), where Γ := Σmϵ and Σϵ :=Σ ∪ {ϵ}, such that A is syntactically an NFA over Γ. In addition,
we define the m-ary relation R ⊆ (Σ∗ )m that A recognises toconsist of all tuples w̄ for which there is an accepting run
σ

σ

σ

1
2
n
π := q0 −→q1 −→· · · −→
qn

of A (treated as an NFA) such that w̄ = σ1 ◦ σ2 ◦ · · · ◦ σn ,where the string concatenation operator ◦ is extended to tuples
over words component-wise (i.e. (v1 , . . . , vk ) ◦ (w1 , . . . , wk ) =(v1 w1 , . . . , vk wk )). An m-ary relation is said to be rational if it
is recognised by an m-ary transducer. To avoid notational clutter,
we shall confuse an m-ary transducer and the m-ary relation that itrecognises. In the following proposition, the set of solutions (i.e.
satisfying assignments) to a formula φ in SLe — i.e. mappingsfrom variables x in φ to strings, integers, or characters dependingon the type of x — is interpreted as a relation (i.e. a set of tuples)by fixing any ordering to the variables occuring in φ.

Proposition 14 ([10]). There exists an exponential-time algorithm
for computing an m-track transducer A = (Γ, Q, δ, q0 , F ) for
the set of solutions of an input formula φ ∈ SLr with variables
x1 , . . . , xm , where each state in Q is of size polynomial in |φ|.
Furthermore, there exists a polynomial space algorithm for:1. Computing q0 .
2. Checking whether a string is a state of Q.
3. Checking whether a state q belongs to F .
4. Checking whether (q, ā, q ′ ) ∈ δ, for some given states q and q ′and a symbol ā ∈ Γ.
This proposition is a stronger version of Proposition 2, which
follows from the proof of Theorem 6.7 in [10].
Obtaining a PSPACE algorithm for checking satisfiability of agiven formula φ′ in SLer is now almost immediate. Our nondeterministic algorithm guesses an assignment to each character variable in φ, whose size is linear in |φ|. By virtue of Lemma 13, ouralgorithm needs to guess an assignment to each integer variable inφ of size polynomial in |φ| (i.e. numbers represented in binary).
In effect, if |x| (resp. |x|a ) appears in the integer constraint of φ,
our algorithm also guesses the length of (resp. number of occurrences of a in) the string variable x. Our algorithm now checks thatthe integer constraints and character constraints in φ are satisfied.
Next our algorithm guesses assignments to the string variables in φ.
However, since they are of exponential size in the worst case, ouralgorithm will have to construct the assignment on the fly. By using
Proposition 14, we will have to simultaneously construct the string
assignments to all string variables in φ. To this end, for each string
variable x, we keep track of |Σ| + 1 extra integer counters (counting in binary) l(x) and la (x), respectively, for each a ∈ Σ. The
counter l(x) (resp. la ) keeps track of the length of (resp. number ofoccurrences of a in) the partially constructed string assignment forx. Putting this all together, if A = (Γ, Q, δ, q0 , F ) is the m-tracktransducer for the set of solutions for φ (as in Proposition 14), ouralgorithm first computes q0 and let q = q0 . It then repeats the following step until (i) q ∈ F , and (ii) l(x) = |x| and la (x) = |x|a ,for each string variable x and letter a ∈ Σ:

counter machine [37] (i.e. counter machines whose counters can
switch between non-incrementing and non-decrementing modes
only for a fixed r ∈ N number of times). [In the case of monotonic
counter machines, we have r = 0]. Such a computation model is
not Turing-complete. In fact, their sets of reachable configurations
are effectively semi-linear, as was first shown in [37]. We will use arecent result from [41, 63] to analyse the size of the smallest reachable configuration, which will give us the bounded model propertyof SLer .
We now formalise the notion of monotonic counter machinewith k ∈ N counters. A monotonic counter machine is a tupleA = (Q, δ, q0 , F, P ), where: (1) Q is a finite set of states, (2)q0 ∈ Q is an initial state, (3) F ⊆ Q is a set of final states,(4) P = {p1 , . . . , pk } is a set of k counters, and (5) δ ⊆ (Q ×
ConsP ) × (Q × {0, 1}k ) is the transition∧ relation, where ConsP
is the set of counter tests of the form ki=1 pi ∼i 0 such that∼i ∈ {=, >} for each 1 ≤ i ≤ k. A vector v̄ ∈ {0, 1}k suchthat (q, ψ, q ′ , v̄) ∈ δ, for q, q ′ ∈ Q and ψ ∈ ConsP , is called an
update vector. In the sequel we shall also denote this vector by its
characteristic set, i.e., the one which consists of all counters pi ∈ Psuch that v̄[i] = 1.
A configuration of A is a pair (q, v̄), where q ∈ Q and v̄ ∈ Nk .
A run π of A is a sequence of the form
(q0 , v̄0 ), (q1 , v̄1 ), . . . , (qn , v̄n )such that:• qi ∈ Q for each 1 ≤ i ≤ n,
• v̄0 = (0, . . . , 0) (i.e., counters are initially empty),• for each 1 ≤ i ≤ n there exists a transition (qi−1 , ψ(x̄), qi , c̄) ∈δ such that ψ(v̄i−1 ) is true, and v̄i = v̄i−1 + c̄.
The configuration (qn , v̄n ) is said to be accepting if qn ∈ F . The
set of accepting configurations of A is denoted by L(A).
From our transducer A = (Γ, Q, δ, q0 , F ), we construct ourmonotonic counter machine B = (Q, δ ′ , q0 , F, P ), where P consists of the following counters:

1. Guess a state q ′ of Q and a symbol ā ∈ Γ = Σmϵ of A, andcheck that (q, ā, q ′ ) ∈ δ in polynomial space.

• c|x|a for each string variable x in φ and each letter a ∈ Σ;

2. If ā = (a1 , . . . , am ), then set l(xi ) := l(xi ) + 1 and la (xi ) :=la (xi ) + 1 for each i ∈ {1, . . . , m} and a ∈ Σ satisfying
ai = a.

• yx[u] and zx[u] for each x[u] occuring in a character constraint

3. Set q := q ′This is a nondeterministic algorithm that uses polynomial space.
Nondeterministic algorithms can be determinised at the cost ofquadratically extra space [56]. As for the bounded model property
part of Theorem 12, it can be derived in precisely the same way as
Theorem 6.
5.1.4

Proving Lemma 13

Our proof idea goes as follows. Given a satisfiable formula φ ∈SLer with m variables, we suppose that ι is a satisfying assignmentof φ. It assigns each character variable x[u] to a certain characterι(x[u]) ∈ Σ. So, we will only have to ensure the existence of a satisfying assignment that assigns each string (resp. integer) variable
to a small enough string (resp. integer). To this end, Proposition 14
gives an m-track transducer A = (Γ, Q, δ, q0 , F ) that recognises
the set of solutions of φ. The number of states in A is exponential
in |φ|. Next we erase the input tape of A, while equipping it with
nonnegative integer-valued counters that cannot be decremented.
The resulting machine is a monotonic (Minsky’s) counter machine,whose set of final configurations captures the set of solutions for φ.
Monotonic counter machines are restrictions of reversal-bounded• cu for each integer variable u in φ;of φ.
The counter c|x|a records the number of a’s seen so far in in thetransducer’s track corresponding to the variable x. The counter curecords the guessed value for the variable u. To avoid notational
clutter, we shall confuse c|x|a (resp. cu ) with |x|a (resp. u). The
counter yx[u] records a guess for the position of u in x, which has
to be recorded separately due to the different tracks in A. The valueof zx[u] is a boolean variable (i.e., either 0 or 1) that acts as a flag
whether the guess for the variable yx[u] is complete.
We now specify the transitions in δ ′ . In doing so, we will ensurethat once a variable of the form zx[u] is set to 1, the value of yx[u]can no longer be incremented. Let W be the set of all character
variables x[u]∧ in φ. For each Y ⊆∧ W , let ψY denote the formulaof the form x[u]∈Y zx[u] = 0 ∧ x[u]∈W \Y zx[u] > 0. Then:
1. If (q, ā, q ′ ) ∈ δ, where ā = (a1 , . . . , am ), then for each subset
Y ⊆ W we add to δ ′ each transition of the form(q, ψY , q ′ , Z),
where Z consists of: (1) each |x|ai with ai ̸= ϵ, (2) yx[u] foreach x[u] ∈ Y , and (3) if zxi [u] = 0 and ai = ι(xi [u]), the set
Z may (nondeterministically) contain zxi [u] .
2. (q, ⊤, q, {u}) for each integer variable u in φ.

In other words, the first transition above simply simulates a transition of A, while the second transition nondeterministically increments the integer counter u.
Recall that φ is our initial formula in SLer and ι is a satisfying assignment for it. Now, let φint be the conjunct of φ containing the integer constraint. We use φ′int to denote a conjunction of(i)∑ the constraint φint but substituting every occurrence of |x| bya∈Σ |x|a , (ii) a conjunction of constraints of the form u = yx[u]for each x[u] ∈ W (i.e. all positions yx[u] equal u), and (iii) a conjunction of constraints of the form zx[u] = 1 for each x[u] ∈ W(i.e. all yx[u] have been completely guessed). The following lemma
is immediate from our construction and Proposition 14.
Lemma 15. Given a configuration (q, v̄) of B, the following are
equivalent:• (q, v̄) ∈ L(B) and v̄ satisfies φ′int .
• There exists a satisfying assignment ι′ of φ whose integer values

agree with v̄ and whose character values agree with ι.
We now use the following proposition, which is a result of [41](see the proof of [63, Proposition 7.5.5]):
Proposition 16. Given a monotonic k-counter machine A withn states, the set of reachable configurations can be represented
as a disjunction of existential Presburger formulas, each of size
polynomial in k + log(n) and at most O(k) variables.
Indeed, in the above proposition the number of disjuncts is polynomial in n, but this is not important for our purpose. It is now easy
to obtain a satisfying assignment for φ given our original satisfying
assignment ι. By the above proposition, the set of reachable configurations of the monotonic counter machine B that we constructed isa disjunction of existential Presburger formulas each of size polynomial in k + log(n) and with O(k) variables, where k = O(|φ|)O(1)
and n = 2|φ|. By Lemma 15 and our assumption that φ issatisfiable with assignment ι, it follows that one of these disjuncts
ψ is satisfiable. Scarpellini [59, Theorem 6(a)] proved that a satisfiable existential Presburger formula θ with c variables has solutions where each variable is assigned a number that is at mostO(1)2(|θ|+c)(and thus can be represented with at most (|θ| + c)O(1)bits). Applying Scarpellini’s result on ψ now gives us a satisfying
assignment of φ which assigns numbers of polynomially many bits
to integer variables of φ and lengths of string variables. This completes the proof of Lemma 13.
5.2 Extensions with Disequalities and IndexOf
Finally, we show that two important features can be added to thelanguage while retaining decidability in EXPSPACE: Disequalities
between strings and IndexOf constraints.
Disequalities: Assume that constraints in SLe are now extended
with disequalities of the form x ̸= y, for x, y ∈ V(str), which statethat x and y are interpreted as different strings. The disequality
relation is regular, and thus can be expressed as a transducer y =R(x). The problem is that the addition of this transducer may yielda constraint that is no longer uniquely definitional. To solve this,we use integer and character constraints; in fact, the disequalityx ̸= y is equivalent to (|x| ≠ |y|) ∨ (x[u] ̸= y[u]), for a
fresh variable u ∈ V(int). More formally, if φ is a constraint
in SLe and x ̸= y is a disequality between string variables, thenφ ∧ (x ̸= y) is satisfiable if and only if either the SLe constraintφ ∧ (|x| ̸= |y|) or the SLe constraint φ ∧ (x[u] ̸= y[u]) issatisfiable. Checking if any of these constraints is satisfiable canbe solved in EXPSPACE from Theorem 12. Clearly, adding moredisequalities does not increase the computational cost if we use a

nondeterministic algorithm that chooses to check either |x| ̸= |y|or x[u] ̸= y[u] for each disequality x ̸= y.
Expressing the IndexOf method: One reason we introduced thecharacter constraints is, besides the use of the JavaScript string
method charAt (which is used rather frequently in JavaScript
according to the benchmark [57]), they can also be used to define
IndexOf(w, x) for any word w ∈ Σ∗ , which is the most standard
usage of IndexOf method in practice. We consider both the firstoccurrence semantics (i.e., for an integer variable u, the constraintu = IndexOf(w, x) says that u is the first position in x where w
occurs), or the anywhere semantics (i.e., u = IndexOf(w, x) saysthat u is any position in x where w occurs).
Formally, an IndexOf constraint is a conjunction of expressionsof the form u = IndexOf(w, x), where w ∈ Σ∗ , x is a string
variable/constant, and u is either an integer variable or a positive
integer. The satisfaction of an expression of this form (under any of
the two semantics) with respect to an assignment of the variables
is the expected one (following the intuition given in the previous
paragraph). The next proposition states that IndexOf constraints do
not increase the “expressiveness” of SLe .
Proposition 17. Let φ be the conjunction of a constraint in SLeand the IndexOf constraint u = IndexOf(w, x). The satisfiabilityof φ can be checked in EXPSPACE.
Proof. Let w = a1 . . . ap ∈ Σ∗ . For the anywhere semantics, every
occurrence of u = IndexOf(w, x) in φ is replaced by the formulax[u1 ] = a1 ∧ · · · ∧ x[up ] = ap
u = u1 ∧ u2 = u1 + 1 ∧ · · · ∧ up = up−1 + 1,
where u1 , . . . , up are fresh integer variables. The resulting formula is an SLe constraint whose satisfiability can be checked in
EXPSPACE from Theorem 12.
The first-occurrence semantics could be handled by replacingu = IndexOf(w, x) with a relational constraint x = x1 x2 x3
and regular constraints stating that w does not occur in x1 andw = x2 . This would allow us to use the anywhere semantics toexpress u = IndexOf(w, x2 ), which can be done as before. The
problem with this approach is that the introduction of the word
equation x = x1 x2 x3 may yield a constraint that is no longer
uniquely definitional. To avoid this, we make a nondeterministic
guess (as we did for formula φchar in Section 5.1.1) as to how
x1 overlaps with x(1), . . . , x(maxx ), e.g., it might overlap with
x(1)x(2)x(3). We will then simply assert that x(1)x(2)x(3) ∈ L,
where L is the regular language of words v that contains no w
as a (contiguous) subword. We then have to apply the splitting
technique for the regular constraint ∧just as in Step of Section 4
to express x(1)x(2)x(3) ∈ L as 3i=1 x(i) ∈ Li . This can
all be done by nondeterministic guesses while incurring only apolynomial blowup.

6. Related Work and Future WorkIn this section, we mention a few related works and discuss theirconnections with our work in more detail. Roughly speaking, they
can be classified into three categories: (1) decidability results, (2)heuristics and string solver implementations, (3) benchmarking
examples. We shall also mention a few possible research avenues
in passing.
Decidability results: In §Introduction, we have mentioned theresults of Makanin’s and Plandowski’s [45, 50–52] on the decidability and complexity of satisfiability for word equations (a conjunction of equations of the form v = w, where v and w are aconcatenation of string constants and variables). We should also remark that the decidability (with the same PSPACE complexity) extends to quantifier-free first-order theory of strings with concatenations and regular constraints [20]. Since extending word equations
with finite-state transducers yields undecidability (see Section 3),
the straight-line fragment SL of our core string constraint language
is incomparable to word equations with regular constraints (neither
subsumes the other). The fragment SL is, in a sense, more complex
since its computational complexity is EXPSPACE, though for constraints of small dimensions the complexity reduces to PSPACE(cf. Theorem 10). In addition, it is still a long-standing open problem whether word equations with length constraints is decidable,
though it is known that letter-counting (i.e. counting the number ofoccurrences of 0s and the number of occurrences of 1s separately)yields undecidability [20]. On the other hand, the extension SLe of
our straight-line fragment SL is decidable (with the same complexity) and yet admits general letter-counting.
In our decidability proof of Theorem 5, we have also used theresult of Barcelo et al. [10] (see Proposition 2) that acyclic conjunctions of rational relation constraints (with regular constraints)
is decidable in PSPACE. Their logic AC, however, supports neither string concatenations nor letter-counting constraints. In fact, it
is easy to show by a standard pumping lemma argument that theconstraint x = y · y cannot be expressed in AC. For this reason, ourlogics SL and SLe are not subsumed in AC.
Abdulla et al. [7] studied acyclic constraints over systems ofword equations with a length predicate (without transducers) anddisequality constraints, for which they showed decidability. Ourdecidable logics are incomparable to their logic. On the one hand,
SLe supports finite-state transducers, letter-counting, and IndexOf
constraints, which are not supported by their logic. Our logic also
supports unrestricted disequality constraints, whereas their logic
supports only restricted (acyclic) disequalities. On the other hand,the string logic of [7] supports string equations of the form x · y =z · z ′ (i.e. both sides of the equations contain different variables),which they showed could be reduced to a boolean combination ofregular constraints. Using this reduction, we can incorporate thisfeature into SLe , yielding a more expressive decidable string logic.
Heuristics and string solver implementation: In §Introduction,
we have mentioned the large amount of works in the past sevenyears or so towards developing practical string solvers (e.g. [7, 8,
16, 22, 24, 29–32, 35, 36, 39, 44, 48, 53, 55, 57, 65–69, 71–76]).
We are not aware of existing string solvers that support both concatenations and finite-state transductions. However, string solvers
that support concatenations and the replace-all operator (i.e. asubset of finite-state transductions) are available, e.g., [16, 65, 75].
Since the focus of our work is on the fundamental issue of decidability, we consider our work to be complementary to these works.
In fact, our results may be construed as providing some completeness guarantee for existing string solvers. Practical string solvers
do not implement Makanin’s or Plandowski’s algorithms, but instead rely on certain heuristics (e.g. bounding the maximum length
k of solutions [16, 39, 57]). For this reason, none of the above
solvers have a completeness guarantee for the entire class of word
equations. However, when the input string constraint φ falls within
the logic SLe , the bounded model properties of SL and SLe (e.g.
Theorem 6 and Theorem 12) imply that string solvers need onlyp(|φ|)
look for solutions of size at most 22
for some polynomial
p(x). Double exponential size is of course only an extremely crude
estimate, so in practice one could devise an algorithm for computp(|φ|)
ing a better estimate f (φ) ≤ 22
by looking at the structureof the formula φ. A rough estimate of f (φ) could, for example, beobtained by first computing the dimension of φ (which could becomputed quickly); as we have seen in Theorem 11, when the di-mension is small the double exponential bound actually reduces toexponential size.
Future Work 1. Give a better algorithm for computing a better
estimate f (φ) of the maximum size of the solutions for straightline formulas φ that need to be explored.
Veanes et al. (e.g. see [24, 34, 36, 66]) have observed that, inpractice, the number of transitions of finite-state transducers for encoding web sanitisation functions could become large fairly quickly(due to large alphabet size, e.g., utf-8). For this reason, they introduce extensions of finite-state transducers that allow succinct representations by allowing transitions to take an arbitrary formula ina decidable logical theory, while taking advantage of state-of-theart SMT solvers for the theory. As a simple example, consider thefinite-state transducer that converts a sequence of digits (over thealphabet Σ = {0, . . . , 9}) to its HTML character numbers (overthe alphabet Σ′ = {&, ;, #, 0, 9}). The general formula for this isthat a digit i is converted to &#(48+i);. Using the standard finitestate transducers, we would require about 2 + 10 × 3 = 32 states,
whereas representing using symbolic finite-state transducers only
∼ 4 states and ∼ 4 transitions are required. There are real-world
examples where this compression would be enormous (e.g. see theencoding of HTMLdecode in [66] as a symbolic transducer). For
this reason, for future work, it would make sense to consider an extension of our work that uses symbolic finite-state transducers (orextensions thereof) both from practical and theoretical viewpoints.
Future Work 2. Study the extension of SL and SLe with symbolic(finite-state) transducers.
In order to be able to apply string solvers to analyse injection and XSS vulnerabilities, it is paramount to develop realistic
browser models, which would model implicit browser transductions. Preliminary works in this direction are available (e.g. see[58, 70]). We believe that an interesting (but perhaps extremely
challenging) line of future work is to develop a formal and precise browser transductions and their transductions (e.g. for a particular version of Firefox) as finite-state transducers (or extensions
thereof). Although some such transducers are already available(e.g. see [1, 24, 36, 66]), much work remains to be done to develop full-fledged browser models that can capture all the subtletyof browser behaviors (e.g. those that can be found in [6, 33]).
Benchmarking examples: In this paper, we have provided four
examples of analysis of mutation-based XSS vulnerabilities thatcan be expressed in SL. A few other interesting XSS vulnerability examples from [33, 62] and [6] can actually be expressed in
our logic, though the vulnerabilities only exist in older browsers(e.g. IE8). We also note that the five benchmarking examples of
PHP programs from [72] that exhibit SQL injection and XSS vulnerabilities (cf. http://www.cs.ucsb.edu/~vlab/stranger/)can also be expressed in SL. As we have argued in §Introduction,
the benchmarking examples from Kaluza [57] are in solved forms,
and therefore expressible in SLe . To the best of our knowledge, thebenchmarking examples from [72] and [57] do not contain mutation XSS test cases.

Acknowledgments
We thank Leonid Libkin and anonymous referees for their helpful feedback. We also thank Lukas Holik and Joxan Jaffar for
the fruitful discussion. Lin was supported by Yale-NUS College
through the MoE Tier-1 grants R–607–265–056–121 and IG15–
LR001. Barceló is funded by the Millenium Nucleus Center for
Semantic Web Research under grant NC120004.

References[1] BEK website (referred in Nov 2015). http://research.
microsoft.com/en-us/projects/bek/.
[2] OWASP XSS cheat sheet (referred in Nov 2015). https://www.owasp.org/index.php/XSS_(Cross_Site_Scripting)_Prevention_Cheat_Sheet.
[3] SAT competition (referred in Nov 2015). http://www.
satcompetition.org/.
[4] SMT competition (referred in Nov 2015). http://www.smtcomp.
org/.
[5] Google Closure Library (referred in Nov 2015). https://developers.google.com/closure/library/.
[6] HTML5 Security cheat sheet (referred in Nov 2015). http://
html5sec.org/.
[7] 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, pages
150–166, 2014.
[8] D. Balzarotti, M. Cova, V. Felmetsger, N. Jovanovic, E. Kirda,
C. Kruegel, and G. Vigna. Saner: Composing static and dynamic
analysis to validate sanitization in web applications. In S&P, pages
387–401, 2008.
[9] P. Barceló, L. Libkin, A. W. Lin, and P. T. Wood. Expressive languages
for path queries over graph-structured data. ACM Trans. Database
Syst., 37(4):31, 2012.
[10] P. Barceló, D. Figueira, and L. Libkin. Graph logics with rational
relations. Logical Methods in Computer Science, 9(3), 2013. .
[11] C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability
modulo theories. In Biere et al. [15], pages 825–885. .
[12] W. Bekker and V. Goranko. Symbolic model checking of tense logics
on rational Kripke models. In Infinity in Logic and Computation, International Conference, ILC 2007, Cape Town, South Africa, November
3-5, 2007, Revised Selected Papers, pages 2–20, 2007. .
[13] W. Bekker and V. Goranko. Symbolic model checking of tense logics
on rational Kripke models. CoRR, abs/0810.5516, 2008.

and its Applications, chapter 12, pages 387–442. Cambridge University Press, 2002.
[27] V. D’Silva, D. Kroening, and G. Weissenbacher. A survey of automated techniques for formal software verification. IEEE Trans. on
CAD of Integrated Circuits and Systems, 27(7):1165–1178, 2008.
[28] 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.
[29] X. Fu and C. Li. Modeling regular replacement for string constraint
solving. In NFM, pages 67–76, 2010.
[30] X. Fu, M. C. Powell, M. Bantegui, and C. Li. Simple linear string
constraints. Formal Asp. Comput., 25(6):847–891, 2013.
[31] V. Ganesh, M. Minnes, A. Solar-Lezama, and M. Rinard. Word
equations with length constraints: whats decidable? In Hardware andSoftware: Verification and Testing, pages 209–226. Springer, 2013.
[32] C. Gould, Z. Su, and P. T. Devanbu. Static checking of dynamicallygenerated queries in database applications. In ICSE, pages 645–654,
2004.
[33] M. Heiderich, J. Schwenk, T. Frosch, J. Magazinius, and E. Z. Yang.
mxss attacks: attacking well-secured web-applications by using innerhtml mutations. In CCS, pages 777–788, 2013.
[34] P. Hooimeijer and M. Veanes. An evaluation of automata algorithms
for string analysis. In VMCAI, pages 248–262, 2011.
[35] P. Hooimeijer and W. Weimer. StrSolve: solving string constraints
lazily. Autom. Softw. Eng., 19(4):531–559, 2012.
[36] P. Hooimeijer, B. Livshits, D. Molnar, P. Saxena, and M. Veanes.
Fast and precise sanitizer analysis with BEK. In USENIX Security
Symposium, 2011. URL http://static.usenix.org/events/
sec11/tech/full_papers/Hooimeijer.pdf.
[37] O. H. Ibarra. Reversal-bounded multicounter machines and theirdecision problems. J. ACM, 25(1):116–133, 1978.
[38] C. Kern. Securing the tangled web. Commun. ACM, 57(9):38–47,
Sept. 2014.

[14] J. Berstel. Transductions and Context-Free Languages. TeubnerVerlag, 1979.

[39] A. Kiezun et al. HAMPI: A solver for word equations over strings,
regular expressions, and context-free grammars. ACM Trans. Softw.
Eng. Methodol., 21(4):25, 2012.

[15] A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbookof Satisfiability, volume 185 of Frontiers in Artificial Intelligence andApplications, 2009. IOS Press.

[40] N. Klarlund, A. Møller, and M. I. Schwartzbach. MONA implementation secrets. International Journal of Foundations of Computer Science, 13(04):571–586, 2002.

[16] N. Bjørner, N. Tillmann, and A. Voronkov. Path feasibility analysis
for string-manipulating programs. In TACAS, pages 307–321, 2009.

[41] E. Kopczynski and A. W. To. Parikh images of grammars: Complexity
and applications. In LICS, 2010.

[17] A. Blumensath and E. Grädel. Automatic structures. In LICS, pages
51–62, 2000. .

[42] D. Kozen. Lower bounds for natural proof systems. In FOCS, pages
254–266, 1977.

[18] A. Blumensath and E. Grädel. Finite Presentations of Infinite Structures: Automata and Interpretations. Theory Comput. Syst., 37(6):641–
674, 2004.

[43] D. Kroening and O. Strichman. Decision Procedures. Springer, 2008.

[19] E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic, Springer, 1997.
[20] J. R. Büchi and S. Senger. Definability in the existential theoryof concatenation and undecidable extensions of this theory. In The
Collected Works of J. Richard Büchi, pages 671–683. Springer, 1990.
[21] O. Carton, C. Choffrut, and S. Grigorieff. Decision problems among
the main subfamilies of rational relations. ITA, 40(2):255–275, 2006.
[22] A. S. Christensen, A. Møller, and M. I. Schwartzbach. Precise analysisof string expressions. In SAS, pages 1–18, 2003.
[23] T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction
to Algorithms, Third Edition. The MIT Press, 3rd edition, 2009. ISBN
0262033844, 9780262033848.

[44] 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, pages 646–662, 2014.
[45] G. S. Makanin. The problem of solvability of equations in a freesemigroup. Sbornik: Mathematics, 32(2):129–198, 1977.
[46] S. Malik and L. Zhang. Boolean satisfiability from theoretical hardness to practical success. Commun. ACM, 52(8):76–82, 2009.
[47] K. L. McMillan. Symbolic model checking. Kluwer, 1993.
[48] Y. Minamide. Static approximation of dynamically generated web
pages. In WWW, pages 432–441, 2005.
[49] C. Morvan. On rational graphs. In FoSSaCS, pages 252–266, 2000.
[50] W. Plandowski. Satisfiability of word equations with constants is in
PSPACE. In FOCS, pages 495–500, 1999.

[24] L. D’Antoni and M. Veanes. Static analysis of string encoders anddecoders. In VMCAI, pages 209–228, 2013.

[51] W. Plandowski. Satisfiability of word equations with constants is in
PSPACE. J. ACM, 51(3):483–496, 2004.

[25] L. De Moura and N. Bjørner. Satisfiability modulo theories: introduction and applications. Commun. ACM, 54(9):69–77, 2011.
[26] V. Diekert. Makanin’s Algorithm. In M. Lothaire, editor, Algebraic
Combinatorics on Words, volume 90 of Encyclopedia of Mathematics[52] W. Plandowski. An efficient algorithm for solving word equations. In
STOC, pages 467–476, 2006.
[53] G. Redelinghuys, W. Visser, and J. Geldenhuys. Symbolic executionof programs with strings. In SAICSIT, pages 139–148, 2012.

[54] J. Sakarovitch. Elements of automata theory. Cambridge University
Press, 2009.
[55] Y. Sakuma, Y. Minamide, and A. Voronkov. Translating regularexpression matching into transducers. J. Applied Logic, 10(1):32–51,
2012.
[56] W. J. Savitch. Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci., 4(2):177–192, 1970.
[57] P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song.
A symbolic execution framework for javascript. In S&P, pages 513–
528, 2010.
[58] P. Saxena, D. Molnar, and B. Livshits. SCRIPTGARD: automatic
context-sensitive sanitization for large-scale legacy web applications.
In CCS, pages 601–614, 2011.
[59] B. Scarpellini. Complexity of subcases of presburger arithmetic.
Trans. of AMS, 284(1):203–218, 1984.
[60] S. Schwoon. Model-Checking Pushdown Systems. PhD thesis, Technischen Universität München, 2002.
[61] M. Sipser. Introduction to the Theory of Computation. PWS Publishing Company, 1997.
[62] B. Stock, S. Lekies, T. Mueller, P. Spiegel, and M. Johns. Precise client-side protection against dom-based cross-site scripting. In
USENIX Security, pages 655–670, 2014.
[63] A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches. PhD thesis, LFCS, School of Informatics, Universityof Edinburgh, 2010.
[64] A. W. To and L. Libkin. Algorithmic metatheorems for decidable LTL
model checking over infinite systems. In FOSSACS, 2010.
[65] M. Trinh, D. Chu, and J. Jaffar. S3: A symbolic string solver forvulnerability detection in web applications. In CCS, pages 1232–1243,
2014.
[66] M. Veanes, P. Hooimeijer, B. Livshits, D. Molnar, and N. Bjørner.
Symbolic finite state transducers: algorithms and applications. In
POPL, pages 137–150, 2012.
[67] G. Wassermann and Z. Su. Sound and precise analysis of web applications for injection vulnerabilities. In PLDI, pages 32–41, 2007.
[68] G. Wassermann and Z. Su. Static detection of cross-site scripting
vulnerabilities. In ICSE, pages 171–180, 2008.
[69] G. Wassermann, D. Yu, A. Chander, D. Dhurjati, H. Inamura, andZ. Su. Dynamic test input generation for web applications. In ISSTA,
pages 249–260, 2008.
[70] J. Weinberger, P. Saxena, D. Akhawe, M. Finifter, E. C. R. Shin, andD. Song. A systematic analysis of XSS sanitization in web application
frameworks. In ESORICS, pages 150–171, 2011.
[71] F. Yu, T. Bultan, and O. H. Ibarra. Symbolic string verification:
Combining string analysis and size analysis. In TACAS, pages 322–
336, 2009.
[72] F. Yu, M. Alkhalaf, and T. Bultan. Stranger: An automata-based string
analysis tool for PHP. In TACAS, pages 154–157, 2010. Benchmark
can be found at http://www.cs.ucsb.edu/~vlab/stranger/.
[73] F. Yu, M. Alkhalaf, and T. Bultan. Patching vulnerabilities withsanitization synthesis. In ICSE, pages 251–260, 2011.
[74] F. Yu, T. Bultan, and O. H. Ibarra. Relational string verification using
multi-track automata. Int. J. Found. Comput. Sci., 22(8):1909–1924,2011.
[75] F. Yu, M. Alkhalaf, T. Bultan, and O. H. Ibarra. Automata-based
symbolic string analysis for vulnerability detection. Formal Methods
in System Design, 44(1):44–70, 2014.
[76] Y. Zheng, X. Zhang, and V. Ganesh. Z3-str: a Z3-based string solver
for web application analysis. In ESEC/SIGSOFT FSE, pages 114–124,
2013.

Appendix
Proof of Proposition 3:
We use a reduction from PCP. Recall that an input to PCP are two
equally long lists a1 , a2 , . . . , an and b1 , b2 , . . . , bn of words overalphabet Σ. We want to decide whether there exists a solution forthis input, i.e., a nonempty sequence of indices i1 , i2 , . . . , ik suchthat 1 ≤ ij ≤ n (1 ≤ j ≤ k) and ai1 ai2 · · · aik = bi1 bi2 · · · bik .
Before explaining how our reduction works, we introduce somenotation. Assume without loss of generality that Σ is disjoint from
N. With every input a1 , a2 , . . . , an and b1 , b2 , . . . , bn for PCP overalphabet Σ, we define an alphabet Σ(n) := Σ ∪ {1, 2, . . . , n}. We
also define regular expressions
Li over Σ(n), for 1 ≤ i ≤ 6, as∪
follows: (1) L1 := ( 1≤i≤n ai · i)+ , (2) L2 = L3 = L5 =∪Σ(n)+ , (3) L4 := ( 1≤j≤n bj · j)+ , and (4) L6 = ϵ.
Further, define A = C = {1, . . . , n} and B = D = Σ. Thus, if
w is a word over Σ(n) it is the case that replace-all(w, ϵ/A) =replace-all(w, ϵ/C) corresponds to the word obtained from w
by deleting every symbol from {1, . . . , n}. On the other hand,replace-all(w, ϵ/B) = replace-all(w, ϵ/D) corresponds tothe string obtained from w by deleting every symbol from Σ.
We now explain our reduction. Consider an input to PCP given
by lists a1 , a2 , . . . , an and b1 , b2 , . . . , bn of words over Σ. We thenconstruct a string constraint φ as follows:
x2
x3
x2
x3
x4

=
=
=
=
=

replace-all(x1 , ϵ/A) ∧replace-all(x1 , ϵ/B) ∧replace-all(x4 , ϵ/C) ∧replace-all(x5 , ϵ/D) ∧x6 .x5 ∧6∧xi ∈ Li ,

(2)

i=1

where A, B, C, D are the subsets of Σ(n) defined above, andcorrespondingly for the regular expressions L1 , . . . , L6 . Clearly,
φ is of the form required by the statement of the proposition.
Assume first that the constraint φ is satisfiable via some mapping σ : {xΣ(n)∗ . Then σ(x1 ) is a word in the∪1 , . . . , x6 } →+language ( 1≤i≤n ai · i) and σ(x4 ) is a word in the language∪( 1≤j≤n bj · j)+ . Furthermore, σ(x4 ) = σ(x5 ) due to the factthat σ(x4 ) = σ(x6 ).σ(x5 ) and σ(x6 ) is the empty word (sinceσ(x6 ) belongs to L6 = ϵ).
Assume that σ(x1 ) = ai1 i1 · · · aik ik , where 1 ≤ iℓ ≤ n foreach 1 ≤ ℓ ≤ k, and σ(x4 ) = bj1 j1 · · · bjp jp , where 1 ≤ jℓ ≤ n
for each 1 ≤ ℓ ≤ p. Sinceσ(x2 )===

replace-all(σ(x1 ), ϵ/A)
replace-all(σ(x4 ), ϵ/C)
replace-all(σ(x4 ), ϵ/A),

it is the case that ai1 · · · aik = bj1 · · · bjp . Similarly, sinceσ(x3 )====

replace-all(σ(x1 ), ϵ/B)
replace-all(σ(x5 ), ϵ/D)
replace-all(σ(x4 ), ϵ/D)
replace-all(σ(x4 ), ϵ/B),

we have that i1 · · · ik = j1 · · · jp . We conclude that i1 , . . . , ik is asolution for the PCP instance defined by a1 , . . . , an and b1 , . . . , bn .
Assume on the other hand that i1 , . . . , ik is a solution for this
PCP instance. Then it is easy to check that the constraint φ defined
above is satisfiable via the mapping σ : {x1 , . . . , x6 } → Σ(n)∗which is defined as follows: (1) σ(x1 ) = ai1 i1 · · · aik ik , (2)σ(x2 ) = ai1 · · · aik = bi1 · · · bik , (3) σ(x3 ) = i1 · · · ik , (4)σ(x4 ) = σ(x5 ) = bi1 i1 · · · bik ik , and (5) σ(x6 ) = ϵ.
Another Mutation XSS example:
Example 6. This example is an adaptation of [62, Listing 7].
[The original example no longer works on modern browsers.] This
example has the same spirit as Example 5. Consider the following
JavaScript.
var title = document.getElementById("node1");
var x = document.getElementById("node");z = goog.string.escapeString(z); // sanitise
title.innerHTML = z;var name="blah";var code = '<iframe id="' + title.innerHTML + '"';
code += ' name="' + name +'"';
code += 'src="http://www.w3schools.com"></iframe>';x.innerHTML = code;

The HTML file contains the following two lines:<div id="node1" style="font-size: h1">Title</div><div id="node">iFrame to add</div>

The purpose of the JavaScript is to add a user-specified title(specified in the variable z) to the page, and modifies the id attribute of the iframe element accordingly. Since the variable z
is untrusted, it is first sanitised before use. Consider the value&#34; onload=&#34;alert(1) of the variable z. In this case,it would remain unmodified by escapeString and is decoded
into " onload="alert(1) by innerHTML mutation. The browser
would execute the code alert(1), which was unintended by thedeveloper.
To analyse such a vulnerability within SL, we need to analyse
whether x.innerHTML could take any string value of the form:
e2 = /<iframe id="("|[^"]*[^"\\]")[a-zA-Z][a-zA-Z0-9]*="("|[^"]*[^"\\]")
name="("|[^"]*[^"\\]")
src="http:\/\/www.w3schools.com"><\/iframe>/

The regular expression essentially implies that the constructed
string has an extra attribute. [The reader could use https://
regex101.com/ to experiment.] Notice that the above script is
not a stright-line program. To this end, we first convert it into thestatic-single assignment form in the standard way:
var title = document.getElementById("node1");
var x = document.getElementById("node");newz = goog.string.escapeString(z); // sanitise
title.innerHTML = newz;
var name="blah";var code = '<iframe id="' + title.innerHTML + '"';
code1 = code + ' name="' + name +'"';
code2 = code1+'src="http://www.w3schools.com"></iframe>';x.innerHTML = code2;

Analysis against the attack pattern e2 can then be expressed in SL
as a conjunction of the following constraints:• newz = R2 (z)• title.innerHTML = R3 (newz)• name = newz
• code = w1 · title.innerHTML · w2
• code1 = code · w3 · name · w4
• code2 = code1 · w4
• x.innerHTML = R3 (code2)• x.innerHTML matches e2

Here R2 is the transducer implementing escapeString, while
R3 is a transducer implementing the implicit browser transductions upon innerHTML assignments. Observe that the resulting constraint is in SL.
Proof of Lemma 8:
The proof of Lemma 8 is by induction on the position of y in the
topological sort ≺ of G(φ).
Base cases: A source node y in G(φ). In which case, byconstruction the formula φ′y is exactly the same formula as φy
except that the variable y is replaced by y(1). (In particular,
φy = {P (y)}, for P a regular language, and therefore φ′y ={P (y(1))}). So, the claim holds.
First inductive case: A non-source node y, where y = y1 . . . yn
is the relational constraint witnessing the incoming edge to y and
P (y) is the regular constraint for y. In this case, let z be the immediate predecessor of y in the topological sort ≺. Among others,
observe that y1 , . . . , yn ⪯ z. To prove the desired claim for y, we
will now apply the induction hypothesis on z.
In one direction, if ι : Zy → Σ∗ is a satisfying assignment for
φy , then the restriction ι|Zz of ι to Zz is a satisfying assignmentfor φz (since φy = φz ∧ y = y1 . . . yn ∧ P (y)). By induction then,there exists a satisfying assignment ι′ : Zz′ → Σ∗ for φ′z such that
ι|Zz (u) = ι′ (u(1)) ◦ · · · ◦ ι′ (u(maxu ))for each u ∈ Zz . Therefore:
ι(y) = ι(y1 ) . . . ι(yn ) =ι′ (y1 (1)) . . . ι′ (y1 (maxy1 )) . . . ι′ (yn (1) . . . ι′ (yn (maxyn )).
For each k ∈ {1, . . . , maxy } and integers i, l satisfying ν(k) =(i, l), the formula φ′y contains the constraint y(k) = yi (l), andso we will simply extend the assignment ι′ : Zz′ → Σ∗ to Zy′
by setting ι′ (y(k)) := ι′ (yi (l)). This shows that ι(u) = ι′ (u(1)) ◦· · ·◦ι′ (u(maxu )) for each u ∈ Zy . It also shows that ι′ : Zy′ → Σ∗satisfies λrel (y). In addition, if π is an accepting run of P on ι(y),then we may split π into maxy segments π1 , . . . , πmaxy , where theinitial (resp. final) state of each πi is a state qi−1 (resp. qi ), suchthat the run πi is also an accepting run of P[qi−1 ,qi ] on ι′ (y(i)).
∧maxThis shows that ι′ : Zy′ → Σ∗ satisfies i=1 y P[qi−1 ,qi ] (y(i)) forsome maxy -splitting q0 , . . . , qmaxy of P , and hence that it satisfies
λreg (y). We conlude then that ι′ : Zy′ → Σ∗ satisfies φ′y .
The converse case can be proven by noticing that the chain ofreasoning in the previous paragraph can be reversed.
Second inductive case: A non-source node y, where R(x, y)is the string constraint witnessing the incoming edge to y and
P (y) is the regular constraint for y. Again, let z be the immediate
predecessor of y in the topological sort ≺. Thus, x ⪯ z. To provethe desired claim for y, we apply the induction hypothesis on z.
In one direction, assume ι : Zy → Σ∗ is a satisfying assignmentfor φy . As in the previous case, we can conclude by induction
hypothesis that there exists a satisfying assignment ι′ : Zz′ → Σ∗for φ′z such that
ι|Zz (u) = ι′ (u(1)) ◦ · · · ◦ ι′ (u(maxu ))for each u ∈ Zz (and, in particular, for u = x). Since ι is asatisfying assignment for φy , it also follows that there exists arun π of R witnessing (ι(x), ι(y)) ∈ R. We may split this run
π into maxx segments π1 , . . . , πmaxx , where the initial (resp. final) state of πi is some state pi−1 (resp. pi ), such that for some
w1 , . . . , wn ∈ Σ∗ such that ι(y) = w1 . . . wn , the run πi witnesses that (ι′ (xi ), wi ) ∈ R[pi−1 ,pi ] . (Note that there might bemore than one way to split π and ι(y) while satisfying the aforea/bb

ϵ/amentioned condition, e.g., if π1 = p0 −→ p1 −→ p2 and

b/ab

a/bb

π2 = p2 −→ p3 , then the splitting π1′ = p0 −→ p1 and
ϵ/a

b/ab

π2′ = p1 −→ p2 −→ p3 will also satisfy the aforementioned
condition). We will simply extend the assignment ι′ to Zy′ by setting ι′ (y(k)) = wk for each k ∈ {1, . . . , maxx }. Clearly then,′ι(u) = ι′ (u(1)) ◦ · · · ◦(u(maxu )) for each u ∈ Zy . Also,∧ιmax′
by definition ι satisfies i=1 y y(i) = R[pi−1 ,pi ] (x(i)) for somemaxy -splitting p0 , . . . , pmaxy of R, and hence it satisfies λrel (y).
Now, let π be an accepting run of of P on ι(y) = w1 . . . wn . As in
the first inductive case, we take the segment πi of π that operates
on wi . If pi−1 (resp. pi ) is theinitial (resp. final) state in the run∧max
segment πi , then ι′ satisfies i=1 y P[pi−1 ,pi ] (y(i)). This showsthat ι′ satisfies λrel (y). We conclude that ι′ satisfies φ′y .
As in the first inductive case, the converse case can be provenby noticing that the chain of reasoning in the previous paragraphcan be reversed.
Proof of the lower bound of Theorem 5:
We prove that checking satisfiability of string constraints in SL
is EXPSPACE-hard. We reduce from the acceptance problem fora deterministic Turing machine M that works in space 2cn , forc > 1. That is, we provide a polynomial time reduction that, given
an input w to M, it constructs a constraint φ(w) in SL such that w
is accepted by M if and only if φ(w) is satisfiable.
Let us assume that M = (Σ, Q, q0 , qf , δ), where (i) Σ is a finite
alphabet which contains the blank symbol ♭, (ii) Q is the finite setof states, (iii) q0 is the initial state, (iv) F is the set of final states,and (v) δ : Q × Σ → Q × Σ × {−1, 0, 1} is the transition function.
We assume without loss of generality that (a) Σ ∩ {0, 1} = ∅, (b)F = {qf } is a singleton, and (c) before accepting the machineerases its tape leaving the head in the first position.
We define Σ(Q) := Σ ∪ (Σ × Q) ∪ {0, 1}. We use this alphabet
to represent configurations of M. Consider, for instance, that M
is in a configuration c in which the i-th cell of the tape contains
symbol ai ∈ Σ, for each 0 ≤ i ≤ 2cn − 1, the head is scanningcell 0 ≤ j ≤ 2cn − 1, and the machine is in state q ∈ Q. Then c isrepresented as the following word over Σ(Q):[0] a0 [1] a1 [2] · · · [j] (aj , q) [j + 1] . . . [2cn

− 1]a2cn −1 ,where for each 0 ≤ i ≤ 2 − 1 we have that [i] is the cn-bit
representation of the integer i over alphabet {0, 1}.
Let w be an input to M (i.e., a word over Σ) of length n ≥0. We now explain how to ∧construct φ(w). To start with, φ(w)contains a regular constraint 1≤i≤m Li (x) such that L1 (x)∧· · ·∧Lm (x) is satisfiable by a word x if and only the following holds:cn

1. The word x satisfies the regular expression:()∗[0] Σ(Q) [1] Σ(Q) [2] · · · [2cn − 1] Σ(Q) $ .

that satisfy the conditions specified above can be constructed inpolynomial time from M and w.
The intuitive idea of the reduction is to codify in the word x an
accepting run of M on input w. Let us assume that x is of the form
c0 $c! $ · · · $cp $, for p ≥ 0, where for each 0 ≤ i ≤ p we have thatci encodes a cn-bit counter. We know that c0 and cp represent an
initial and final configuration, respectively, of M on input w. Thus,in order to check that x in fact represents an accepting run of M
on w we only need to verify that for each 0 ≤ j ≤ p − 1 it is thecase that cj+1 encodes the configuration which is obtained from cj
by one application of the transition function δ.
As usual, we check this locally for each block of three consecutive addresses in the cj ’s. Formally, for each 0 ≤ i ≤ 2cn − 1
and 0 ≤ j ≤ p, we define cj [i] to be the unique substring of cj of
the form [i]a, for a ∈ Σ(Q). Clearly then, checking whether theword x = c0 $c1 $ · · · $cp $ codifies an accepting run of M on input
w is equivalent to checking that for each 1 ≤ i ≤ 2cn − 2 and0 ≤ j < p the block cj+1 [i − 1]cj+1 [i]cj+1 [i + 1] follows fromcj [i − 1]cj [i]cj [i + 1] according to the transition function δ. For
instance, if
cj [i − 1]cj [i]cj [i + 1] = [i − 1] a [i] (b, q) [i + 1] c,
where a, b, c ∈ Σ and q ∈ Q, and δ(q, b) = (q ′ , b′ , −1), thencj+1 [i − 1]cj+1 [i]cj+1 [i + 1] = [i − 1] (a, q ′ ) [i] b′ [i + 1] c.
This is precisely the role of the remaining constraints in φ(w),which we define next.
First, we add to the constraint φ(w) the string constrainty = x#x#x#x#x#xthat takes six copies of the word x, separates them with a newdelimiter #, and assigns the result to the variable y. We then apply
a transducer R to y to define a new variable z. Let us recall thatx is of the form c0 $c1 $ . . . $cp $, where each ci encodes a cn-bit
counter. The transducer R then converts y = x#x#x#x#x#x
into z = x1 #x2 #x3 #x4 #x5 #x6 , where:
1. x1 is exactly as x except that now we have replaced eachcounter cj with a new counter c1j that only preserves from cj
information about addresses [0], [1], [2], [6], [7], [8], . . .
2. Same for x2 and cj2 , but now cj2 preserves information about
addresses [1], [2], [3], [7], [8], [9], . . .
3. Same for x3 and cj3 , but now cj3 preserves information about
addresses [2], [3], [4], [8], [9], [10], . . .
4. Same for x4 and cj4 , but now cj4 preserves information about
addresses [3], [4], [5], [9], [10], [11], . . .
5. Same for x5 and cj5 , but now cj5 preserves information about
addresses [4], [5], [6], [10], [11], [12], . . .

In other words, x represents the concatenation of several cn-bit
counters separated by the delimiter $. Each address [i] in one ofthese bit couters is followed by a symbol from Σ(Q).

6. Same for x6 and cj6 , but now cj6 preserves information about
addresses [5], [6], [7], [11], [12], [13], . . .

2. The first counter in x encodes the initial configuration of M
with input w. That is, if w = a0 a1 · · · an−1 then the following
word is a prefix of x:

We also assume that transducer R deletes from each counter clj inul (0 ≤ j ≤ p and 1 ≤ l ≤ 6) the “incomplete” blocks before adelimiter $, i.e., the suffixes that do not form a complete block of
three consecutive addresses. (For instance, if 2cn = 8 then each c2j
is of the form [1]a[2]b[3]c[7]d. In this case, R simply deletes thesuffix [7]d completely).
Notice that each block of three consecutive addresses appears
in one, and only one, of the words xl , for 1 ≤ l ≤ 6. In particular,
the information from x about addresses [i − 1], [i], [i + 1], for1 ≤ i ≤ 2cn − 2, is preserved in xj , where j is the remainder
obtained by dividing i by 6 (assuming that if i is divisible by 6 thenthis remainder is 6). Further, it is not hard to see how the transducer
R can be constructed in polynomial time from our input.

[0] (a0 , q0 ) [1] a1 · · · [n − 1] an−1 [n] ♭ · · · [2cn − 1] ♭ $Recall that q0 is the initial state of M and ♭ is the blank symbol.
3. The last counter of x encodes a final configuration of M. Thatis, the following word is a suffix of x:[0] (♭, qf ) [1] ♭ [2] ♭ · · · [2cn − 1] ♭.
Using standard ideas on how to enconde n-bit counters (see, e.g.,[19, 42]), it is possible to show that a set {L1 , . . . , Lm } of NFAs

We now extend the formula φ(w) by including the conjunctionof the following atomic string constraints:
ui = zi−1 #i zi−1
zi = Si (ui−1 )(1 ≤ i ≤ cn − 1)
(1 ≤ i ≤ cn),

where z0 = z, the symbol #i is a fresh delimiter, and Si is atransducer we define below. That is, ui consists of two copies ofzi−1 separated by the delimiter #i and zi is obtained from ui−1 byapplying the transducer Si . We stop this process after cn steps.
For the sake of readability, we will keep the explanation at
the intuitive level. We start by explaining how the transducer S1
is defined. By definition, u1 = z0 #1 z0 = z#1 z and z =x1 #x2 #x3 #x4 #x5 #x6 . Then S1 takes the the copy of xl =cl0 $ . . . $clp , for 1 ≤ l ≤ 6, that appears before the delimiter #1
in u1 , and turns it into a new word x′l = dl0 $ . . . $dlp , where eachdlj is obtained by performing the following modifications over clj :If clj consists only of a block of three consecutive addresses, thenleave as it is (i.e., dlj = clj ); otherwise, remove every other block of
three consecutive addresses from clj . For the copy of xl that occurs
after #1 , the transducer S1 transforms it into a new word x′′l by
doing the opposite: If clj contains more than one block of threeconsecutive addresses, then it removes the first block, keeps thesecond one, removes the third one, etc. It is not hard to see that S1
can be constructed in polynomial time from our input.
Notice then thatz1 = x′1 #x′2 #x′3 #x′4 #x′5 #x′6 #1 x′′1 #x′′2 #x′′3 #x′′4 #x′′5 #x′′6 ,where, for instance, x′1 corresponds to the restriction of x toaddresses [0], [1], [2], [12], [13], [14], . . . , while x′′1 corresponds
to the restriction of x to [6], [7], [8], [18], [19], [20], . . . . In thesame way, x′2 corresponds to the restriction of x to addresses[1], [2], [3], [13], [14], [15], . . . , while x′′2 corresponds to the restriction of x to addresses [7], [8], [9], [19], [20], [21], . . . . In general, the restriction of x to addresses [i − 1], [i], [i + 1], for1 ≤ i ≤ 2cn − 2, is contained in (i) x′j if and only if the remainder of i divided by 12 is 1 ≤ j ≤ 6, and in (ii) x′j if and only
if the remainder of i divided by 12 is j + 6, for 1 ≤ j ≤ 6.
In general, we will assume inductively that zl , for 1 ≤ l ≤ cn−
1, is constructed from words w1 , w2 , . . . , w6·2i over Σ(Q) ∪ {$}– suitably separated by delimiters #, #1 , . . . , #i according to thestructure provided by the constraints that define the zl ’s and ul ’s– in such a way that wj corresponds to the restriction of x toaddresses [i − 1], [i], [i + 1] (1 ≤ i ≤ 2cn − 2) for which theremainder of i divided by 6 · 2i is precisely j.
Then ul+1 = zl #l+1 zl , and we define Sl+1 similarly to S1 .
That is, Sl+1 takes the copy of wj = t0 $ . . . $tp (where each this a word over Σ(Q)) that appears before the delimiter #l+1 in
ul+1 , and turns it into a new word wj′ = t′0 $ . . . $t′p , where eacht′h is obtained by performing the following modifications over th :If th consists only of a block of three consecutive addresses, thenleave as it is (i.e., t′h = th ); otherwise, remove every other block of
three consecutive addresses from th . For the copy of wj that occurs
after #l+1 , the transducer Sl+1 transforms it into a new word wj′′
by doing the opposite: If th contains more than one block of threeconsecutive addresses, then it removes the first block, keeps thesecond one, removes the third one, etc. It is not hard to see thenthat zl+1 consists of words v1 , v2 , . . . , v6·2i+1 over Σ(Q) ∪ {$} –suitably separated by delimiters #, #1 , . . . , #l+1 according to thestructure provided by the constraints that define the zl ’s and ul ’s –in such a way that vj corresponds to the restriction of x to addresses[i − 1], [i], [i + 1] (1 ≤ i ≤ 2cn − 2) for which the remainder of idivided by 6 · 2i+1 is precisely j. This proves our inductive case.
In particular then, zcn consists of words v1 , v2 , . . . , v6·2cn overΣ(Q) ∪ {$} – suitably separated by delimiters #, #1 , . . . , #cn

according to the structure provided by the constraints that define
the zl ’s and ul ’s – in such a way that vj , for 1 ≤ j ≤ 2cn − 2,corresponds to the restriction of x to addresses [j − 1], [j], [j + 1]
(and nothing else). That is, vj is of the form
c0 [j − 1]c0 [j]c0 [j + 1]$c1 [j − 1]c1 [j]c1 [j + 1]$ · · ·$ cp [j − 1]cp [j]cp [j + 1],
Further, the vj ’s such that j > 2 − 2 also correspond to therestriction of x to addresses [i − 1], [i], [i + 1] (and nothing else),
for some 1 ≤ i ≤ 2cn − 2.
Finally, we only have to check in each subword vj (1 ≤ j ≤6 · 2cn ) of zcn of the formcn

c0 [i − 1]c0 [i]c0 [i + 1]$c1 [i − 1]c1 [i]c1 [i + 1]$ · · ·$ cp [i − 1]cp [i]cp [i + 1],
for 1 ≤ i ≤ 2 − 2, that cl+1 [i − 1]cl+1 [i]cl+1 [i + 1] is obtained
from cl [i − 1]cl [i]cl [i + 1] by applying the transition function δ, foreach 0 ≤ l < p. It is easy to see how to construct an NFA L which
verifies this for each subword vj of the form above (see, e.g., [42]).
We then add to φ(w) a regular constraint A∗ (zcn ), where A∗ is the
NFA that checks that each subword vj in zcn is accepted by A. The
NFA A∗ simply “restarts” A if A is in an acceptance state while
reading one of the delimiters #i or #; otherwise it rejects.
Clearly, φ(w) is in SL and can be constructed in polynomial
time from the input. Furthermore, M accepts w if and only if φ(w)is satisfiable. This concludes the proof.
cn