The paper "String Solving with Word Equations and Transducers: Decidability and Applications" by Associate Researcher Pablo Barcelo and Anthony W. Lin, from Yale-NUS College, Singapore, has been accepted for presentation at the ACM Symposium on Principles of Programming Languages (POPL 2016). This premier symposium addresses fundamental principles and important innovations in the design, definition, analysis, and implementation of programming languages, programming systems, and programming interfaces. POPL will be held during January 2016, in St. Petersburg, Florida.
The article studies the decidability of satisfiability over string logics with concatenations and finite-state transducers as atomic operations. Although restricting to one type of operations yields decidability, little is known about the decidability of their combined theory, which is especially relevant when analysing security vulnerabilities of dynamic web pages in a more realistic browser model. On the one hand, word equations (string logic with concatenations) cannot precisely capture sanitisation functions (e.g. htmlescape) and implicit browser transductions (e.g. innerHTML mutations). On the other hand, transducers suffer from the reverse problem of being able to model sanitisation functions and browser transductions, but not string concatenations. Naively combining word equations and transducers easily leads to an undecidable logic. The main contribution of the paper is to show that the “straight-line fragment” of the logic is decidable. The fragment can express the program logics of straight-line string-manipulating programs with concatenations and transductions as atomic operations, which arise when performing bounded model checking or dynamic symbolic executions.