BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Static Verification for Web Scripting Languages - Ravi Chugh\, UC 
 San Diego
DTSTART:20130409T090000Z
DTEND:20130409T100000Z
UID:TALK43848@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Modern web applications are developed largely in so-called "dy
 namic" or "scripting" languages like JavaScript\, PHP\, and Python. In add
 ition to being untyped\, these languages sport several features --- run-ti
 me type tests\, value-indexed dictionaries\, and dynamic code loading --- 
 that make it easy to rapidly prototype and to glue together applications f
 rom disparate components. As applications grow large\, however\, the lack 
 of static typing makes it difficult to achieve reliability and maintainabi
 lity. Moreover\, third-party code like ads and browser extensions are rout
 inely downloaded and run in the client's browser\, and the flexibility of 
 scripting languages makes it hard to ensure security.\n\nIn the first part
  of this talk\, I will present Dependent JavaScript (DJS)\, a statically t
 yped dialect that facilitates precise reasoning about JavaScript and other
  web scripting languages. I will describe the major obstacles that have st
 ymied prior attempts at static reasoning for JavaScript\, and I'll outline
  how DJS overcomes them using several key innovations based on refinement 
 types.\n\nIn the second part of the talk\, I will show how to build on DJS
  to verify security properties of third-party JavaScript. After describing
  preliminary experiments that use DJS to author provably-secure JavaScript
  browser extensions\, I will identify several future directions of work th
 at will lead to a platform for fine-grained web security.\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR