Static Verification for Web Scripting Languages

Add to your list(s) Download to your calendar using vCal

• Ravi Chugh, UC San Diego
• Tuesday 09 April 2013, 10:00-11:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

Modern web applications are developed largely in so-called “dynamic” or “scripting” languages like JavaScript, PHP , and Python. In addition to being untyped, these languages sport several features— run-time type tests, value-indexed dictionaries, and dynamic code loading— that make it easy to rapidly prototype and to glue together applications from disparate components. As applications grow large, however, the lack of static typing makes it difficult to achieve reliability and maintainability. Moreover, third-party code like ads and browser extensions are routinely downloaded and run in the client’s browser, and the flexibility of scripting languages makes it hard to ensure security.

In the first part of this talk, I will present Dependent JavaScript (DJS), a statically typed dialect that facilitates precise reasoning about JavaScript and other web scripting languages. I will describe the major obstacles that have stymied prior attempts at static reasoning for JavaScript, and I’ll outline how DJS overcomes them using several key innovations based on refinement types.

In 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 that will lead to a platform for fine-grained web security.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge University Engineering Department Talks
• Centre for Smart Infrastructure & Construction
• Featured lists
• Methodology in design research
• Microsoft Research Cambridge, public talks
• School of Technology
• de239's list
• engineering

Note that ex-directory lists are not shown.