Spécification de JavaScript

Cette approche part de deux constats : d'une part, le JavaScript n'est pas sécurisé à cause d'une sémantique non conventionnelle ; d'autre part, le langage est trop complexe pour être testé par des outils de tests standard. C'est sur ces deux points que se sont portés les travaux de Arjun Guha, Claudiu Saftoiu et Shriram Krishnamurthi.

Leur premier travail a été de concevoir un noyau, nommé λJS, qui ne contient que les fonctions essentielles du langage, sorte de sous-ensemble complet de JavaScript. Bien sûr, le fait de ne garder que l'essence du langage fait que beaucoup de sucre syntaxique n'existe plus. Prenons, par exemple, l'implémentation des objets, où certaines syntaxes ont été supprimées, au privilège d'une seule lorsque plusieurs sont envisageables. Afin d'accéder à l'attribut x d'un objet Y, il est normalement possible d'écrire Y['x'] ou Y.x. Cependant, λJS ne possède que l'écriture Y['x'] et n'implémente pas d'écriture alternative afin de garder le noyau de langage le plus petit possible. Une autre modification majeure est la disparation de l'utilisation implicite du this. En effet, lorsque l'on utilise le mot clé this, le programme fait référence à l'objet sur lequel est appelée la fonction. Toutefois, ce paramètre est implicite, il n'est donc pas nécessaire de le renseigner lors de l'appel de la méthode d'un objet, ce qui n'est pas le cas avec λJS. Ils ont ainsi fait disparaître un grand nombre de sucres syntaxiques dans le but de minimiser l'implémentation des fonctions pour permettre plus facilement la vérification d'un programme.

Cependant, afin de faire accepter leur noyau par les autres développeurs, il est nécessaire pour eux de prouver que n'importe quel programme écrit en JavaScript peut être réduit en un programme basé sur λJS. Pour réaliser leurs tests, l'équipe s'est basée sur trois implémentations de Javascript : SpiderMonkey (Firefox), V8 (Chrome), et Rhino (implémentation en Java). Ils ont transformé différents programmes compatibles sur ces implémentations vers un programme λJS, et ont ensuite vérifié que la sortie du nouveau programme correspond à celle de la version d'origine. Afin de couvrir un maximum de cas, les programmes sont un échantillon important de la série de test JavaScript de Mozilla[6]. Les tests ont été concluants : l'intégralité de la série de tests produit exactement le même résultat que les trois autres implémentations.

L'objectif final étant de fournir un langage sûr, il est nécessaire de fournir un outil permettant de vérifier ce résultat. Le λJS étant une implémentation simplifiée du JavaScript, et étant donné qu'un programme peut être réduit en λJS, il est nécessaire de montrer que λJS est sûr. Pour prouver ceci, ils ont décomposé chaque propriété en sous-problèmes. Pour illustrer, prenons le cas de l'addition : ils jugent qu'une addition e1 + e2 est sûre si les expressions e1 et e2 sont sûres. En posant plusieurs lemmes, ils démontrent que l'addition est sûre et qu'elle peut être incluse dans le λJS. En appliquant cette démarche sur plusieurs éléments du langage, ils ont réussi à inclure un grand nombre de fonctionnalités à leur noyau en le gardant sûr. Ceci a permis en 2012 de définir le λJS comme base pour le langage JavaScript par ECMAScript 6[7], toutefois cette version n'est pas encore totalement supportée par tous les navigateurs[8].

SAFE[10] (Scalable Framework Analysis for ECMAScript) est un projet mené par le groupe de recherche en langage de programmation de l'Institut supérieur coréen des sciences et technologies (KAIST).

Tout comme le papier précédent, l'équipe se penche ici sur le constat que la spécification informelle du langage rend celui-ci sujet à interprétation. L'équipe relève également que les différents moteurs Javascript ne sont pas assez documentés, rendant leur compréhension et leur modification difficile. Ceci était le cas avec λJS qu'ils ont souhaité utiliser : ils ont jugé que la documentation concernant la réduction du Javascript en leur noyau n'était pas assez détaillée. C'est en partant de ces deux propositions qu'ils ont débuté le projet SAFE qui a pour but d'améliorer l'analyse d'un programme Javascript ainsi que de fournir un outil documenté pour la recherche.

SAFE est développé à destination de la communauté de recherche en JavaScript, c'est un projet open-source dont le code est accessible en ligne[11]. L'implémentation est réalisée en Java et en Scala.

Comparé à l'approche de λJS, l'équipe ne s'est pas contentée de réduire un maximum de langage afin de fournir une spécification simplifiée mais a préféré réaliser une spécification de l'ensemble du langage. C'est dans ce sens qu'ils ont défini une spécification sur chaque niveau de représentation d'un programme Javascript.

