Secure Compilation of a Multi-Tier

Add to your list(s) Download to your calendar using vCal

• Ioannis Baltopoulos
• Monday 08 December 2008, 12:45-14:00
• FW26.

If you have a question about this talk, please contact Matthew Parkinson.

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.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Computer Laboratory talks
• FW26
• School of Technology
• Semantics Lunch (Computer Laboratory)
• de239's list

Note that ex-directory lists are not shown.