Anthony Widjaja Lin

Date: 10:00, Wednesday, November 22, 2017
Speaker: Anthony Widjaja Lin
Venue: Zemanek, Favoritenstrasse 9-11, 1040 Wien

Symbolic executions (and their recent variants called dynamic symbolic
executions) are an important technique in automated testing. Instead
of analysing only concrete executions of a program, one could treat
such executions symbolically (i.e. with some variables that are not
bound to concrete values) and use constraint solvers to determine this
(symbolic) path feasibility so as to guide the path explorations of
the system under test, which in combination with dynamic analysis
gives the best possible path coverage. For string-manipulating
programs, solvers need to be able to handle constraints over the
string domain. This gives rise to the following natural question: what
is an ideal decidable logic over strings for reasoning about path
feasibility in a program with strings? This is a question that is
connected to a number of difficult results in theoretical computer
science (decidability of the theory of strings with concatenations,
a.k.a., word equations) and long-standing open problems (e.g.
decidability of word equations with length constraints). Worse yet,
recent examples from cross-site scripting vulnerabilities suggest that
more powerful string operations (e.g. finite-state transducers) might
be required as first class citizens in string constraints. Even though
putting all these string operations in a string logic leads to
undecidability, recent results show that there might be a way to
recover decidability while retaining expressivity for applications in
symbolic execution. In this talk, I will present one such result from
my POPL’16 paper (with P. Barcelo). The string logic admits
concatenations, regular constraints, finite-state transductions,
letter-counting and length constraints (which can consequently express
charAt operator, and string disequality). I will provide a number of
examples from the cross-site scripting literature that shows how a
string logic can, for the first time, be used to discover a bug in or
prove correctness of the programs. I will conclude by commenting on a
new decision procedure for the logic that leads to an efficient
implementation (POPL’18 with L. Holik, P. Janku, P. Ruemmer, and T.
Vojnar) and a recent attempt to incorporate the fully-fledged
replace-all operator into a string logic (POPL’18 with T. Chen, Y.
Chen, M. Hague, and Z. Wu).

Posted in RiSE Seminar