Towards Security Types for Client-Side Web ApplicationsK. Bhargavan and S. Maffeis |
Web applications such as social networks, online banking, web-based email etc. play an ever increasing role in our lives, and cause common concern about the security of our data and browsers. The goal of this internship is to work towards a type system able to verify security properties of JavaScript programs, which today (and for the foreseeable future) constitute the bulk of client-side web applications.
In previous work [Bengtson et al., 2008, Bhargavan et al., 2010], we have defined F7, a typechecker for the F# language based on refinement types. The underlying type system is very expressive, and can be used to verify customizable security properties. Moreover, it is able to verify programs also under the assumption that part of the code is not trusted, which is a very important concern for web applications (such as mashups) that integrate third-party code. We plan to base the type system for JavaScript on the one for F7.
Although recently there have been some academic proposals for type systems for JavaScript, they either are defined on toy languages inspired by JavaScript or come with no formal soundness guarantee. Our approach will not suffer from such limitations. Maffeis et al. have defined a complete operational semantics for JavaScript [Maffeis et al., 2008]. It has proven to be a useful tool for defining secure subsets of JavaScript and for discovering vulnerabilities in web applications [Maffeis and Taly, 2009, Maffeis et al., 2010]. We plan to formally prove that our type system is sound with respect to the JavaScript operational semantics.
The internship will involve designing a refinement-based type system for JavaScript, proving its soundness, implementing a corresponding typechecker, and verifying some JavaScript programs to validate the typechecker. Due to the internship timing constraints, this work will be carried out as a proof-of-concept, on suitable fragments of the language and the type system. The project has scope to be extended to the full type system and language, with a release quality implementation, as part of a PhD. The ideal candidate would have a strong interest in formal methods (in particular types systems or abstract interpretation), some interest in security and web applications, and knowledge of (or desire to learn) Ocaml/F# and JavaScript.
The internship will be based at the Microsoft Research–INRIA Joint Center and may involve a period of research at Imperial College London (with Dr. S. Maffeis). At the joint center, the intern will work within the Secure Distributed Programming team which also includes C. Fournet, J. Leifer, A. Pironti, P-Y Strub, and F Zappa-Nardelli).
The internship is funded under a long-running ERC-funded project, called CRYSP, whose aim is to develop provably secure web applications. We expect the research carried out during the internship will form the major part of a Masters-level thesis and lead to a conference publication. We also expect to fund several Ph.D. students over the next few years.
To apply, send an email describing your research interests, and including your CV and the names and email addresses of two referee, to karthikeyan DOT bhargavan AT inria DOT fr. The deadline for applications is February 15, 2011.
This document was translated from LATEX by HEVEA.