[Colloq] Hiring Talk Amal Ahmed Wednesday, 25 May 2011

[panarese at ccs.neu.edu]

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.