Wed 10 Jan 2018 11:45 - 12:10 at Bunker Hill - Strings Chair(s): Zachary Tatlock

String analysis is the problem of reasoning about how strings are manipulated by a program. It has numerous applications including automatic detection of cross-site scripting, and automatic test-case generation. A popular string analysis technique includes symbolic executions, which at their core use constraint solvers over string domains, a.k.a. string solvers. Such solvers typically reason about constraints expressed in theories over strings with the concatenation operator as an atomic constraint. In recent years, researchers started to recognise the importance of incorporating the replace-all operator (i.e. replace all occurrences of a string by another string) and, more generally, finite-state transductions in the theories of strings with concatenation. Such string operations are typically crucial for reasoning about XSS vulnerabilities in web applications, especially for modelling sanitisation functions and implicit browser transductions (e.g. innerHTML). Although this results in an undecidable theory in general, it was recently shown that the straight-line fragment of the theory is decidable, and is sufficiently expressive in practice for many applications. In this paper, we provide the first string solver that can reason about constraints involving both concatenation and finite-state transductions, and that is a decision procedure for several relevant fragments, including straight-line. The main challenge that we address in the paper is the prohibitive worst-case computational complexity of the theory (double-exponential time), which is exponentially harder than the case without finite-state transductions. To this end, we propose a method that exploits succinct alternating finite-state automata as concise symbolic representations of string constraints. Compared to methods that use representations based on nondeterministic machines, alternation offers not only (expected) exponential savings in space when representing Boolean combinations of transducers, but, importantly, also a possibility of succinct representation of otherwise costly combinations of transducers and concatenation. Reasoning about the emptiness of the AFA language requires a state-space exploration in an exponential-sized graph. To this end, we use the model checking algorithms like IC3 for solving the problem. We have implemented our algorithm and demonstrated its efficacy on string benchmarks that are derived from cross-site scripting analysis and other examples in the literature.

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
StringsResearch Papers at Bunker Hill
Chair(s): Zachary Tatlock University of Washington, Seattle
10:30
25m
Talk
Synthesizing Bijective Lenses
Research Papers
Anders Miltner Princeton University, Kathleen Fisher Tufts University, Benjamin C. Pierce University of Pennsylvania, David Walker Princeton University, Steve Zdancewic University of Pennsylvania
10:55
25m
Talk
WebRelate: Integrating Web Data with Spreadsheets using Examples
Research Papers
Jeevana Priya Inala MIT, Rishabh Singh Microsoft Research
11:20
25m
Talk
What's Decidable About String Constraints with ReplaceAll Function?
Research Papers
Taolue Chen Birkbeck, University of London, Yan Chen State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences, Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
11:45
25m
Talk
String Constraints with Concatenation and Transducers Solved Efficiently
Research Papers
Lukáš Holík Brno University of Technology, Anthony Widjaja Lin Oxford University, Petr Janků Brno University of Technology, Philipp Ruemmer Uppsala University, Tomáš Vojnar Brno University of Technology