Logical Relations: A Step Towards More Secure and Reliable Software
Speaker: Amal Ahmed , Toyota Technological Institute at Chicago
Date: March 19 2009
Time: 4:00PM to 5:00PM
Location: 32-G449
Host: Martin Rinard, MIT
Contact: Francis Doughty, 253-4602, doughty@mit.edu
Relevant URL: 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.
Bio:
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.
See other events that are part of CS Special Seminar Series Spring 2009
See other events happening in March 2009
