Sémantique formelle des proxies de la prochaine version de JavaScript

Nous utilisons de plus en plus des applications web, que ce soit dans notre vie personnelle, professionnelle ou sociale. Nous les utilisons pour communiquer, travailler sur des documents partagés, gérer nos comptes bancaires ou interagir avec des administrations. Dans tous ces cas, nous leur confions des données personnelles. De plus, ces applications sont intrinsèquement distribuées: nous les utilisons au travers d'un navigateur web en téléchargeant et exécutant des scripts qui communiquent avec des services web. Pour des raisons de performances, une part de plus en plus grande de ces applications est exécutée directement par le navigateur. Celui-ci est ainsi devenu une machine virtuelle pour applications web.

La conjonction de ces aspects, c'est à dire l'utilisation massive d'applications manipulant des données personnelles et s'exécutant dans un même environnement, est le point de départ de ce sujet de stage: jusqu'à quel point pouvons-nous faire confiance à ces applications ?

La réponse apportée en pratique est une compartimentation par le navigateur selon la « same origin policy » (SOP): un script envoyé par un site peut seulement accéder à des informations associées à ce site, que ce soit ses données, par exemple des cookies, ou d'autres scripts. Malheureusement, non seulement l'implémentation cohérente de cette compartimentation est particulièrement complexe ¹, elle va également à l'encontre de la construction de « mashups »: l'intégration de plusieurs applications web pour fournir un nouveau service, comme l'affichage de critiques de restaurants provenant d'un site sur une carte interactive fournie par un autre site. Une deuxième faiblesse de la SOP est qu'elle fait implicitement confiance au site web visité: l'origine des scripts atteste leur innocuité. Cependant, il arrive parfois qu'un site utilise de tels scripts afin de suivre ses utilisateurs sans les en informer. Un site peut également avoir des failles qui, lorsque exploitées, conduisent à l'injection de scripts illégitimes comme s'ils provenaient du site initial. Cette attaque, connue sous le nom de « cross-site scripting », est une des vulnérabilités les plus communes des applications web, et permet à un attaquant de modifier impunément une page web ou d'accéder à des informations sensibles comme des identifiants de session.

Une solution à ce problème consiste à compartementaliser, au niveau du langage, les données manipulées par les applications. Cette approche est en particulier utilisée par Secure EcmaScript ², basé sur le langage Caja ³ développé par Google. Le cœur de cette solution est la notion de « Object Capabilities » et de « proxies » ⁴. Ces concepts sont en cours de standardisation dans la spécification EcmaScript 6 de la prochaine version de JavaScript.

Afin de pouvoir apporter des garanties formelles, nous proposons dans le cadre de ce stage de:

• donner une définition formelle des Objets Capabilities;
• prouver que les proxies d'EcmaScript 6 capturent ces garanties.

Ce travail se basera sur JSCert ⁵, une formalisation en Coq de JavaScript.

Le projet sera encadré par Alan Schmitt dans l'équipe Celtique (Inria Rennes). L'étudiant aura l'opportunité d'interagir avec les autres membres du projet JSCert, non seulement dans Celtique, mais également au centre Inria de Saclay et à Imperial College. Ce sujet pourra être prolongé par une thèse dans le cadre du projet ANR AJACS.