Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Logical Relations: A Step Towards More Secure and Reliable Software
Speaker:Amal Ahmed
coming from:Toyota Technological Institute Chicago
Speakers 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 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
Event Type:SWS Colloquium
Visibility:D1, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Expert Audience
Date, Time and Location
Date:Tuesday, 10 March 2009
Duration:60 Minutes
Building:E1 4
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
Name(s):Claudia Richter
Phone:9325 688
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:206
Meeting ID:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Claudia Richter, 03/06/2009 08:57 AM
  • Claudia Richter, 03/05/2009 09:57 AM -- Created document.