JStify — Appel à commentaires

October 15, 2007 § 1 Comment

Ce billet est une description de JStify, un outil que je suis en train de développer. Une fois complet, JStify sera une boîte à outils pour l’analyse statique de programmes écrits dans le langage JavaScript 2. Cette boîte à outils s’adressera aussi bien aux développeurs web qu’aux développeurs d’extensions Firefox. JStify pourra être inclus dans des applications côté client ou côté serveur et pourra être étendu avec de nouveaux types d’analyse.

Ceci est un appel à commentaires. N’hésitez pas à me faire part de vos remarques — je préférerais découvrir mes erreurs maintenant que dans deux ans.

Reprenons avec un peu plus de détails

L’objectif

JStify (prononcez “justify” ou “jestify” selon votre humeur) sera une boîte à outils pour l’analyse statique de programmes JavaScript 2. En d’autres termes, JStify contiendra un certain nombre d’outils qui pourront servir à examiner le contenu d’un programme sans avoir à le lancer — et en déduire des informations sur la manière dont le programme fonctionne, ce qu’il peut faire et ce qu’il ne peut pas faire. Certains types d’analyse seront fournis avec JStify, alors que d’autres devront être construits à l’aide de JStify.

L’analyse statique ne remplace pas le test, mais elle est fondamentale :

  • la vérification automatique d’erreurs bien connues peut faire gagner beaucoup de temps aux développeurs
  • la vérification automatique de propreté, de commentaires… peut aider les développeurs débutants à prendre de bonnes habitudes et les équipes de développeurs à adopter des conventions communes
  • la vérification automatique de problèmes de sûreté est critique pour, mettons, addons.mozilla.org, ou pour les dépôts de widgets de Opera ou Safari — imaginez que vous proposez votre extension/widget et que, quelques minutes plus tard, un e-mail vous arrive “Nous avons trouvé dans votre code quelque chose qui ressemble à un problème, du coup, nous ne pouvons pas accepter votre soumission dans l’état actuel. Pourriez-vous jeter un œil à la ligne XXX du fichier YYY et réécrire la fonction pour la rendre plus sûre contre une attaque de type ZZZ ? Avec un peu de chance, il vous suffira d’ajouter la ligne suivante : <Insérer ici une assertion automatiquement générée>.”

Plus tard, JStify sera complété à l’aide d’outils de réécriture de code, qui permettront de modifier automatiquement le code source d’un programme de manière complexe si nécessaire, par exemple pour forcer à employer un style donné ou pour ajouter des vérifications dynamiques avant des appels potentiellement dangereux.

Ce second aspect est, lui aussi, fondamental, car il pourra servir à écrire des modules pour :

  • porter automatiquement du code depuis JavaScript vers des sous-ensembles sûrs tels que ADsafe
  • porter automatiquement du code de JavaScript 1.x vers le style plus sûr JavaScript 2
  • éliminier automatiquement certaines faiblesses connues
  • …et, si nécessaire, porter automatiquement du code de JavaScript 2 vers JavaScript 1.

Plus d’informations ?

Techniquement, JStify est un ensemble de modules pour OCaml.

Les modules de base se chargement de

  • l’analyse lexicale et syntaxique de JavaScript 2
  • l’analyse lexicale et syntaxique des annotations ajoutées par le développeur
  • parcourir l’arbre syntaxique d’un programme JavaScript 2
  • résoudre les noms, c’est-à-dire, lorsque vous examinez une variable i, trouver de quelle variable il s’agit
  • remonter le flux de l’information, c’est-à-dire trouver d’où vient une variable ou un argument
  • ajouter des informations syr les symboles au fur et à mesure qu’ils sont rencontrés et examinés
  • accéder au code source des fonctions pour les ré-examiner si nécessaire lorsqu’elles sont utilisées, pour pouvoir bénéficier d’informations contextuelles
  • afficher avertissements et messages d’erreur.

Des modules additionnels, construits à partir des précédents, ajouteront progressivement des informations qui pourront servir à raffiner ces vérifications. Nous commencerons par

  • appliquer l’algorithme standard de vérification de types de JavaScript 2
  • réimplanter les vérifications de JSLint
  • plus tard, ajouter l’analyse des appels XPCom.

Encore plus tard, des modules de réécriture seront ajoutés, qui permettront de

  • modifier l’arbre syntaxique
  • modifier les annotations
  • sauvegarder l’arbre syntaxique obtenu
  • exporter un arbre syntaxique vers du XML (pour affichage ou manipulation dans d’autres programmes).

Although this is not their primary purpose, it will be possible to use these modules to generate (possibly annotated) JavaScript from other languages.

État actuel

Le développement de JStify vient de commencer. J’espère disposer d’un prototype d’ici l’été.

Des questions ?

Que signifie “JStify” ?

Pour l’instant, pas grand chose. Je n’ai rien trouvé de mieux que “JavaScript, Trace Information Flow ! Yessir !” Mike Shaver suggère “JavaScript Traces Information For You”.

Pourquoi OCaml ?

Parce que OCaml est le meilleur compromis que je connaisse entre

  • du code propre et concis pour la manipulation de langages de programmation — je n’écrirais pas des dizaines de milliers de lignes de parcours d’arbre sans filtrage par motifs ou ramasse-miettes
  • vérification statique de mon code — je n’écrirai pas des dizaines de milliers de lignes de manipulation de structures de données sans typage statique et fort
  • débogage — et je n’écrirai pas ces dizaines de milliers de lignes de code sans printf
  • extension — toujours pas de dizaines de milliers de lignes de code sans un beau système de macros
  • hautes performances et faible consommation en mémoire — pour pouvoir utiliser JStify sur un serveur web, qui a déjà beaucoup à faire.

Alors maintenant, il aurait été possible de choisir d’autres langages de programmation.

Et pourquoi pas en JavaScript ?

JavaScript est un beau langage fortement maltraité. Cela dit, malgré toutes ses qualités réelles et tous les mauvais traitements auxquels il est soumis par des gens qui essayent de l’appliquer à des tâches qui ne sont pas de ressort, JavaScript (même JavaScript 2) n’est pas conçu pour la manipulation de langages de programmation. Lisp ou ML (la famille de langages dont est tiré OCaml), si.

Cela dit, il est possible d’appeler du JavaScript depuis du OCaml, ce qui devrait déjà permettre de scripter un minimum JStify depuis JavaScript. J’espère aussi que quelqu’un voudra bien, un jour, écrire un pont XPCom-OCaml, qui permettra d’employer JStify depuis Firefox ou XulRunner sans avoir à passer par du C.

Pourquoi pour JavaScript ?

Parce que JavaScript est un langage intéressant, dont la popularité ne cesse d’augmenter. Ce langage est employé pour développer le côté client d’applications web telles que GMail ou Google Maps, le côté serveur d’autres applications web ou encore des applications de bureau telles que Firefox, Thunderbird, Nvu/Kompozer, Songbird, des extensions pour Firefox, Opera, Safari, le Dashboard de MacOS X, des contrôles pour téléphones portables…

Avec JavaScript 2, le langage se donne de quoi devenir un acteur majeur, quelque part entre Java ou C# (du côté des langages assez-fortement-typés) et Python ou Ruby (du côté des langages dynamiques).

Puis-je utiliser JStify dans Eclipse ?

Il y a plusieurs manières d’appeler OCaml depuis Java, qui permettront de construire un plug-in Eclipse à partir de JStify. Cela dit, ce n’est pas ma priorité. Si quelqu’un veut s’en charger, il sera reçu avec plaisir.

Quelle est la différence avec JSLint ?

JSLint et JStify sont tous les deux des vérificateurs conduits par la syntaxe. Entre les deux, deux différences principales :

  • JSLint existe déjà et est parfaitement utilisable, JStify pas encore ;
  • avec JStify, nous comptons aller bien plus loin, permettre la vérification de propriétés de bien plus haut niveau, combiner plusieurs types de vérifications spécifiées par l’utilisateur, de la réécriture…

Cela dit, nous comptons bien adapter tout ce que fait JSlint à JStify.

Un moment. Lors d’un appel de méthode, comment faites-vous pour déterminer quelle méthode est effectivement invoquée ? Je peux remplacer des méthodes dynamiquement !

En général, c’est impossible, d’autant plus que le remplacement d’une méthode peut être causé par l’interaction entre plusieurs programmes. Par contre, nous pouvons déterminer si une méthode est protégée ou si toutes les méthodes qui semblent pouvoir remplacer une méthode ont les mêmes propriétés utiles.

Cela dit, ces deux formes de vérification sont de niveau relativement avancé — elles n’apparaîtront pas dans la première version de Jstify.

Est-ce un outil de vérification de types ? Un outil d’inférence de types ?

Ni l’un ni l’autre. JStify est un support qui devra permettre de construire des outils d’analyse et en particulier des outils de vérification (et d’inférence) de types.

Mais, mais… mais à peu près toutes les propriétés intéressantes sont indécidables, non ?

Oui. L’objectif est donc de construire des approximations raisonnables. Reste à décider si ces approximations doivent garantir qu’un programme est correct, quitte à refuser des programmes incorrects, ou le contraire. Chaque développeur de module d’analyse devra faire ce choix.

Comment prouverez-vous vos analyses ?

Précisons une chose importante : JStify lui-même est une boîte à outils conçue pour permettre aux développeurs d’écrire leurs propres analyseurs. À ce niveau-là, il n’est pas intéressant d’écrire des preuves, puisqu’il n’y a aucun moyen de garantir que les développeurs écriront des choses mathématiquement cohérentes.

Maintenant, JStify contiendra un certain nombre d’analyseurs standard. Ce ne sera pas une priorité mais, lorsque le temps le permettra, j’essayerai de prouver la validité de ces analyseurs (en termes techniques la Réduction du Sujet). C’est envisageable grâce à l’implantation de référence fonctionnelle de JavaScript 2. Des propriétés de validité ont été prouvées pour un sous-ensemble de JavaScript 1.x nommé JS0 mais il a fallu des années pour en arriver là. Nous espérons que l’implantation de référence simplifiera les choses.

Il sera envisageable de combiner JStify et un intepréteur de JavaScript 2 pour créer un outil de vérification de systèmes de types (en fait, une forme d’interpréteur abstrait), mais ça risque d’attendre quelques années au mieux.

Pourquoi vérifier des propriétés de sécurité sur JavaScript ? JavaScript est déjà sûr, non ?

Non. JavaScript est plus sûr que d’autres langages, essentiellement parce qu’il n’y a pas accès aux fonctions de bas niveau, mais cette sûreté est loin d’être parfaite — il suffit de se souvenir des nombreuses failles inter-sites (Cross-Site Scripting exploits). De plus, JavaScript est le langage principal pour le développement d’extensions Firefox. Pour ce genre d’usages, JavaScript a accès à une bibliothèque de programmation importante et potentiellement dangereuse, puisqu’elle permet de gérer les fichiers les processus, etc. Cela rend JavaScript aussi dangereux que n’importe quel autre langage de programmation.

Qui paye ?

Je suis un chercheur, ceci fait partie de mes activités. Cela dit, je n’ai pas la possibilité matérielle de travailler sur JStify à plein temps, puisque je suis aussi enseignant et puisque je suis impliqué directement ou non dans plusieurs projets.

Quelle est la licence ?

Pas tout à fait décidé. Probablement MPL/GPL/LGPL.

Besoin d’aide ?

Clairement, mais pas tout de suite. Si vous voulez donner un coup de main, laissez un commentaire ou votre mail, je vous recontacterai le moment venu.

Où est le code ?

Pas encore disponible, mais ça viendra. En fait, c’est juste un problème technique, le temps que le laboratoire décide comment organiser son GForce.

Il ne manque pas des remerciements ?

Ah, oui. L’idée initiale pour JStify vient d’une discussion avec Taras Glek. L’objectif de JStify est proche de son travail sur squash and dehydra — mais en JavaScript, alors que lui travaille sur C++.

Qu’est-ce que c’est que JavaScript 2 ?

JavaScript 2 est la prochaine version de JavaScript, un langage dynamique compris par la quasi-totalité des navigateurw web et qui sert à ajouter de l’interactivité aux pages web. JavaScript 2 n’est pas encore tout à fait prêt — a fortiori pas encore totalement compris par les navigateurs. Le prototype final est attendu sous peu et on espère que les navigateurs suivront en 2008. En particulier, il semble assez probable que Firefox adopte JavaScript 2 très rapidement, aussi bien pour le web que pour les extensions.

Pour plus d’informations sur JavaScript 2, vous pouvez vous renseigner sur

Quel genre de problèmes de sécurité pourrait-on détecter avec JStify ?

Voyons un peu…

D’abord, des choses simples :

  • pas d’eval() ni d’équivalent
  • pas de XPCom

Plus tard, des choses plus complexes et plus utiles :

  • pas d’appel certains composants ou interfaces XPCom (ex. nsIFile, nsIDebug, nsIRegistry)
  • pas d’appels à certaines méthodes de certains composants
  • pas de (re)définition de composants “@mozilla.org/*”
  • pas d’exécution de code téléchargé par XMLHttpRequest

Encore plus tard, des tests plus précis (et fortement indécidables) :

  • s’assurer que toutes les utilisations de nsIFile n’accèdent qu’à certains fichiers sûrs
  • s’assurer qu’aucune autre extension ne sera modfiée

Et, bien entendu, des propriétés pas-tout-à-fait-de-sécurité telles que :

  • chaque fichier ouvert doit être refermé
  • chaque exception doit être rattrapée quelque part

S’il n’y a pas de code, ce n’est pas un peu tôt pour mettre en ligne une description aussi précise ?

L’idée est d’avoir les commentaires avant de faire les bêtises.

Tagged: , , , , , , ,

§ One Response to JStify — Appel à commentaires

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

What’s this?

You are currently reading JStify — Appel à commentaires at Il y a du thé renversé au bord de la table.

meta

Follow

Get every new post delivered to your Inbox.

Join 31 other followers

%d bloggers like this: