Campus Event Calendar
Event Entry
What and Who
Logical Relations: A Step Towards More Secure and Reliable Software
Amal Ahmed
Toyota Technological Institute Chicago
SWS Colloquium
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 interests
lie in programming languages and language-based security, including
type theory, semantics, and secure compilation, with a focus on
advanced type systems and proof methods for reasoning about mutable
state.
AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 10 March 2009
16:00
60 Minutes
E1 4
019
Saarbrücken
Abstract
Logical relations are a powerful proof technique for establishing many
important properties of programs, programming languages, and language
implementations. In particular, they provide a convenient method for
proving behavioral equivalence of programs. Hence, they may be used
to show that one implementation of an abstract data type (ADT) can be
replaced by another without affecting the behavior of the rest of the
program; to prove that security-typed languages satisfy
noninterference, which requires that confidential data not affect the
publicly observable behavior of a program; and to establish the
correctness of compiler optimizations.
Yet, despite three decades of research and much agreement about their
potential benefits, logical relations are still primarily used to
reason about languages that are not even Turing complete. The method
has not scaled well to many features found in practical programming
languages: support for recursive types (lists, objects) and mutable
memory (as in Java or ML) requires sophisticated mathematical
machinery (e.g., domain theory, category theory), which makes the
resulting logical relations cumbersome to use and hard to extend.
Mutable memory is particularly problematic, especially in combination
with features like generics (parametric polymorphism) and ADTs.
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 applications.
The first is a secure multi-language system where we show that code
written in different languages may interoperate without sacrificing
the abstraction guarantees provided by each language in isolation.
The second is imperative self-adjusting computation, a system for
efficiently updating the results of a computation in response to
changes to some of its inputs; we show that our update mechanism is
consistent with a from-scratch run. The third is 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; we
show that the typed closure conversion phase of a compiler has this
property.
important properties of programs, programming languages, and language
implementations. In particular, they provide a convenient method for
proving behavioral equivalence of programs. Hence, they may be used
to show that one implementation of an abstract data type (ADT) can be
replaced by another without affecting the behavior of the rest of the
program; to prove that security-typed languages satisfy
noninterference, which requires that confidential data not affect the
publicly observable behavior of a program; and to establish the
correctness of compiler optimizations.
Yet, despite three decades of research and much agreement about their
potential benefits, logical relations are still primarily used to
reason about languages that are not even Turing complete. The method
has not scaled well to many features found in practical programming
languages: support for recursive types (lists, objects) and mutable
memory (as in Java or ML) requires sophisticated mathematical
machinery (e.g., domain theory, category theory), which makes the
resulting logical relations cumbersome to use and hard to extend.
Mutable memory is particularly problematic, especially in combination
with features like generics (parametric polymorphism) and ADTs.
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 applications.
The first is a secure multi-language system where we show that code
written in different languages may interoperate without sacrificing
the abstraction guarantees provided by each language in isolation.
The second is imperative self-adjusting computation, a system for
efficiently updating the results of a computation in response to
changes to some of its inputs; we show that our update mechanism is
consistent with a from-scratch run. The third is 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; we
show that the typed closure conversion phase of a compiler has this
property.
Contact
Claudia Richter
9325 688
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
206
passcode not visible
logged in users only
Claudia Richter, 03/06/2009 08:57
Claudia Richter, 03/05/2009 09:57 -- Created document.
Claudia Richter, 03/05/2009 09:57 -- Created document.