Ankur Taly : 2010 Security Workshop

A growing number of current web sites combine active content (applications) from untrusted sources, as in so-called mashups. The object-capability model provides an appealing approach for isolating untrusted content: if separate applications are provided disjoint capabilities, a sound object-capability framework should prevent untrusted applications from interfering with each other, without preventing interaction with the user or the hosting page.

In this talk, I will present a formal definition of the object capability model and its application to the 'mashup isolation problem'. In developing language-based foundations for isolation proofs based on object-capability concepts, we identified a more general notion of authority safety that also implies resource isolation. I will present a formal definition of the authority safety property and show that capability safety implies authority safety. Next I will show the applicability of our framework for a specific class of mashups. In addition to proving that a JavaScript subset based on Google Caja is capability safe, I will show that a more expressive subset of JavaScript is authority safe, even though it is not based on the object-capability model.

Joint work with Sergio Maffeis and John C. Mitchell.

I am a 3rd year PhD candidate in the Department of Computer Science at Stanford University, working with Prof. John C. Mitchell. Prior to joining Stanford, I completed my B.Tech in Computer Science from Indian Institute of Technology, Bombay in 2007. My research interests include - web-security, formal methods, programming languages and logic.