Afin de réaliser leur framework, il a été dans un premier temps nécessaire de transformer le code Javascript en un code facilement analysable.

Pour ce faire, le framework se base sur 3 niveaux de représentation d'un programme Javascript. La première représentation (qui est la plus proche du code source) est un AST (Arbre syntaxique abstrait). Afin d'obtenir l'AST correspondant au code source analysé, l'équipe s'est intéressée aux parsers JavaScript existants (ANTLR[12], les combinateurs de parseur de Scala[13], Rhino, SpiderMonkey, Closure Tools[14] de Google, JSConTest[15], ou encore JSure[16]) sans trouver entière satisfaction. Elle a finalement utilisé l'outil de génération Rats! se trouvant dans le projet eXTensible Compiler[17] développé par une équipe de New York. Elle fournit à Rats! une grammaire de style BNF dont voici l'extrait[18] concernant les instructions de boucle (l'indentation représente une relation de sous-classe) :

	/**
	* SourceElement ::= Stmt
	*/
	abstract Stmt();
		/**
		* Stmt ::= do Stmt while ( Expr ) ;
		*/
		DoWhile(Stmt body, Expr cond);
		/**
		* Stmt ::= while ( Expr ) Stmt
		*/
		While(Expr cond, Stmt body);
		/**
		* Stmt ::= for ( Expr? ; Expr? ; Expr? ) Stmt
		*/
		For(Option<Expr> init, Option<Expr> cond,
		Option<Expr> action, Stmt body);
		/**
		* Stmt ::= for ( lhs in Expr ) Stmt
		*/
		ForIn(LHS lhs, Expr expr, Stmt body);
		/**
		* Stmt ::= for ( var VarDecl(, VarDecl)* ;
		*
		Expr? ; Expr? ) Stmt
		*/
		ForVar(List<VarDecl> vars, Option<Expr> cond,
		Option<Expr> action, Stmt body);
		/**
		* Stmt ::= for ( var VarDecl in Expr ) Stmt
		*/
		ForVarIn(VarDecl var, Expr expr, Stmt body);

Rats! génère alors un parser JavaScript en langage Java, qui couplé à ASTGen[19], qui génère les classes Java représentant l'AST à partir d'une description fournie, va permettre de transformer le code JavaScript en représentation intermédiaire.

Dans un second temps, le framework transforme l'AST en une représentation intermédiaire IR qui permet de fournir une spécification de chaque fonctionnalité du langage Javascript définie par ECMAScript. Par exemple, chaque fonction possède au moins l'argument this afin de respecter cette norme. C'est cette représentation qui est utilisée pour l'évaluation du programme par un interpréteur. C'est à ce niveau qu'intervient SAFE en fournissant une spécification formelle et une implémentation de chaque fonctionnalité.

Grammaire de JavaScript IR[20] :

  p ::= s*
  s ::= x = e
    |  x = delete x
    |  x = delete x [x]
    |  x = {(m,)* }
    |  x = [(e,)* ]
    |  x = x(x(, x)?)
    |  x = new x((x,)* )
    |  x = function f(x, x) { s*  }
    |  function f(x, x) { s*  }
    |  x = eval(e)
    |  x [x] = e
    |  break x
    |  return e?
    |  with (x) s
    |  x : { s }
    |  var x
    |  throw e
    |  s* 
    |  if (e) then s (else s)?
    |  while(e) s
    |  try { s } (catch (x){ s })?  (finally { s })?
    |  (s* )
  e ::= e ⊗ e
    | ɵ e
    | x [e]
    | x
    | this
    | num
    | str
    | true
    | false
    | undefined
    | null
  m ::= x : x
    | get f(x, x) { s*  }
    | set f(x, x) { s*  }
  ⊗ ::= | | & | ^ | << | >> | >>> | + | - | * | / | % | == | != | === | !== | < | > | <= | >= | instanceof | in
  ɵ ::= ~ | ! | + | - | void | typeof

Le troisième niveau de représentation est le CFG (Graphe de flot de contrôle) qui est utilisé uniquement pour l'analyse des performances. Afin de générer ce graphe, le projet utilise CFGBuilder qui est un composant du compilateur Polyglot. Ce programme prend en paramètre une représentation intermédiaire et génère un graphe correspondant qui pourra ensuite être analysé par le framework afin de réaliser plusieurs analyses.

Un exemple de transformation du code JavaScript au graphe de contrôle de flot en passant par la représentation intermédiaire, proposé dans le paragraphe 3.3 dans la publication présentant SAFE[21], illustre bien le résultat obtenu à ce stade.

