Decidable Logics for Path Feasibility of Programs with Strings
Department of Computer Science
University of Oxford
COM2 Level 4
Executive Classroom, COM2-04-02
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 (XSS) 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 DOM-based XSS literature that shows how a string logic can, for the first time, be used to discover a bug in or prove the 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).
Biodata:
Anthony W. Lin is an Associate Professor in Programming Languages at University of Oxford Department of Computer Science and an Official Fellow at Kellogg College. Prior to joining Oxford, Lin was an assistant professor in computer science at Yale-NUS College (National University of Singapore). Broadly speaking, he is interested in all aspects (ranging from theory to systems) of the development of principled techniques that can make software less error-prone and more efficient.Lin was a winner of Google Faculty Research Award (2017), EPSRC Research Fellowship (2010-2013), and LICS Kleene Award (2010). He regularly publishes, reviews, and serves on the program committee at premier conferences in the areas including CAV, CONCUR, FoSSaCS, ICALP, LICS, OOPSLA, POPL, and TACAS.
website: https://anthonywlin.github.io/