Static Analysis for Securing Event-driven JavaScript Programs

Printer-friendly version
Info
Prerequisites: 
  • Strong interest in and knowledge of dynamic programming languages and interpreters, particularly JavaScript.
  • Interest in static analysis and program verification.
Context: 

JavaScript is a very flexible language that is used to write large and complex web and server applications that run in event-driven runtime environments such as the browser or Node.js. Due to the complex nature of these applications, it is very difficult for application developers to keep track of control flow (possible paths through a program) and information flow (possible values of expressions). Yet, many security problems can be formalized as control and information flow problems which for example seek to preserve the integrity of data (don't allow untrusted values to affect a sensitive value or operation) and confidentiality of data (don't pass sensitive values to untrusted parties).

Different approaches to analyze control and information flow in a program exist, including static approximation using abstract interpretation. The Software Languages Lab has developed an abstract interpreter for JavaScript, called JIPDA [1]. Given a JavaScript program, it produces a state transition graph that represents a finite representation of the behavior of that program at runtime. This state graph can then be queried to deduce program properties, thereby implementing different kinds of analyses. To see it in action, go to http://jensnicolay.github.io/jipda/protopurity/protopurity.html and type in a simple program such as 

function sq(x){return x*x};sq(5)

and press eval.

However, JIPDA currently implements a whole-program analysis of non-event-driven programs only, resulting in a traditional flow graph of these programs containing control and value flow induced by function calling. Therefore, JIPDA is unable to reason over the ever-increasing number of event-driven JavaScript programs, because its graphs do not reflect the flow implied by the registration of event listeners and the emission of events.

Goal & Research Activities: 

The goal of this thesis is to extend JIPDA so that it can handle event-driven programs. The idea is to extend or complement the graph that JIPDA produces with event information to create an abstract event graph. Such a graph consists of the explored states of the program, as well as the event flow together with the executed event listeners. Furthermore, it should be possible to construct event sequences from this graph. An event sequence is a regular expression that summarizes which successive events lead up to a particular program state.

We propose to design and test your solution on simple Node.js programs.

The principal research activities are (i) surveying existing solutions and domains for static event-driven analysis, and (ii) designing your own solution on top of JIPDA for simple Node.js programs, together with a formal description of your work.