Leur framework est disponible au public[22]. Afin de permettre l'utilisation de leur projet par le plus grand nombre, SAFE fournit, en plus de la spécification et d'une documentation fournie, une implémentation des différentes fonctionnalités. Ceci permet d'utiliser leurs recherches plus facilement que les autres projets qui n'ont pas ou peu de documentation.

Les 3 niveaux de représentation du code JavaScript (AST, IR, CFG) rendent SAFE plus flexible, évolutif, et connectable, proposant ainsi un outil puissant dans la recherche et le développement de JavaScript.

"Le projet JSCert a pour but de vraiment comprendre JavaScript", annonce le site du projet. Une équipe de chercheurs des laboratoires de l'INRIA et de l'Imperial College London se sont intéressés à la nécessité de clarifier les ambiguïtés liées à la longueur et aux nombreux recoins du standard ECMAScript.

JSCert est une spécification mécanisée du standard ECMAScript, écrite dans l'assistant interactif de preuve Coq[24], conçue pour être la plus proche de la norme ECMAScript5[25]. Elle se base sur le développement en 2008, mené par Sergio Maffeis, d'une sémantique de description formelle du comportement complet de JavaScript[26] suivant fidèlement ECMAScript3, à l'exception des parties ambiguës de ce standard. Cette formalisation se limite au cœur du langage JavaScript.

En parallèle a été développé JSRef, un interpréteur exécutable de référence, certifié dans le respect de JSCert, et testé en utilisant la suite de tests de confirmité d'ECMAScript, test262[27].

JSCert n'est pas directement utilisable, de par sa conception : c'est une définition inductive à destination du développement de preuves de sûreté, qui compense l'imprécision concernant les fonctionnalités dépendantes de l'implémentation dans ECMAScript5. En tant que spécification Coq calculable, on en a extrait automatiquement le code OCaml correspondant, obtenant ainsi l'interpréteur JSRef. Celui-ci respecte la norme ECMAScript5 autant qu'il était possible de la formaliser par JSCert.

La vérification de JSCert dans cette sémantique mécanisée est dû à sa proximité avec la norme ECMAScript5 : la prose anglaise de celle-ci et les règles formelles qui en découlent peuvent être mises côte-à-côte, chaque ligne de pseudo-code correspondant à une ou deux règles formelles de JSCert. JSRef se vérifie par le mécanisme automatique par lequel il est extrait de JSCert.

Le pseudo-code[28] correspondant à la boucle while dans ECMAScript5 :

	1. Let V = empty.
	2. Repeat
	   a. Let exprRef be the result of evaluating Expression.
	   b. If ToBoolean(GetValue(exprRef)) is false, return (normal,V,empty).
	   c. Let stmt be the result of evaluating Statement.
	   d. If stmt.value is not empty, let V = stmt.value.
	   e. If stmt.type is not continue || stmt.target is not in the current label set, then
	       i. If stmt.type is break and stmt.target is in the current label set, then return (normal,V,empty).
	      ii. If stmt is an abrupt completion, return stmt.

