[PRL] Reminder: Seminar today (11h00), Ioannis Baltopoulos

[Riccardo Pucella]

Hi folks,

I would just like to remind you that Ioannis Baltopoulos, a student  
of Andy Gordon in Cambridge, is taling this morning. 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.