Symbolic Transducers

Symbolic Finite Transducers, or SFTs, is a representation of finite transducers that annotates transitions with logical formulae to denote sets of concrete transitions. This representation has practical advantages in applications for web security analysis, as it provides ways to succinctly represent web sanitizers that operate on large alphabets. More importantly, the representation is also conducive for efficient analysis using state-of-the-art theorem proving techniques. Besides introducing SFTs we provide algorithms for various closure properties including composition and domain restriction. A central result is that equivalence of SFTs is decidable when there is a fixed bound on how many different values that can be generated for arbitrary inputs. In practice, we use a semi-decision algorithm, encoded axiomatically, for non-equivalence of arbitrary SFTs. We show that several of the main results lift to a more expressive version of SFTs with Registers, SFTRs. They admit a fixed set of registers that can be referenced in the logical formulae, updated by input characters, or used to generate output.