Write a Blog >>
Wed 20 Jan 2016 14:45 - 15:10 at Grand Bay North - Track 1: Decision Procedures Chair(s): Loris D'Antoni

We study the fundamental issue of 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. Our main contribution is to show that the straight-line fragment of the logic is decidable (complexity ranges from PSPACE to EXPSPACE). 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. We demonstrate that the logic can naturally express constraints required for analysing mutation XSS in web applications. Finally, we show that the logic remains decidable in the presence of length, letter-counting, regular, and indexOf constraints.

Wed 20 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00
Track 1: Decision ProceduresResearch Papers at Grand Bay North
Chair(s): Loris D'Antoni University of Pennsylvania
14:20
25m
Talk
Query-Guided Maximum Satisfiability
Research Papers
Xin Zhang Georgia Tech, Ravi Mangal Georgia Institute of Technology, Aditya Nori Microsoft Research, UK, Mayur Naik Georgia Tech
File Attached
14:45
25m
Talk
String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS
Research Papers
Anthony Widjaja Lin Yale-NUS College, Singapore, Pablo Barcelo University of Chile, Chile
Media Attached
15:10
25m
Talk
Symbolic Computation of Differential Equivalences
Research Papers
Luca Cardelli Microsoft Research and University of Oxford, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy, Max Tschaikowski IMT Institute for Advanced Studies Lucca, Italy, Andrea Vandin IMT Institute for Advanced Studies Lucca, Italy
Media Attached
15:35
25m
Talk
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
Research Papers
Matthew Hague Royal Holloway University of London, UK, Jonathan Kochems Department of Computer Science, University of Oxford, C.-H. Luke Ong University of Oxford, UK
Media Attached