The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

(French version below)

- Laboratory: IMT/OLPS/ASE/SEC Security laboratory in the Orange Labs
  Service Platforms division Company: Orange SA
- Associated university: University of Rennes 1 – France
- Job location: Lannion – Côtes d'Armor (Brittany) - France

** Context
JavaScript is one of the most common languages of the web. It is
increasingly used to program embedded yet full-featured services. These
services, typically available through a regular browser or a specific
platform, often require access to critical functions of the device.
JavaScript's presence is also growing on the server side (node.js).

Unfortunately, the semantics of JavaScript is complex and it is
difficult to obtain formal guarantees on the behavior of scripts. This
may ultimately limit the use of language in services with high added
value and reduce its interest as an alternative to the proprietary
native platforms offered by devices.

** PhD topic
The goal of the thesis is to explore restrictions of the language that
would make possible the definition of a practical programming logic.
Additionally, the restricted language should preserve the
expressiveness, so that developers may still program in the most natural
way. In particular, the functional features of the language will have to
be supported. The choice of the restrictions will be guided by the
requirements of the programming frameworks most commonly used. The
approach will reuse existing tools, including the Why3 platform
developed to analyze C and Java programs. It will however be necessary
to extend it to support first class functions.

** Profile

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

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 system (or an equivalent theorem
prover), 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 at Orange Labs in Lannion (Brittany) in the
Security Department. This laboratory combines the expertise of its
project teams to design new security solutions to protect the
infrastructure or data of its customers. The team develops static
analysis tools for 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 expected to collaborate with other research teams
working on the topic especially those involved in the JSCert project
(http://jscert.org).

Contact at Orange: 
pierre.cregut AT orange.com

Contact at Irisa: 
alan.schmitt AT inria.fr

Reference on Orange Jobs website: not available yet: check section
"Etudiants/Students", subsection "Thèse/Thesis" on http://orange.jobs

------------- French Version ------------------------

- Laboratoire : IMT/OLPS/ASE/SEC laboratoire sécurité au sein de la
  division Orange Labs Plate-formes de Service Entreprise : Orange SA.
- Université partenaire : Université de Rennes 1
- Localisation : Lannion – Côtes d'Armor – France

** Contexte
JavaScript est un langage de plus en plus utilisé pour étendre les
fonctionnalité des appareils connectés, grâce à des applications
s'exécutant sur un navigateur web pouvant piloter directement certaines
fonctions critiques du terminal. JavaScript est également devenu très
présent dans les infrastructures, comme l'atteste node.js.

Malheureusement, la sémantique de JavaScript est complexe et il est
difficile d'obtenir des garanties formelles sur le comportement de
scripts. Cela peut à terme limiter l'emploi du langage dans des services
à forte valeur ajoutée et diminuer son intérêt comme alternative aux
plate-formes natives mais propriétaires offertes par les terminaux

** Sujet
L'objectif de la thèse est d'explorer des restrictions au langage qui
rendraient possible la définition d'une logique de programmes. Une
contrainte supplémentaire est que le langage restreint conserve la même
expressivité, et que les développeurs puissent programmer de la manière
la plus naturelle possible. En particulier, le cœur fonctionnel du
langage devra être conservé. Le choix des restrictions sera guidé par
les besoins des frameworks couramment utilisés pour structurer les
applications. L'approche suivie s'appuiera sur les outils existant, en
particulier la plate-forme Why3 développée pour l'analyse de programmes
C ou Java. Il sera cependant nécessaire d'étendre cette dernière
à l'ordre supérieur pour prendre en compte les fonctions de première
classe.

** Poste
Le candidat doit être diplômé d’une école d’ingénieur, titulaire d’un
Master Recherche ou équivalent. Il doit avoir de solides connaissances
en sémantique des langages et techniques de vérification de code (preuve
ou analyse statique). En particulier la connaissance du système Coq (ou
d'un assistant de preuve équivalent) dans lequel sont formalisés les
principaux travaux sur la sémantique de JavaScript est nécessaire. Une
bonne compréhension de Javascript et de son intégration avec HTML serait
un plus.

La thèse se déroulera dans les locaux d'Orange Labs à Lannion (Bretagne)
au sein du département Sécurité. Ce laboratoire combine l'expertise de
ses équipes projets pour définir de nouvelles solutions de sécurité, que
ce soit pour protéger les infrastructures ou les données de ses clients.
L'équipe développe des outils d'analyse statique pour les applications
sur terminaux mobiles (d'abord pour Java MIDP et aujourd'hui pour
Android).

La thèse sera rattachée à l'université de Rennes 1 et l'étudiant sera
amené à effectuer des séjours réguliers dans l'équipe Celtique de
l'Irisa. Le candidat aura également l'opportunité de collaborer avec
d'autres équipes de recherche, en particulier les membres du consortium
JSCert (http://jscert.org).

- Contact Orange : 
pierre.cregut AT orange.com
- Contact universitaire : 
alan.schmitt AT inria.fr
- Référence de la thèse sur Orange Jobs : à venir. Consulter
  http://orange.jobs menu 'Etudiants', rubrique 'Thèses'.

Alan Schmitt