• About
  • About the Department
  • Contact
  • Directions
  • Partners
  • Rooms
  • Systems & Software
  • Conduit
  • News
  • Events
  • Blog
• People
  • Our Community
  • Faculty
  • Staff
  • Grad Students
  • Ugrad Students
  • Alums
  • Directory
• Research
  • Research Links
  • Areas
  • Publications
• Degrees
  • Degree Programs
  • Doctoral
  • Masters
  • Undergrad
  • Programs
  • Miscellaneous
• Courses
  • Course List
  • Schedule
  • Sections
  • TA Program

The 44th IPP Symposium

Confining the Ghost in the Machine: Using Types to Secure JavaScript Sandboxing

Arjun Guha, Brown University

The commercial Web depends on combining content, especially advertisements, from sites that do not trust one another. Because this content can contain malicious code, several corporations and researchers have designed JavaScript sandboxing techniques (e.g., ADsafe, Caja, and Facebook JavaScript). These sandboxes depend on static restrictions, transformations, and libraries that perform dynamic checks. But, do they actually work?

We tackle the problem of proving the security of these sandboxes. Our technique is to employ a JavaScript type-checker to encode and verify the properties of sandboxes. The type-checker is lightweight, efficient, and operates on actual source. I will discuss our verification of ADsafe, which revealed several bugs and other weaknesses. (Joint work with Spiridon Eliopoulos, Shriram Krishnamurthi, and Joe Gibbs Politz)

Arjun Guha is a graduate student of Computer Science at Brown University. His work focuses on securing existing Web programs and designing new programming languages for the Web. He co-developed Flapjax (a reactive programming language), LambdaJS (a semantics for JavaScript), and Google Belay (a cloud authorization protocol). More recently, he has been working on the safe management of software-defined networks.