[TYPES/announce] PhD position on JavaScript at Orange

[Alan Schmitt]

Hello,

A PhD position to do research on JavaScript at Orange, Lannion, France,
is available. Please find more information about it below.

Alan Schmitt

* Contracts for JavaScript in an Open environment
** About Orange
Orange is one of the world's leading telecommunications operators with sales of
43.5 billion euros for 2012. Orange employs 170,000 persons worldwide, including
105,000 in France. Present in 32 countries, the Group has a total customer base
of 230 million customers as of December, 31, 2012.

** Context
JavaScript is the assembly language of the web. It is increasingly used to
program complete embedded services accessible from web browsers, including
browsers running on mobile terminals. As a consequence, JavaScript applications
may need to have access to critical functions of these terminals to provide the
services of interest.

Unfortunately, the semantics of JavaScript is very complex. It is thus
challenging to obtain any formal guarantee on the behavior of scripts. This
shortcoming may ultimately limit the use of the language to program services,
and thus reduce its interest as an alternative to the usual native and
proprietary device-specific platforms.

** PhD topic
The goal of the thesis is to explore the definition of subsets of the JavaScript
language that would make it possible to design a practical programming logic
without fundamentally changing the expressiveness of the language: developers
should still be able to program in the most natural way. In particular, the
functional heart of the language must be supported. This programming logic would
then be used to prove properties of the applications.

Wherever possible existing tools will be reused, possibly extending them. In
particular, a stepping stone of the research should be the Why3 platform,
developed for the analysis of C and Java programs. A first challenge will be its
extension to a higher-order logic, required for the functional aspects of
JavaScript.

** Profile
The candidate should have a degree equivalent to a French Research Master.

She or he must have a solid background on the semantics of programming language
and code verification techniques (proof or static analysis). In particular,
knowledge of the Coq proof assistant (or an equivalent theorem prover), which is
currently used for the formalization of the semantics of JavaScript, is
required. A good understanding of JavaScript and its integration with HTML is a
plus.

The thesis will take place in the Security Department of Orange Labs in Lannion
(Brittany). This laboratory offers its expertise to design new security
solutions ranging from infrastructure to data protection for Orange
customers. The team currently develops static analysis tools for the analysis of
mobile applications (initially for MIDP phones and now for Android).

The thesis will be done in collaboration with the University of Rennes 1. The
student will work with the Celtique Research team from Inria and will make
regular visits to this team.

The candidate is also expected to collaborate with other research teams working
on the topic, especially those involved in the JSCert project
(http://jscert.org).

** Contacts
Contact at Orange: pierre.cregut at orange.com

Contact at Inria: alan.schmitt at inria.fr

Reference on Orange Jobs :
http://orange.jobs/jobs/offer.do?joid=32730&lang=en&wmode=light (reference
0005874).