Security Types for Web Applications

K. Bhargavan and S. Maffeis

Web applications such as social networks, online banking, and cloud-based storage routinely manipulate sensitive data, causing common concern about their security. These applications are written as a combination of PHP scripts that run on the server and client-side JavaScript that run in a browser. The goal of this internship is to design and implement type-based analyses that can verify security properties of such applications.

In previous work [Bengtson et al., 2008, Swamy et al., 2011], we desined and implemented a series of refinement type systems (F7, Fine, F*) for the F# language. The underlying type system are very expressive, and have been used to verify customizable security properties of sophisticated cryptographic applications. Moreover, they are able to verify programs even when part of the code is not trusted, which is crucial for analyzing web applications (such as mashups) that integrate third-party code. Our goal is to adapt these refinement type system and apply them to JavaScript and PHP programs.

There have been many recent attempts to design type systems for JavaScript, but most of them have no formal soundness guarantee. We plan to build a type system that is sound with respect to the JavaScript operational semmantics of Maffeis et al. [Maffeis et al., 2008], which has previously been used to define secure subsets of JavaScript and for discovering vulnerabilities in web applications [Maffeis et al., 2010].


The precise topic will be decided after discussion with the student, but during the course of the internship, the student will learn to do the following:

Some prior knowledge of web programming, cryptographic verification, and type systems will be an advantage, but is not mandatory.

The internship will be located at INRIA in Paris, with short visits to Imperial College in London. The dates of the internship and its duration are flexible and students of any nationality may apply. Masters students who are thinking of doing a Ph.D. are encouraged to apply for a six-month internship (i.e. a French M1/M2 stage). Ph.D. students and advanced undergraduate students (with adequate background) may apply for a three-month summer internship. 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. All interns are funded under the ERC grant CRYSP and successful internships are expected to lead to funded Ph.D. studentships.

Application Details.

To apply, send an email describing your research interests, and including your CV and the names and email addresses of one or two referees (professors or prior employers), to karthikeyan DOT bhargavan AT inria DOT fr. The deadline for applications is January 5, 2012. Positions will be kept open until filled.

The intern will have the opportunity to work closely with a team of researchers from INRIA and MSR-INRIA, including B. Blanchet, G. Steel, C. Fournet, and P-Y. Strub.

Related Proposals.


Bengtson et al. [2008]
J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. In 21st IEEE Computer Security Foundations Symposium (CSF’08), pages 17–32, 2008. PDF.
Maffeis et al. [2008]
S. Maffeis, J. Mitchell, and A. Taly. An operational semantics for JavaScript. In Proc. of APLAS’08, volume 5356 of LNCS, pages 307–325, 2008. See also: Dep. of Computing, Imperial College London, Technical Report DTR08-13, 2008. PDF.
Maffeis et al. [2010]
S. Maffeis, J. C. Mitchell, and A. Taly. Object capabilities and isolation of untrusted web applications. In IEEE Symposium on Security and Privacy, pages 125–140, 2010. PDF.
Swamy et al. [2011]
N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with value-dependent types. In Proceeding of the 16th ACM SIGPLAN international conference on Functional programming, ICFP ’11, pages 266–278, New York, NY, USA, 2011. ACM. .

This document was translated from LATEX by HEVEA.