La sémantique JSCert implémentée dans Coq correspondant à la boucle while, et traduisant la sémantique définie dans la publication de JSCert[29] :

	(* Step 1: red_while_1 *)
	| red_stat_while : forall S C labs e1 t2 o,
		red_stat S C (stat_while_1 labs e1 t2 resvalue_empty) o ->
		red_stat S C (stat_while labs e1 t2) o
	(* Steps 2a and 2b: red_while_2a_2b *)
	| red_stat_while_1 : forall S C labs e1 t2 rv y1 o,
		red_spec S C (spec_expr_get_value_conv spec_to_boolean e1) y1 ->
		red_stat S C (stat_while_2 labs e1 t2 rv y1) o ->
		red_stat S C (stat_while_1 labs e1 t2 rv) o
	(* Step 2b False: red_while_2b'_false *)
	| red_stat_while_2_false : forall S0 S C labs e1 t2 rv,
		red_stat S0 C (stat_while_2 labs e1 t2 rv (vret S false)) (out_ter S rv)
	(* Step 2b True and 2c: red_while_2b'_true_2c *)
	| red_stat_while_2_true : forall S0 S C labs e1 t2 rv o1 o,
		red_stat S C t2 o1 ->
		red_stat S C (stat_while_3 labs e1 t2 rv o1) o ->
		red_stat S0 C (stat_while_2 labs e1 t2 rv (vret S true)) o
	(* Step 2d: red_while_2d *)
	| red_stat_while_3 : forall rv S0 S C labs e1 t2 rv' R o,
		rv' = (If res_value R <> resvalue_empty then res_value R else rv) ->
		red_stat S C (stat_while_4 labs e1 t2 rv' R) o ->
		red_stat S0 C (stat_while_3 labs e1 t2 rv (out_ter S R)) o
	(* Step 2e False: red_while_2e_false *)
	| red_stat_while_4_continue : forall S C labs e1 t2 rv R o,
		res_type R = restype_continue /\ res_label_in R labs ->
		red_stat S C (stat_while_1 labs e1 t2 rv) o ->
		red_stat S C (stat_while_4 labs e1 t2 rv R) o
	(* Step 2e True: red_while_2e_true *)
	| red_stat_while_4_not_continue : forall S C labs e1 t2 rv R o,
		~ (res_type R = restype_continue /\ res_label_in R labs) ->
		red_stat S C (stat_while_5 labs e1 t2 rv R) o ->
		red_stat S C (stat_while_4 labs e1 t2 rv R) o
	(* Step 2e i True: red_while_2e_i_true *)
	| red_stat_while_5_break : forall S C labs e1 t2 rv R,
		res_type R = restype_break /\ res_label_in R labs ->
		red_stat S C (stat_while_5 labs e1 t2 rv R) (out_ter S rv)
	(* Step 2e i False: red_while_2e_i_false *)
	| red_stat_while_5_not_break : forall S C labs e1 t2 rv R o,
		~ (res_type R = restype_break /\ res_label_in R labs) ->
		red_stat S C (stat_while_6 labs e1 t2 rv R) o ->
	red_stat S C (stat_while_5 labs e1 t2 rv R) o
	(* Step 2e ii True: red_while_2e_ii_true *)
	| red_stat_while_6_abort : forall S C labs e1 t2 rv R,
		res_type R <> restype_normal ->
		red_stat S C (stat_while_6 labs e1 t2 rv R) (out_ter S R)
	(* Step 2e ii False: red_while_2e_ii_false *)
	| red_stat_while_6_normal : forall S C labs e1 t2 rv R o,
		res_type R = restype_normal ->
		red_stat S C (stat_while_1 labs e1 t2 rv) o ->
		red_stat S C (stat_while_6 labs e1 t2 rv R) o

La sémantique JSRef de la boucle while[30] :

Definition run_stat_while runs S C rv labs e1 t2 : result :=
	if_spec (run_expr_get_value runs S C e1) (fun S1 v1 => 
		Let b := convert_value_to_boolean v1 in
			if b then
				if_ter (runs.runs_type_stat S1 C t2) (fun S2 R =>
					Let rv' := ifb res_value R != resvalue_empty
						then res_value R else rv in
							Let loop := fun _ => runs.runs_type_stat_while S2 C rv' labs e1 t2 in
								ifb res_type R != restype_continue
									|| res_label_in R labs
								then (ifb res_type R = restype_break
										&& res_label_in R labs
									then res_ter S2 rv'
									else (ifb res_type R != restype_normal
										then res_ter S2 R else loop tt))
								else loop tt)
						else res_ter S1 rv).
Definition run_stat runs S C t : result :=
	match t with
	|stat_while ls e1 t2 => runs.runs_type_stat_while S C ls e1 t2 resvalue_empt...

On peut envisager plusieurs utilisations potentielles de JSCert et JSRef :

• analyser des morceaux de code JavaScript
• vérifier la bonne implémentation d'un compilateur d'un langage de plus haut niveau en JavaScript
• comparer l'implémentation d'un interpréteur avec celle de JSRef

On peut imaginer que cette spécification formelle et mécanisée soit intégrée dans une future édition d'ECMAScript.

(en) Arjun Guha, Claudiu Saftoiu et Shriram Krishnamurthi, « The Essence of JavaScript », ECOOP '10 Proceedings of the 24th European conference on Object-oriented programming,‎ 21 juin 2010, p. 126-150 (ISBN 3-642-14106-4 et 978-3-642-14106-5, lire en ligne)

(en) Hongki Lee, Sooncheol Won, Joonho Jin, Junhee Cho et Sukyoung Ryu, « SAFE: Formal Specification and Implementation of a Scalable Analysis Framework for ECMAScript », FOOL '12 Foundations of Object-Oriented Languages,‎ 22 octobre 2012 (DOI 10.1.1.387.1030, lire en ligne)

(en) Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudžiuniene, Alan Schmitt et Gareth Smith, « A Trusted Mechanised JavaScript Specification », POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,‎ 22 janvier 2014 (ISBN 978-1-4503-2544-8, DOI 10.1145/2535838.2535876, lire en ligne)

(en) Sergio Maffeis, John C. Michell et Ankur Taly, « An Operational Semantics for JavaScript », APLAS '08,‎ 2008 (lire en ligne)

• JavaScript
• ECMAScript