Skip to main content

Find us on

facebook youtube flickr twitter itunes u logo


Upcoming Events   

 Craig Shue



Managing User-Level Compromises in Enterprise Networks
Craig Shue
Worcester Polytechnic Institute
Tuesday March 31, 2015 @4:15pm
Carson L01

 Harold Thimbleby




The Best Way to Improve Healthcare is to Improve Computers
Harold Thimbleby
Swansea University
Thursday April 23, 2015 @4:15pm

Carson L01

Mary Ellen Zurko



User-Centered Security: From Grand Challenge to Technology Transfer
Mary Ellen Zurko
Tuesday May 12, 2015 @4:15pm
Carson L01

Scout Sinclair Brody



Open-Sourcing Usable Security
Scout Sinclair Brody D'13 Ph.D.
Simply Secure
Tuesday June 2, 2015 @4:15pm
Carson L01

Recent Talks  

Radu Sion

Computation Privacy and Regulatory Compliance Mechanisms for the Cloud
Radu Sion
Stony Brook University and Private Machines Inc.
May 28, 2013

mechael youtube

Keynote: Securing IT in Healthcare: Part III
Patty Mechael
mHealth Alliance
May 16, 2013



Feb news 2015


ISTS Information Pamphlet



Institute for Security, Technology, and Society
Dartmouth College
6211 Sudikoff Laboratory
Hanover, NH 03755 USA
HomeEvents >

Towards a formal theory of computer insecurity: a language-theoretic approach

len meredith
Len Sassaman Meredith L. Patterson

Len Sassaman, Katholieke Universiteit Leuven
Meredith L. Patterson, Independent researcher
Thursday, February 17, 2011


Finding weaknesses in computer programs and systems is commonly thought of as a "knack" or "a black art" by industry practitioners and academics alike. This craft of vulnerability analysis is typically taught by example, through case studies of (in)famous vulnerabilities of the past and the often highly idiosynchratic methods used by their discoverers. Moreover, even though we have a number of theories for how to build provably secure systems from scratch, they do not readily yield themselves to finding insecurities in state-of-the-art existing systems.

When we teach students about those pitfalls of insecure programming, we do not involve a theory that would explain the fundamental origins of this insecurity, and neither do we look to such a theory when searching for exploitable vulnerabilities in a piece of software. This is in stark contrast with other areas of CS, where we continually see and use applications of complexity theory, computation theory, various algorithm analysis results, etc.

The authors show their way from asking themselves these questions to identifying the suitable theoretical constructs and using them to expose a slew of high-impact "0day" vulnerabilities in one of the most frequently used security protocols of today, Secure Sockets Layer and X.509 security certificates, used throughout the world to protect e-commerce, as well as confidential and even classified data.

The authors will further show how many classic case studies in software vulnerabilties can be reduced to familiar principles of the formal languages and computation theory and discuss the implications of this reduction for the future of the current Internet protocols and the design of new secure ones.

Finally, the authors will discuss how modern programming language techniques such as monadic programming and parser combinators -- usually considered obscure -- can have a direct bearing on teaching secure programming in such mundane tasks as web application development.


Len Sassaman, Katholieke Universiteit Leuven

Len Sassaman is a member of the Shmoo Group, as well as a researcher at COSIC, the COmputer Security and Industrial Cryptography laboratory at Katholieke Universiteit Leuven. He is currently pursuing his PhD in electrical engineering, advised by Bart Preneel and David Chaum. The focus of Len's past research has been privacy-preserving technologies, such as anonymity and confidentiality systems, which emphasize usability as a security parameter in privacy solutions subject to the limitations of today's communication systems. Len has over fifteen years of experience designing and deploying privacy enhancing technologies and evaluating protocol security. Len is the maintainer of the anonymous remailer software Mixmaster, a former Tor and Mixmaster server operator, and has written many papers on the topic of anonymous system design. Len has also consulted on policy issues regarding Internet privacy in today's society.

Len Sassaman also co-invented the field of language-theoretic security research, which is the topic of his talk. Prior to becoming an academic researcher, Len was an active cypherpunk and held such roles as Chief Architect at Anonymizer, Inc., Senior Security Architect at Known Safe, Inc., and a Lead Software Engineer at PGP Security, Inc. Last year at Black Hat, Len presented (with Dan Kaminsky) a series of fatal flaws in the Certificate Authority system, discovered using language-theoretic security analysis methods.

Len has spoken at many security conferences, co-founded the CodeCon and Biohack! conferences and the HotPETS workshop.


Meredith L. Patterson is an independent researcher whose areas of expertise range from CS-related topics such as database design, data-mining algorithms, complexity theory, computational linguistics, information security, and privacy-enhancing technology systems; to synthetic biology, design of transgenic organisms using low-cost, build-it-yourself lab equipment, and human metabolic system studies; and speculative fiction as a published author of multiple short stories, mostly science fiction.

Meredith has a BA in Linguistics from the University of Houston and a MA in Linguistics from the University of Iowa. She is heavily involved with the DIYBio movement, and works on transgenic lactic acid bacteria. She co-founded the field of language-theoretic security research, which she used to successfully defeat such troublesome attacks as SQL injection with her "Dejector" library. Most recently, she presented the Biopunk Manifesto at a UCLA synthetic biology conference, and presented her work with Dan Kaminsky and Len Sassaman on breaking the Internet's certificate authority system (by creating usable, bogus certificates crafted to exploit ambiguity in X.509 parsing implementations using language-theoretic security analysis principles) at the Financial Cryptography 2010 conference.

Meredith lives in Leuven, Belgium. In her spare time, she knits, repairs cars, and hacks on open source software.



Last Updated: 2/28/11