[Colloq] Hiring Talk Amal Ahmed TODAY Wednesday, 25 May 2011
panarese at ccs.neu.edu
panarese at ccs.neu.edu
Wed May 25 08:32:16 EDT 2011
The College of Computer and Information Science presents a hiring talk by:
Amal Ahmed
Date: Wednesday, 25 May 2011
Time: 11:00am
Location: 366 West Village H
Title:
Stepping Beyond Toy Languages: Logical Relations for More Secure and Reliable Software
Abstract:
Logical relations are an important 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.
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
sophisticated mathematical machinery (e.g., domain or category theory)
that may be difficult to formalize and/or extend. 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.
_______________________________________________
Colloq mailing list
Colloq at lists.ccs.neu.edu
https://lists.ccs.neu.edu/bin/listinfo/colloq
More information about the Colloq
mailing list