String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report)

Řetězcová omezení s konkatenací a převodníky řešena efektivně (technická zpráva)

report

English

Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Janků Petr, Ing. (RG VERIFIT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Lin Anthony
Rummer Philipp

• https://arxiv.org/abs/2010.15975

string analysis, XSS, string constraints

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 (XSS). A popular string analysis technique includes symbolic
executions, which at their core use string (constraint) 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 and
finite 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). In this paper, we provide the first
string solver that can reason about constraints involving both concatenation and
finite 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. To
this end, we propose a method that exploits succinct alternating finite automata
as concise symbolic representations of string constraints. 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 XSS and other examples in the literature.

2020

1–33

Springer International Publishing

New York