ADsafety: Type-Based Verification of JavaScript Sandboxing
Programming Languages
2015-06-26 v1
Abstract
Web sites routinely incorporate JavaScript programs from several sources into a single page. These sources must be protected from one another, which requires robust sandboxing. The many entry-points of sandboxes and the subtleties of JavaScript demand robust verification of the actual sandbox source. We use a novel type system for JavaScript to encode and verify sandboxing properties. The resulting verifier is lightweight and efficient, and operates on actual source. We demonstrate the effectiveness of our technique by applying it to ADsafe, which revealed several bugs and other weaknesses.
Keywords
Cite
@article{arxiv.1506.07813,
title = {ADsafety: Type-Based Verification of JavaScript Sandboxing},
author = {Joe Gibbs Politz and Spiridon Eliopoulos and Arjun Guha and Shriram Krishnamurthi},
journal= {arXiv preprint arXiv:1506.07813},
year = {2015}
}
Comments
in Proceedings of the USENIX Security Symposium (2011)