Programming using Automata and Transducers

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.