When reviewing code or protocol specifications, have you ever had a feeling that it might be a problem but couldn’t quite prove it? LangSec can help you do that. LangSec, or language-theoretic security, is the idea that basic theory of computation (that is, reasoning about grammatical complexity and automata) can act as a guiding design principle for the construction of secure parsers, and thereby increase the security of programs in general. Until this point, it has been a somewhat theoretical discipline–aside from the Hammer framework, few industry tools make specific use of it.
We discuss recent developments in LangSec and bring the community up to speed on our efforts to bridge the gap between theoretical and practical information security. We back-validated LangSec and found that it would have predicted a lot of bugs in commonly used software; we discuss these results. We’ll contextualize several real examples in the LangSec framework and demonstrate a set of rules (and corresponding proposed CWE entries) designed to help programmers avoid writing insecure parsers. Then, we’ll discuss how code reviewers can use this context to find bugs and what tooling can be constructed around LangSec principles in the future.