BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Confining the Ghost in the Machine: Using Types to Secure JavaScri
 pt Sandboxing - Shriram Krishnamurthi\, Brown University
DTSTART:20120418T093000Z
DTEND:20120418T103000Z
UID:TALK37555@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:The commercial Web depends on combining content\, especially a
 dvertisements\, from sites that do not trust one another.  Because this co
 ntent can contain malicious code\, several corporations and researchers ha
 ve designed JavaScript sandboxing techniques (e.g.\, ADsafe\, Caja\, and F
 acebook JavaScript).  These sandboxes depend on static restrictions\, tran
 sformations\, and libraries that perform dynamic checks.  How can we be su
 re that they work?\n\nWe tackle the problem of proving the security of the
 se sandboxes.  Our technique depends on creating specialized types to char
 acterize the properties of the sandboxes\, exploiting the structure of the
  checks contained in the libraries.  The resulting checkers work on actual
  JavaScript code that is effectively unaltered\; I will focus on our appli
 cation to Yahoo!'s ADsafe.  We establish soundness using our semantics for
  JavaScript\, which has been tested for conformity against real implementa
 tions.\n\nJoint work with Arjun Guha and Joe Politz.
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR