String Solving with Word Equations and Transducers: Towards a Logic for Analysing Mutation XSS
String solving (a.k.a. SMT over strings) for detecting security vulnerabilities (especially those related to SQL injections and cross-site scripting, a.k.a., XSS) in web applications has been the subject of many papers in the past 6-7 years. In this talk, we will argue that the existing string solving frameworks are not sufficient for analysing real-world XSS vulnerabilities. In particular, they do not accommodate constraints that allow both string concatenations and transducers; the latter can capture sanitisation functions (e.g. htmlescape) and implicit browser transductions (e.g. innerHTML). Unfortunately, naively combining concatenations and transducers easily results in undecidability. In this talk, we will present a fragment of the string logic, called the straight-line fragment, that allows both concatenations and transductions, whose satisfiability problem is still decidable. We show that the fragment is sufficiently expressive in that it can encode many practical examples where XSS arise, which furthermore cannot be encoded in other string solving frameworks. We will mention a few extensions of the straight-line fragment (e.g. adding length constraints, and disequality) that preserve decidability. A number of future challenges will be mentioned at the end of the talk.
The talk is based on my recent POPL'16 paper (joint with Pablo Barcelo).
Dr. Anthony Lin is an assistant professor in computer science at Yale-NUS College. He completed his PhD at Edinburgh's University School of Informatics under Prof. Leonid Libkin and Dr. Richard Mayr. Previously, he was an EPSRC Postdoctoral Research Fellow at University of Oxford (2010-2013). His current research focuses on constraint solving, program analysis, and formal verification with applications to web security, web performance optimisation, and analysis of concurrent systems with many processes.