Abstract:

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).