JStify — Request For Comments

October 11, 2007 § 8 Comments

Note Je mettrai en ligne sous peu une version française de ce billet.

This entry contains the description of JStify, a tool I’m currently developing. When complete, JStify will be a static analysis toolbox for the JavaScript 2 language, targetted towards both web-developers and Firefox extension developers. JStify will be embeddable inside both desktop applications and server-side applications and will support pluggable analysis modules.

This is a request for comments, so please don’t hesitate. I’d rather answer questions and find out about potential pitfalls now than after two years of work.

Let’s restart with more details

The objective

JStify (pronounce “justify” or “jestify” depending on your mood) will be a static analysis toolbox for JavaScript 2. In other words, a number of tools that one may use to examine the contents of a program without having to run it, and deduce things about how that program works and what it can or can’t do. Some checks will be built-in JStify, while others will need to be written using JStify.

Although it won’t replace testing, this type of analysis is primordial, as

 

  • automatic checking of well-known errors may save lots of time to the developer
  • automatic checking of cleanliness and other metrics may help both newbie developers and teams a lot
  • automatic checking of security issues is critical for, say, addons.mozilla.org, or for Opera’s or Safari’s widget repositories — imagine uploading your extension/widget and receiving within seconds an e-mail stating that “Hey, we’ve noticed a potential security flaw in your code, so we’re not going to accept it as such. Could you please look at line XXX of file YYY.js and rewrite the function to make it safer from an attack such as ZZZ ? Chances are that pasting the following line will be sufficient. <Here, insert an automatically-generated assertion>.”

At a later stage, JStify will also include rewriting tools, that will allow automatically modifying the source code of a program in non-necessarily trivial ways, for instance to automatically add assertions before potentially dangerous calls, or for enforcing style.

This second aspect is also primordial, as, the appropriate modules will allow

 

  • automatic porting of code from general JavaScript to safe(r) subsets such as ADsafe
  • automatic porting of code from JavaScript 1.x style to the safer JavaScript 2 style
  • automatic elimination of well-known (albeit perhaps recently discovered) weaknesses
  • …and if necessary, automatic backporting of code from JavaScript 2 to JavaScript 1.

More details

Technically, JStify is a set of OCaml modules.

The base modules take charge of

 

  • lexing and parsing JavaScript 2
  • lexing and parsing user-added annotations (in comments)
  • walking through the syntax tree of a JavaScript 2 program
  • resolving names, i.e. to find out which variable named i you’re currently examining
  • tracing information flow, i.e. to find out where that argument named file_name comes from (usually several possibilities)
  • adding information on symbols (functions, variables, methods, fields) as they’re encountered / examined
  • accessing the source of functions to re-examine them if necessary when they’re used, so as to be able to type them “in context”
  • spitting-out errors and warnings.

Additional modules, written on top of these modules, will progressively add informations which may then be used to refine checks. We will start with

 

  • applying JavaScript 2′s standard type-checking algorithm
  • reimplementing JSLint’s checks
  • later, adding analysis of XPCom (system) calls.

At a later stage, rewriting modules will be added, allowing among other things to

 

  • modify the syntax tree
  • modify the comments to add annotations
  • save a syntax tree
  • pretty-print JavaScript
  • export a syntax tree to XML (for pretty-printing or manipulation by other programs).

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

Current status

JStify is currently in early development stage. I hope to have a first prototype by the summer.

Any questions ?

Does “JStify” mean anything ?

For now, my best attempt is “JavaScript, Trace Information Flow ! Yessir !” If you have better ideas, I’m listening.

Update

Mozilla’s Mike Shaver suggests “JavaScript Traces Information For You”.

Why OCaml ?

Because OCaml is the best trade-off I know between

 

  • clean and concise programming for programming language-related stuff — and I’m not going to write several 10k lines of tree walking without pattern-matching and garbage-collection
  • static checking of my code — and I’m not going to write several 10k lines of data structure manipulation without static checking of my data structures
  • debuggability — and I’m not going to write several 10k lines of code without printf
  • extendability — and I’m not going to write several 10k lines of code without the possibility of developing my own type-safe macros
  • high performance and low memory usage — because I want JStify to be usable on a server.

Now, other languages would have been acceptable, too.

Why not writing it JavaScript ?

Because despite all its qualities, JavaScript (even JavaScript 2) is not designed for manipulation of programming-language constructs. Lisp and ML have been designed with this in mind, and it shows.

