Programming Languages Lunch - Andreas Gampe, The University of Texas at San Antonio, "A Framework for Composing Security-Typed Languages"

Contact Name: 
John Thywissen
GDC 6.302
Sep 9, 2013 12:00pm - 1:30pm

Talk Audience: UTCS Faculty, Grads, Undergrads, Other Interested Parties

Talk Abstract: Users often run software programs that have access to private information that they do not wish to be disclosed publicly.  One approach to protecting such data is to require that the programs be certified using a security type system.  Security type systems have, previously, only been studied for programs written entirely in a single language.  In practice, however, software is frequently implemented using multiple specialized languages for different tasks.

We present a framework that facilitates reasoning over composed languages. In it guarantees of sufficiently related component languages can be lifted to the composed language.  This can significantly lower the burden necessary to certify that such composite programs are safe. Our simple but powerful approach relies, at its core, on computability and security-level separability.  To demonstrate this framework, we develop a secure type system for an expressive fragment of SQL and embed it into a secure While language from the literature.  We then prove all the requirements necessary to apply our approach and show that all well-typed composite While+SQL programs are safe.

Speaker Bio: Andreas Gampe is a PhD candidate in the Department of Computer Science at the University of Texas at San Antonio. His research interests include programming languages, security, and software engineering. His current research focuses on formal aspects of security, applying language-based techniques to secure multi-component software systems.