Analyse statique de code dynamique

JavaScript : un langage dynamique et flexible

Un langage très dynamique JavaScript est un langage impératif orienté objet, à l’instar de C++ ou Java. À la différence de ces langages, en revanche, il n’existe pas de notion de classe en JavaScript. Les relations entre différents types d’objets sont dictées par des prototypes. Les prototypes sont des objets qui représentent un équivalent d’une super-classe (ou classe mère) en programmation objet à classes. Par exemple, lorsque l’on cherche une propriété dans un objet, on cherche d’abord dans l’objet lui-même puis, si la propriété est absente, on va chercher dans son prototype, et ainsi de suite jusqu’à trouver l’objet ou arriver au bout de la chaîne de prototypes. La différence principale par rapport à un langage à classes est la suivante : en Java par exemple, la hiérarchie de classes est statique. En effet, si A est une sous-classe de B, cela restera ainsi pendant toute l’exécution. En JavaScript, cette hiérarchie est dynamique. On peut, au cours de l’exécution, affecter C comme nouvelle valeur du prototype de A. De plus, comme évoqué en introduction, tous les objets sont mutables par défaut en JavaScript, en particulier les objets natifs. Ainsi, il est possible de modifier le comportement des objets natifs, en modifiant leur prototype. Par exemple, on peut modifier le comportement de Object, dont héritent tous les objets en JavaScript. Changer la valeur de Object.prototype.toString modifiera le comportement de tous les objets. Un langage difficile à analyser Cette flexibilité est appréciable des développeurs JavaScript, mais elle entraîne de nombreuses vulnérabilités, dont le risque est d’autant plus grand que JavaScript est puissant. La plus connue de ces vulnérabilités est le cross-site scripting (XSS), dont on a parlé en introduction, qui permet d’injecter du code dans une page qui ne nous appartient pas. Du fait que JavaScript est un langage très dynamique, il est difficile de mener des analyses statiques sur ce genre de programmes.

Analyse de flux d’information

Les propriétés de flux d’information permettent d’interdire des flux considérés dangereux. Ces propriétés sont de deux types différents : on peut vouloir garantir que des informations non fiables s’insèrent dans le script (intégrité), ou bien que des informations confidentielles soient révélées (confidentialité).
Intégrité du programme : La première catégorie concerne les propriétés d’intégrité : on ne veut pas que des informations non fiables s’infiltrent dans des fonctions critiques. Comme on l’a vu en introduction, on peut en JavaScript accéder au DOM et ainsi écrire sur la page. On peut imaginer une instruction du type monElement.innerHTML = champ.text qui va affecter au champ innerHTML de l’élément monElement le texte contenu dans le champ de texte champ. Le champ innerHTML représente la structure HTML d’un élément. Ainsi, modifier ce champ modifiera directement la structure interne du document HTML. Il faut donc faire attention à ce à quoi on l’affecte : on peut très bien insérer un script malicieux.
La solution proposée par Guarniera et coll est une analyse de teintes permettant d’éviter ce genre de flux. L’analyse de teintes considère plusieurs types d’élements :
les sources : ce sont les données d’entrée, typiquement non fiables, dans notre exemple champ.text est une source ;
les puits : ce sont les locations sensibles, dans lesquels on ne veut mettre que des informations de confiance, dans notre exemple monElement.innerHTML est un puits ;
les sanitizers : ce sont des fonctions qui permettent de rendre des données issues d’une source invulnérables. Dans notre exemple, la fonction escape(), qui permet d’échapper les caractères spéciaux, pour les faire apparaître comme du texte, est un sanitizer.
Les auteurs automatisent le processus d’identification des sources, puits et sanitizers en utilisant des règles du type : le champ innerHTML d’un objet est toujours un puits. L’analyse consiste ensuite à teinter les variables sources, puis à propager la teinte sur les variables auxquelles on affecte des valeurs teintées.
Une fois cette propagation effectuée, on vérifie si les puits sont teintés : si oui, le programme est potentiellement vulnérable, sinon il est sain.

Utilisation d’analyses statique et dynamique pour transformer le code