On the other hands, I intend to take advantage of the OCaml-SpiderMonkey bindings to give a degree of scriptability from JavaScript.

Why for JavaScript ?

Because JavaScript is an interesting language, with growing popularity. It’s used to develop client-side web applications, including GMail, Google Maps, as well as server-side web applications, but also desktop applications such as Firefox, Thunderbird, Nvu/Kompozer, Songbird, and extensions for Firefox, Opera, Safari, MacOS X’ Dashboard, etc.

With JavaScript 2, the language becomes a serious contender in the world of programming languages, somewhere between Java and C# (on the side of rather-strongly-typed languages) and Python and Ruby (on the side of dynamic languages).

Can I use it in Eclipse ?

There are several ways to call OCaml from Java, which may be used to build an Eclipse plug-in from JStify. I’m not going to do it myself, though.

What is the difference with JSLint ?

Both JSLint and JStify are syntax-driven checkers. With JStify, however, we’re planning to go beyond, supporting much higher-level checking, plus combining several types of user-defined checks, plus rewriting… On the other hand, we’re very much planning to adapt everything JSlint does to JStify. And if Douglas Crockford is reading this, working with you on this would be nice.

How can you determine which method is being called ? I can replace methods dynamically !

Usually, we can’t, because that can happen due to interactions with other programs. What we can do, on the other hand, is determine if a method is somehow protected or, if all the methods that seem to be able to replace it share the same “useful trait”.

But determining which methods are protected is effectively an advanced question. It’s not going to be built-in the first set of modules we deliver. That’s going to be an additional layer on top of these modules, and we’re going to need lots of experimentations before we’re sure of what we’re doing there.

Is it a type-checker ? Does it perform Hindney-Milner type inference ?

It’s not a type-checker, but it’s designed so as to simplify writing type checkers. I, for one, will use it for that purpose.

But, but, any useful check is undecidable !

Indeed. Most static checks are undecidable. We’re going to go for conservative approximations.

How are you going to prove your checks ?

Let’s introduce a distinction here. JStify itself is, first and foremost, a generic toolbox designed to let people write their own checkers. Proofs at this level would be essentially meaningless — there is no way of enforcing that everything people are going to do with the toolbox will be mathematically consistent.

Now, JStify will be delivered with a number of standard checkers. While this is not a priority, I will try and prove that these checks are consistent (in technical terms, that Subject Reduction holds). This might be possible due to the fact that JavaScript 2 has a reference implementation written in ML. Subject Reduction properties have been proved for a type system designed around JS0, a subset of JavaScript 1.x, but have taken years of work. Hopefully, the reference implementation will make things easier.

It is conceivable that JStify could be combined with a JS 2 interpreter so as to create a type system checker (actually a form of abstract interpreter), but that’s a distant objective at best.

But JavaScript is already safe, isn’t it ?

No, it’s not. It’s safer than most languages, because it doesn’t have access to low-level functions, but this safety is far from perfect. Take, for instance, Cross-Site Scripting exploits. In addition, JavaScript is used as the main language for the development of Firefox extensions, and for this usage, JavaScript has access to the unbriddled library known as XPCom, with APIs for file management, process management, etc. This makes JavaScript just about as unsafe as anything else.

Who’s funding this ?

I’m a researcher. This is part of my activities. I’m not full-time on this, mind you. I’m working on several projects at once, some of them also related to JavaScript security, plus teaching.

What’s the license ?

Not completely decided. Probably triple-license MPL/GPL/LGPL.

Do you need help ?

Definitely, but not right now. If you want to help, drop a line, I’ll recontact you when time is right.

Where is the code ?

Not available yet. Initially, I planned to put it on SourceForge, but by lab is considering getting a publically-accessible GForge, so I’m not uploading the code yet. Anyway, it’s still very early in its development.

Aren’t you forgetting to quote someone ?

Oh, yeah, I forgot that the initial idea for JStify comes from a discussion with Taras Glek and that what I’m trying to do is quite similar to his work on squash and dehydra — except JStify is for JavaScript, while he’s working on C++.

What’s JavaScript 2 ?

JavaScript 2 is the upcoming new version of JavaScript, a dynamic language understood by most browsers and used to add interactivity to web pages. JavaScript 2 is not yet fully finalized — hence not yet understood by browsers. The final prototype of JavaScript 2 is expected shortly and one may hope that browsers will follow in 2008. In particular, Firefox is expected to take advantage of JavaScript 2 quickly, both for the web and for its own user interface.

For more information about JavaScript 2, see

What kind of security issues do you propose this could detect ?

Let’s see…

Firstly, simple stuff:

  • no eval() or any implicit conversion string -> code
  • no XPCom

Later, more complex (and useful) stuff:

  • no call to such-and-such XPCom component or interface (e.g. nsIFile, nsIDebug, nsIRegistry)
  • no call to such-and-such method of such XPCom component
  • no (re)definition of “@mozilla.org/*” XPCom components
  • no execution of code dynamically downloaded with XMLHttpRequest

Even later, very precise (and, generally, very undecidable) stuff:

  • make sure that all uses of nsIFile use file names built-to-be-safe methods (e.g. only in the user’s profile)
  • no rewiring of other extensions

All this, of course, in addition to checking non-security policies, such as

  • every open file will be closed again
  • every exception will be caught

If there’s no code, isn’t it a bit early to post this ?

Well, better get comments and criticisms earlier than later. That and burning ships…

Tagged: , , , , ,

§ 8 Responses to JStify — Request For Comments

  • This is important work. I thought of doing something like this for a course on program analysis I’m taking, but it was too daunting. A few static tools for JS exist, with some even in the research (Yu et al. at POPL ’07, e.g.), but this promises to be the most useful and general of them all.

    What are you going to do about the inevitable deviations from the specification? It might be possible to parameterize the analysis framework so that it can be run with an eye to different browsers/platforms.

  • yoric says:

    A few static tools for JS exist, with some even in the research (Yu et al. at POPL ’07, e.g.), but this promises to be the most useful and general of them all.

    Thanks for the reference, I’ll try and read it tomorrow. At first glance, the paper you mention seems to indicate that the Flint team concentrates on a subset of JS and attempts to mathematically build provably sound policies, while we try to go the other way round, start from the full language, with initially probably-somewhat-unsound policies and experiment our way towards sound policies. Both approaches have their interest and I often belong to that let’s-build-mathematically school of thought. It just happens so that I believe it’s not adapted to JavaScript, but I might be wrong.

    What are you going to do about the inevitable deviations from the specification? It might be possible to parameterize the analysis framework so that it can be run with an eye to different browsers/platforms.

    Good question and good suggestion. I’ll keep both somewhere safe until time comes :)

  • [...] an interesting post about the safety of extensions and put forward the outline of an analysis toolbox for the Javascript language. Feel free to comment. addthis_url = [...]

  • Wes Garland says:

    Yoric –

    This is indeed an interesting tool. You must also remember, there are applications for it outside of the browser, and indeed outside of the OSS world which make its extensibility particularly interesting.

    For example, we use JavaScript as glue or application code driving large collections of well-worn systems code. Being able to perform general-prupose analysis on this type of code is only so useful… but being able to add specific rules for JS Classes which are unique to our environment means that we can go further, and potentially perform tasks such as enforcement of business rules, custom and non-trivial security enhancements, etc.

  • yoric says:

    A few static tools for JS exist, with some even in the research (Yu et al. at POPL ‘07, e.g.)

    I’ve taken a second look at that paper and it seems I had missed just about everything that was interesting in it. It looks like something we could implement with JStify once we have rewriting tools.

  • yoric says:

    Being able to perform general-prupose analysis on this type of code is only so useful… but being able to add specific rules for JS Classes which are unique to our environment means that we can go further, and potentially perform tasks such as enforcement of business rules, custom and non-trivial security enhancements, etc

    It will definitely be possible to add specific rules. For now, however, I can’t think of any method easier to do that than writing a little OCaml code. If you have any example of a specific rule, though, I’ll be glad to read it.

  • Matt says:

    Is there any update on this project? I note the dates are 2007 but a google for the name didn’t yield anything.

    I have been thinking about similar things, and having trouble grappling with a way to make decent assertions with the dynamic nature of the language.

  • yoric says:

    Is there any update on this project? I note the dates are 2007 but a google for the name didn’t yield anything.

    Unfortunately, this project has been cancelled by my hierarchy. So much for burning ships…

    I have been thinking about similar things, and having trouble grappling with a way to make decent assertions with the dynamic nature of the language.

    Well, of course, you’re not going to get away with the full dynamism of the language if you want decent assertions. If you’re looking for bibliography, you should take a look at JS0. You could start from this and progressively expand.

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 — Request For Comments at Il y a du thé renversé au bord de la table.

meta

Follow

Get every new post delivered to your Inbox.

Join 29 other followers

%d bloggers like this: