University of Cambridge > > Semantics Lunch (Computer Laboratory) > Secure Compilation of a Multi-Tier

Secure Compilation of a Multi-Tier

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

  • UserIoannis Baltopoulos
  • ClockMonday 08 December 2008, 12:45-14:00
  • HouseFW26.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity