Secure compilation of a multi-tier web language

Secure compilation of a multi-tier web language,10.1145/1481861.1481866,Ioannis G. Baltopoulos,Andrew D. Gordon

Secure compilation of a multi-tier web language   (Citations: 4)
BibTex | RIS | RefWorks Download
Storing state in the client tier (in forms or cookies, for exam- ple) improves the efficiency of a web application, but it also ren- ders the secrecy and integrity of stored data vulnerable to untrust- worthy clients. We study this general problem in the context of the LINKS multi-tier programming language. Like other systems, LINKS stores unencrypted application data, including web contin- uations, 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 from re- view of the source code (as opposed to the detailed study of the files compiled for each tier, for example). 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 l- 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 imple- mentations, we show that our compilation strategy guarantees all the properties provable by our type-and-effect system.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: