Proceedings of the Symposium on Principles of Prog
Proceedings of the Symposium on Principles of Programming Languages (POPL) Year 2013 Peer-reviewed
BibTeX PDF
Web Security · Privacy

Fully Abstract Compilation to JavaScript

Cedric Fournet Nikhil Swamy Juan Chen Pierre-Evariste Dagand Pierre-Yves Strub Benjamin Livshits
2013
Publication year
POPL
Venue
Peer-reviewed
Type
§ Abstract

Problem

Many tools allow programmers to develop applications in high- level languages and deploy them in web browsers via compilation to JavaScript. While practical and widely used, these compilers are ad hoc: no guarantee is provided on their correctness for whole programs, nor their security for programs executed within arbitrary JavaScript contexts.

Approach

This paper presents a compiler with such guarantees. We compile an ML-like language with higher-order functions and references to JavaScript, while preserving all source pro- gram properties.

Results

Relying on type-based invariants and applicative bisimilarity, we show full abstraction: two programs are equivalent in all source contexts if and only if their wrapped translations are equivalent in all JavaScript contexts. We evaluate our compiler on sample programs, including a series of secure libraries.

Cite this paper — BibTeX 
@inproceedings{fournet-popl13,
  title = "Fully Abstract Compilation to JavaScript",
  author = "Cedric Fournet and  Nikhil Swamy and  Juan Chen and  Pierre-Evariste Dagand and  Pierre-Yves Strub and Benjamin Livshits",
  year = "2013",
  month = jan,
  booktitle = {Proceedings of the Symposium on Principles of Programming Languages (POPL)}
}
Copied