USENIX Security '13 LangSec BoF

Wed Aug 14, 9:30pm in Regency Ballroom BCD (after rump session)

Language-Theoretic Security: Compositional Correctness for the Real World

Meredith L. Patterson, Nuance Communications

Sergey Bratus, Dartmouth College

Handling the composition of computing systems is arguably the hardest task of both security theory and practice. A system composed of parts with well-understood properties typically has emergent properties that are hard to derive from the properties of the parts, to validate, or even to detect. These new properties often come as a nasty surprise, creating vulnerabilities that only manifest when "safe" pieces are combined.

The language-theoretic view of security examines system and program components as computational automata, both in isolation and when composed into larger systems. This approach has led to the discovery of serious vulnerabilities in the PKI infrastructure, remote PHY-layer frame injection in 802.11b and other wireless protocols, and attacker-driven computation in the ELF runtime toolchain. Defensively, it also points the way to better implementation security through message validation and the conceptual separation of code between input recognition and processing. This BoF will also explore how to employ language-theoretic principles to construct software that is robust by design and exposes as little state and computational power as possible to adversaries.

If you've ever struggled to find a "sweet spot" between formal software validation and the collective experience of both software exploiters and defenders in the field, language-theoretic security offers a way to design protocols and build systems that can actually be validated and avoid large classes of bugs. Come hear success stories in both attack and defense, and check out the theory and systems challenges of this new and developing field.

[Summary]