String analysis is the problem of reasoning about how strings are
manipulated by a program. It has numerous applications including
automatic detection of cross-site scripting, and automatic test-case
generation. A popular string analysis technique includes symbolic
executions, which at their core use constraint solvers over the string
domain, a.k.a. string solvers. Such solvers typically reason about
constraints expressed in theories over strings with the concatenation
operator as an atomic constraint. In recent years, researchers started
to recognise the importance of incorporating the replace-all operator
(i.e. replace all occurrences of a string by another string) and, more
generally, finite-state transductions in the theories of strings with
concatenation. Such string operations are typically crucial for
reasoning about XSS vulnerabilities in web applications, especially
for modelling sanitisation functions and implicit browser
transductions (e.g. innerHTML). Although this results in an
undecidable theory in general, it was recently shown that the
straight-line fragment of the theory is decidable, and is sufficiently
expressive in practice. In this paper, we provide the first string
solver that can reason about constraints involving both concatenation
and finite-state transductions. Moreover, it has a completeness and
termination guarantee for several important fragments
(e.g. straight-line fragment). The main challenge addressed in the
paper is the prohibitive worst-case complexity of the theory
(double-exponential time), which is exponentially harder than the case
without finite-state transductions. To this end, we propose a method
that exploits succinct alternating finite-state automata as concise
symbolic representations of string constraints. In contrast to
previous approaches using nondeterministic automata, alternation
offers not only exponential savings in space when representing Boolean
combinations of transducers, but also a possibility of succinct
representation of otherwise costly combinations of transducers and
concatenation. Reasoning about the emptiness of the AFA language
requires a state-space exploration in an exponential-sized graph, for
which we use model checking algorithms (e.g. IC3). We have implemented
our algorithm and demonstrated its efficacy on benchmarks that are
derived from cross-site scripting analysis and other examples in the
literature.