|
Amal Ahmed Toyota Technological Institute |
|
Logical Relations: A Step Towards More Secure and Reliable Software Logical relations are a promising proof technique for establishing many important properties of programs, programming languages, and language implementations. They have been used to show type safety, to prove that one implementation of an abstract data type (ADT) can be safely replaced by another, to show that languages for information-flow security ensure confidentiality, and to establish the correctness of compiler transformations and optimizations. Yet, despite three decades of research and much agreement about their potential benefits, logical relations have only been applied to "toy" languages, because the method has not easily scaled to important linguistic features, including recursive types, mutable references, and (impredicative) generics. Previous approaches have tried to address some of these features through sophisticated mathematical machinery (domain or category theory) which makes the results difficult to formalize and/or extend. In this talk, I will describe *step-indexed* logical relations which support all of the language features mentioned above and yet permit simple proofs based on operational reasoning, without the need for complicated mathematics. To illustrate the effectiveness of step-indexed logical relations, I will discuss three new contexts where I have been able to successfully apply them: secure multi-language interoperability; imperative self-adjusting computation, a mechanism for efficiently updating the results of a computation in response to changes to some of its inputs; and security-preserving compilation, which ensures that compiled code is no more vulnerable to attacks launched at the level of the target language than the original code is to attacks launched at the level of the source language. ********** Amal Ahmed is a Research Assistant Professor at the Toyota Technological Institute at Chicago. She received her Ph.D. in Computer Science from Princeton University in 2004 and spent two years at Harvard as a Postdoctoral Fellow before joining TTI-C in 2006. She holds an A.B. in Computer Science and Economics from Brown University and an M.S. in Computer Science from Stanford. Her research in programming languages and language-based security focuses on type systems, semantics, secure compilation, and reasoning about mutable state. |
|
4:15pm 5130 Upson Hall Thursday, April 23, 2009 Refreshments at 3:45pm in the Upson 4th Floor Atrium |
|
Computer Science Colloquium Spring 2009 |
|
www.cs.cornell.edu/events/colloquium |