String Solving with Word
Equations and Transducers:
Anthony W. Lin (Yale-NUS), Pablo Barcelo (Univ. of Chile)

String Solving: A View
on the LandscapeWhat are String Solvers?
Domain: the set of all words over
Operations: concatenation, regex matching, length
constraints, replace, replace-all, string transductions, ...
A different combination of operations gives rise to a different
theory over strings!! (Just as for integer domain)
Many string solvers: CVC, HAMPI, Kaluza, Kudzu, Norn,
Pex/Z3, PISA, S3, Saner, Stranger, StrSolve, SUSHI, Z3-str, ...Why Develop StringSolvers?
•

Static analysis of security vulnerabilities in web
applications against code injection and XSS•

Automatic test case generation for scriptinglanguages•

Path query languages for graph databases

String Solving: Theory vs.
Practice•

Faster heuristics each year•

Much less progress on theory
Which SMT over strings is decidable?

1. Word equations (Makanin’77)
2. Existential theory strings with concat (Buchi&Senger’90)
3. Word equations with regex matching (Schulz’90)

The need to add stringtransductions

Cross-Site Scripting (XSS)Sanitising Input Data•

Escape certain characters•

EVERY occurrence of < should be changed to &lt;

•EVERY occurrence of > should be changed to &gt;
A kind of “replace-all” operation

Adding Sanitisation
Google Closure<script>…</script>
will be converted to&lt;script&gt;…&lt;script&gt;
The script won’t be executed by Dilbert’s browser

A more tricky example(Adapted from Kern’14)

escapeString “backslash-escape” certain metacharacters‘ is replaced by &#39; or \’“ is replaced by &#34; or \”Q: Is this code vulnerable to XSS?

Analysis of the code
SWAP

INPUT 1: name being Tom & Jerry gives HTML markup<a onclick=“viewPerson(‘Tom &amp; Jerry’)”>Tom &amp; Jerry</a>

INPUT 2: name being ‘);alert(1);// gives HTML markup<a onclick=“viewPerson(‘&#39;);alert(1);//’)”>&#39;);alert(1);//‘</a>innerHTML “mutates” this string to<a onclick=“viewPerson(‘’);alert(1);//’)”>’);alert(1);//‘</a>

XSS!

Detecting XSS via a String
Solver
Step 1: Identify “sink variables” (innerHTML, document.write)

Step 2: Find “attack patterns” from known vulnerabilities (eg, OWASP)
e1 = /<a onclick="viewPerson\(' ( ' | [^']*[^'\\] ' ) \); [^']*[^'\\]' )">.*<\/a>/Step 3: Express the program logic in a string logic:
1.
2.
3.
4.
5.

x = R1(name)y = R2(x)z = w1 . y . w2 . x . w3
nameElem.innerHTML = R3(z)nameElem.innerHTML matches e1

Step 4: Check for satisfiability

Which String Logic?
1.
2.
3.
4.
5.

x = R1(name)y = R2(x)z = w1 . y . w2 . x . w3
nameElem.innerHTML = R3(z)nameElem.innerHTML matches e1

concatenation
R1, R2, R3 - replace-all kind ofoperations
String transductions!

Finite-state I/O Transducers
Just like finite-state automaton, but the transition
label is a pair of words:

Erases 1

Replaces some reserved characters
by HTML entity names

Relation recognised byisModelling sanitisation functions
and implicit browser transductions
Lots of works modelling these as FST or extensions
thereof:-Saxena et al, S&P’10
D’Antoni&Veanes, VMCAI’13
Hooimejer et al., USENIX Security’11
Veanes et al., POPL’11…

Is theory of strings withconcatenation and FSTdecidable?

Undecidability
Proposition (BFL’13): Checking if the constraint
x = y.z & x = R(z)for a transduction R, is satisfiable is undecidable

Proposition: Undecidability still holds when only
allowing “erasing” transducers (i.e. replace A with
an empty string)The Straight-Line Fragment(SSA Form)
Inductive Definition:(Base) An empty set(Inductive) If
thenwhere theof conjuncts is in SL

is in SL with variables
is in SL, where’s are variables inor new variables

regex matching: a boolean combination of

Decidability of SL
Theorem: SATISFIABILITY for the class SL is decidable
in exponential space (double-exponential-time)
In fact, EXPSPACE-complete

Theorem (Bounded Model Property):
Every satisfiable constraint in SL has a solutionof double-exponential size
Provides some completeness guarantee of several existing string solvers

Under a reasonable assumption, we get a single-exponential boundProof idea for decidability (without regexmatching)
Step 1: Remove concatenation from the formulawherehas states

Bound on the size of formula
without concatenation“Doubling” Trick
Resulting formula uses

variables

Can use this trick to encode EXPSPACE Turing machines

Solving the final formula

Acyclic (straight-line)
Satisfiability for this kind of formulas is decidable

Post/pre images of regular languages under FST are regularImproving the upper boundThe doubling tricks are artificial
Limiting them into a bounded height is reasonable in practiceAll the examples we’ve seen in practice are of height at most 4
Theorem: SATISFIABILITY for the restricted SL is decidable
in polynomial space (exponential-time)
Theorem (Bounded Model Property):
Every satisfiable constraint in restricted SL has a solutionof exponential size

Extending the logic

Adding integer constraints
Constraints of the form

whereis a constant integer
is either:1) an integer variable,2)
for some string variable3)
for some string variableDecidability
Theorem: SATISFIABILITY for the class SL with integer
constraints is decidable in exponential space
In fact, EXPSPACE-complete

Theorem (Bounded Model Property):
Every satisfiable constraint in SL with integer constraints has asolution of double-exponential size

Conclusion and Future Work•

Concatenation and string transductions are both important for
XSS applications•

Straight-line fragment of string logic with concatenation andtransductions (and even with integer constraints) is decidable•

Future work 1: an algorithm for computing a better estimateof the maximum size of solutions•

Future work 2: study the extension with symbolic transducers•

Future work 3: A more precise model of sanitisation functions
and implicit browser transductions as transducers