Secure Compilation of a Multi-Tier Web Language

Ioannis Baltopoulos and Andrew Gordon

The ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2009)
Savannah, Georgia, USA, Saturday, 24 January, 2009

---

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 web-programming language. Like other systems, Links stores unencrypted application data, including web continuations, on the client tier; hence, Links is open to attacks that expose secrets, and modify control flow and application data. We characterise these attacks as failures of the general principle that security properties of multi-tier applications should follow simply from review of the source code (as opposed to the detailed study of the files compiled for each tier, for example). We propose a secure compilation strategy, which uses authenticated encryption to eliminate these threats, and we implement it as a simple extension to the Links system. 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.

---

START Conference Manager (V2.56.8 - Rev. 399)