ADsafety: Type-Based Verification of JavaScript Sandboxing
Joe Gibbs Politz, Spiridon Eliopoulos, Arjun Guha, and Shriram, Krishnamurthi

TL;DR
This paper introduces ADsafety, a novel type-based verification method for JavaScript sandboxing, ensuring security properties are maintained across multiple sources in web pages.
Contribution
It presents a lightweight, source-level verifier using a new type system to verify sandboxing properties in JavaScript, demonstrated on ADsafe.
Findings
Revealed several bugs in ADsafe
Identified weaknesses in existing sandboxing approaches
Proved the effectiveness of the type-based verification method
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsWeb Application Security Vulnerabilities · Security and Verification in Computing · Software Testing and Debugging Techniques
