Type-Based Verification of Web Sandboxes
Joe Gibbs Politz, Arjun Guha, and Shriram Krishnamurthi
The paper: adsafety.pdf
The typed, annotated version of ADsafe discussed in the paper: typed-adsafe.js
The environment file that defines, among other things, the Untrusted type presented in the paper: adsafe.env
The source code: adsafety-aug-2013.tgz