ADsafety: Type-Based Verification of JavaScript Sandboxing

Joe Gibbs Politz, Spiridon Aristides Eliopoulos, Arjun Guha, and Shriram Krishnamurthi

Please see the journal version instead. Rather than a minimal revision, it is a substantial improvement over this version of the paper. It provides a better description of the problem and of the solution approach; provides a thorough description of the technical approach; fixes some mistakes in this version; and reflects progress since this version was written. This version should be regarded as purely archival.

The paper. (pdf)

Proofs for the object type system presented in the paper. (pdf)

Note: The journal page has updated source with some bugfixes; these files are archival.

The typed, annotated version of ADsafe discussed in the paper: typed-adsafe.js

The environment file that defines, among other things, the Widget type presented in the paper: adsafe.env

The original source code (tested with Rhino 1.7 and ML 3.11.1 on Ubuntu 9.10): adsafety.tgz