JStify — Request For Comments
October 11, 2007 § 8 Comments
Note Je mettrai en ligne sous peu une version française de ce billet.
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
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 elimination of well-known (albeit perhaps recently discovered) weaknesses
Technically, JStify is a set of OCaml modules.
The base modules take charge of
- lexing and parsing user-added annotations (in comments)
- 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
- 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
- export a syntax tree to XML (for pretty-printing or manipulation by other programs).
JStify is currently in early development stage. I hope to have a first prototype by the summer.
Any questions ?
Does “JStify” mean anything ?
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.
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.
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.
Who’s funding this ?
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 ?
- the official site
- a technical presentation by Firefox’ Brendan Eich
- update of the previous presentation by the same Brendan Eich.
What kind of security issues do you propose this could detect ?
Firstly, simple stuff:
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…