The goal of my research is to develop programming abstractions and automated
analyses to assist programmers. In this talk, we focus on how techniques
rooted in automata and transducers can be used to detect security
vulnerabilities in programs such as HTML sanitizers and string encoders.
In the first part of the talk, we show how HTML sanitizers and augmented
reality taggers can be modeled using tree transducers, a specialized machine
model for tree transformations. Then, using the decision procedures for
manipulating and analyzing transducers, we can prove whether an HTML
sanitizer always produce safe outputs, and whether two augmented reality
taggers can interfere with each other. We show how these techniques are
built into Fast, a programming language that makes transducer-based analysis
easy to use in practice.
In the second part of the talk, we focus on a foundational question about
tree transformations. The class of regular tree transformations contains
many commonly occurring transformations and has robust closure properties
similar to regular languages. We present the first deterministic machine
model that is capable of computing all regular tree transformations by
traversing the input tree in a single left-to-right pass. This model allows
us to establish the first known upper bound for checking equivalence of
regular tree transformations.