Decidable Logics for Path Feasibility of Programs with Strings

Add to your list(s) Download to your calendar using vCal

• Anthony Widjaja Lin (University of Oxford)
• Friday 10 November 2017, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

If you have a question about this talk, please contact Paul Taylor.

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 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 string 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 suggests that more powerful string operations (e.g. finite-state transducers) might be needed 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, for the first time, can 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).

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.