LANGSEC: Language-theoretic Security "The View from the Tower of Babel"

The Language-theoretic approach (LANGSEC) regards the Internet insecurity epidemic as a consequence of ad hoc programming of input handling at all layers of network stacks, and in other kinds of software stacks. LANGSEC posits that the only path to trustworthy software that takes untrusted inputs is treating all valid or expected inputs as a formal language, and the respective input-handling routines as a recognizer for that language. The recognition must be feasible, and the recognizer must match the language in required computation power.

When input handling is done in ad hoc way, the de facto recognizer, i.e. the input recognition and validation code ends up scattered throughout the program, does not match the programmers' assumptions about safety and validity of data, and thus provides ample opportunities for exploitation. Moreover, for complex input languages the problem of full recognition of valid or expected inputs may be UNDECIDABLE, in which case no amount of input-checking code or testing will suffice to secure the program. Many popular protocols and formats fell into this trap, the empirical fact with which security practitioners are all too familiar.

LANGSEC helps draw the boundary between protocols and API designs that can and cannot be secured and implemented securely, and charts a way to building truly trustworthy protocols and systems.

How to get on the LANGSEC mailing list: subscribe at https://mail.langsec.org/list/

Articles and Papers

Talks

Two high-level summary articles in December 2011 ;login: "Exploit Programming: from Buffer Overflows to Weird Machines and Theory of Computation", Sergey Bratus, Michael E. Locasto, Meredith L. Patterson, Len Sassaman, Anna Shubina [PDF] "The Halting Problems of Network Stack Insecurity", Len Sassaman, Meredith L. Patterson, Sergey Bratus, Anna Shubina [PDF], [PDF@USENIX] (The first article explains the "weird machines" view of exploitation, the second one starts with a computation-theoretic view. We recommend reading both, and choosing the reading order based on your background.) Papers: Security Applications of Formal Language Theory, Len Sassaman, Meredith L. Patterson, Sergey Bratus, Michael E. Locasto, Anna Shubina [submitted for publication] [Dartmouth Computer Science Technical Report TR2011-709] The View from the Tower of Babel: a Language-theoretic Perspective on Vulnerability Classification, TBA

"The Science of Insecurity", Meredith L. Patterson, Sergey Bratus, October-December 2011 [Intro from 28c3], [28c3 video], || slides [28c3], [R.S.S.], [H2HC/Day-con], || [synopsis], [Patch for Postel's Principle] Coming soon: Q&A, notes, and references. Upcoming presentatons: Shmoocon, Troopers "Towards a formal theory of computer insecurity: a language-theoretic approach" Len Sassaman, Meredith L. Patterson, Invited Lecture at Dartmouth College, March 2011, [youtube] "Exploiting the Forest with Trees", Len Sassaman, Meredith L. Patterson, BlackHat USA, August 2010, [youtube]

Please link to this page as http://langsec.org/. This is a temporary page for the Language-theoretic Security interest group. It will likely move around and grow to include a forum of some kind. Please stay tuned.