D’autres travaux permettent de transformer eval en code statique. Meawad, Richards, Morandat et Vitek proposent une solution qui s’appuie sur des informations obtenues à la fois statiquement et dynamiquement.
On commence par naviguer sur la page à tester à travers un proxy nommé Evalorizer. Le proxy établit un journal des appels à eval qui apparaissent sur la page et dans les fichiers inclus. Ce journal contient une liste de triplets (fichier,ligne,appel). Cela constitue ce que les auteurs appellent le journal statique. Le proxy instrumente les appels à eval pour enregistrer, lors de chaque appel, les chaînes données en argument à eval, ce qui constituera le journal dynamique. Pour le construire, un utilisateur parcourt la page en essayant d’activer tous les appels à eval cachés dans du code exécuté après un clic sur un bouton par exemple.
À ce stade, on a donc pour chaque appel à eval le nom du fichier et la ligne à laquelle il apparaît, ainsi qu’un échantillon de valeurs passées en paramètre. Pour chaque valeur passée en paramètre, on crée une représentation sous forme d’arbre de syntaxe abstrait (AST pour Abstract Syntax Tree). Si on a plusieurs valeurs possibles pour un même appel, on fusionne les deux AST avec un nœud de choix (OU) à la racine. Par la suite, on pourra raffiner cette fusion. Par exemple, si les chaînes passées à eval sont window.width et window.height, on va générer l’AST : OU(.(window,width),.(window,height)). On peut raffiner ceci par .(window,OU(width,height)). On peut aller encore plus loin en généralisant width et height par n’importe quel identifiant de champ, ce qui est une abstraction suffisante pour transformer ce type d’appel à eval.

Analyse d’isolation dans des mashups

On trouve souvent sur les pages web plusieurs scripts qui interagissent. Par exemple, un script JavaScript qui affiche de la publicité en lien avec la page visitée inspecte la page dans laquelle il est inséré pour deviner les intérêts du visiteur. Ou encore lors d’une recherche quelconque, on peut trouver un script tiers qui affiche un plan de l’adresse recherchée, avec éventuellement un itinéraire à partir de la localisation de l’utilisateur si disponible. On appelle mashups ces pages où différents scripts interagissent.
Pour insérer différents scripts sur une même page, on a classiquement deux solutions : mettre les différents scripts dans des iframes différents : les communications entre scripts sont soumises à la Same Origin Policy (SOP) : un script ne peut interagir qu’avec des documents venant de la même origine, c’est-à-dire le même sous-domaine, avec le même protocole et le même port de communication ; laisser les scripts communiquer librement en les plaçant dans la même iframe : on ne peut garantir aucune propriété de sécurité.
Pour faire interagir des scripts afin d’enrichir le contenu des sites web, on doit alors les placer dans une même iframe, ce qui pose des problèmes de sécurité. Plusieurs travaux proposent des alternatives plus souples.

Sémantique de JavaScript

Notre but est de faire de l’analyse statique de JavaScript pour prouver des propriétés de sécurité. L’analyse statique s’appuie sur un modèle du programme (i.e. pas le programme lui-même) et raisonne sur ce modèle grâce à des règles de sémantique. La première étape du stage est donc d’écrire une sémantique de JavaScript. Plusieurs travaux existants visent à définir une sémantique de JavaScript. En effet, la spécification officielle est relativement verbeuse (250 pages en langage naturel) et ne permet pas de faire des analyses formelles. Maffeis, Mitchell et Taly ont écrit une sémantique formelle correspondant à la spécification officielle. Pour établir cette sémantique, les auteurs ont interprété la spécification officielle de la manière qui leur semblait la plus naturelle, puis ils ont testé les comportements de différents navigateurs (Mozilla Firefox, Internet Explorer, Safari, Opera et l’interpréteur JavaScript pour Java, Rhino). Cette sémantique a l’avantage de définir le comportement entier de JavaScript, contrairement à d’autres travaux qui ne s’intéressent qu’à un sous-ensemble du langage. Cependant, elle est plutôt volumineuse (70 pages de règles formelles). Il est donc possible de mener des analyses statiques avec cette sémantique, cependant sa formalisation en un langage informatique utilisable pour analyser automatiquement des programmes est difficile .

Table des matières

Introduction 
1 État de l’art 
1.1 JavaScript : un langage dynamique et flexible
1.2 Analyse de type
1.3 Analyse de flux d’information
1.4 Analyse de eval
1.5 Analyse d’isolation dans des mashups
2 Systèmes de réécriture
2.1 Un exemple de système de réécriture
2.2 Définition formelle
2.3 Application à l’analyse statique
3 Sémantique de JavaScript 
3.1 Valeurs manipulées
3.2 État du programme
3.3 Langage noyau
3.4 Objets
3.5 Fonctions
3.6 La fonction eval
3.7 Tests
4 Preuve automatique d’isolation de programmes JavaScript 
4.1 Objectif de l’analyse
4.2 Adaptation de la propriété à λJS
4.3 Automates d’arbres
4.4 Timbuk : un outil de réécriture sur des automates d’arbres
4.5 Cadre expérimental
4.6 Résultats
Conclusion 
Références 
A Découverte d’une anomalie dans Timbuk

Télécharger le rapport complet