BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Secure Compilation of a Multi-Tier - Ioannis Baltopoulos
DTSTART:20081208T124500Z
DTEND:20081208T140000Z
UID:TALK14776@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:Storing state in the client tier (in forms or cookies\, for ex
 ample)\nimproves the efficiency of a web application\, but it also renders
  the\nsecrecy and integrity of stored data vulnerable to untrustworthy\ncl
 ients. We study this general problem in the context of the Links\nmulti-ti
 er programming language.\n\nWe eliminate these threats by augmenting the L
 inks compiler to encrypt\nand authenticate any data stored on the client. 
 We  model this\ncompilation strategy as a translation from a core fragment
  of the\nlanguage to a concurrent lambda-calculus equipped with a formal\n
 representation of cryptography. To formalize source-level reasoning\nabout
  Links programs\, we define a type-and-effect system for our core\nlanguag
 e\; our implementation can machine-check various integrity\nproperties of 
 the source code. By appeal to a recent system of\nrefinement types for sec
 ure implementations\, we show that our\ncompilation strategy guarantees al
 l the properties provable by our\ntype-and-effect system.
LOCATION:FW26
END:VEVENT
END:VCALENDAR