[PRL] Seminar Monday 12/01 - Ioannis Baltopoulos

[Riccardo Pucella]

Hi folks,

Happy Thanksgiving!

Sorry about the short notice, but Ioannis Baltopoulos, a student of  
Andy Gordon in Cambridge, is going to be around on Monday and has  
agreed to give an out-of-schedule semantics seminar on recent work to  
be presented at TLDI'09. Information follows.


;; ---


Speaker: Ioannis Baltopoulos, Cambridge University

When/Where: Monday 12/01, 11h00, 366 WVH.

Title: Secure Compilation of a Multi-Tier Web Language

Abstract:
Storing state in the client tier (in forms or cookies, for example)
improves the efficiency of a web application, but it also renders the
secrecy and integrity of stored data vulnerable to untrustworthy
clients. We study this general problem in the context of the Links
multi-tier programming language.

We eliminate these threats by augmenting the Links compiler to encrypt
and authenticate any data stored on the client. We  model this
compilation strategy as a translation from a core fragment of the
language to a concurrent lambda-calculus equipped with a formal
representation of cryptography. To formalize source-level reasoning
about Links programs, we define a type-and-effect system for our core
language; our implementation can machine-check various integrity
properties of the source code. By appeal to a recent system of
refinement types for secure implementations, we show that our
compilation strategy guarantees all the properties provable by our
type-and-effect system.