ABSTRACT. TBA

ABSTRACT. JavaScript supports a powerful mix of object-oriented and functional programming, which provides flexibility for the programmers but also makes it difficult to reason about the behavior of the programs without actually running them. One of the main challenging for program analysis tools is to handle the complex programming patterns that are found in widely used libraries, such as jQuery, without losing critical precision. Another challenge is the use of dynamic language features, such as 'eval'. This talk presents an overview of the challenges and the techniques used in the TAJS research project that aims to develop sound and effective program analysis techniques for JavaScript web applications. 

ABSTRACT. JavaScript is a popular, powerful, and highly dynamic programming language. It is the arguably the most widely used and ubiquitous programming language, has a low barrier to entry, and has vast amounts of code in the wild. JavaScript has grown from a language used primarily to add small amounts of dynamism to web pages into one used for large-scale applications both in and out of the browser--including operating systems and compilers. As such, automated program analysis tools for the language are increasingly valuable. Almost all of the research to date targets ECMAScript 3, a standard that was succeeded by the most recent version, 5.1, over four years ago. Much of the research targets well-behaved subsets of JavaScript, eliding the darker corners of the language (the bad parts). In this work, we demonstrate how to statically analyze full, modern JavaScript, focusing on uses of the language's so-called bad parts. In particular, we highlight the analysis of scoping, strict mode, property and object descriptors, getters and setters, and eval.

Speed, precision, and soundness are the basic requirements of any static analysis. To obtain soundness, we began with LambdaS5, a small, functional language developed by Guha et al. that, through desugaring, encompasses the entirety of the ECMAScript 5.1 standard. Its small size and deliberate desugaring make it a tractable intermediate representation for the analysis of JavaScript. Leveraging the semantics of LambdaS5, we build an abstract machine interpreter. Following the abstracting abstract machines recipe developed by Van Horn and Might, a small-step abstract machine is easily and soundly transformed into an abstract interpreter.

Once we have a sound abstract interpreter, speed and precision can be configured from a number of angles. Optimization techniques developed by Johnson et al. make any AAM-style analyzer faster. By parameterizing the analyzer's allocation function we gain another axis of control. A modular design of the analyzer's values makes it possible to plug-and-play different lattices, which is necessary for testing different abstractions of JavaScript's values and non-trivial objects. The objects of the 5.1 specification are no longer simple key-value mappings, but map their string keys to either data or accessor properties, each of which hold their own metadata. Further, data properties can be converted to and from accessor properties. The objects themselves hold metadata that changes the semantics of modifying both their mappings and metadata, causing the same line of code to either update a value, silently have no effect, or raise an exception. In the setting of analysis, a map with abstract spaces for both keys and values presents its own challenges to retain soundness while remaining performant. As an example of a potential lattice, we discuss an abstraction of JavaScript's objects that significantly improves performance at the cost of a loss in precision.

ABSTRACT. Multi-stack pushdown systems are a well-studied model of concurrent computation using threads with first-order procedure calls. While, in general, reachability is undecidable, there are numerous restrictions on stack behaviour that lead to decidability. To model higher-order procedures calls, a generalisation of pushdown stacks called collapsible pushdown stacks are required. Reachability problems for multi-stack collapsible pushdown systems have been little studied. In a recent FSTTCS article we studied ordered, phase-bounded and scope-bounded multi-stack collapsible pushdown systems using saturation techniques and showed decidability of control state reachability, as well as giving a regular representation of all configurations that can reach a given control state.

ABSTRACT. We propose a new way of thinking about abstract interpretation with a method we term environment unrolling. Model checkers for imperative languages will often apply loop unrolling to make their state space finite in the presence of loops and recursion. We propose handling environments in a similar fashion by putting a bound on the number of environments to which a given closure can transitively refer. We present how this idea relates to a normal model of abstract interpretation, give a general overview of its soundness proof in regards to a concrete semantics, and show empirical results demonstrating the effectiveness of our approach.

ABSTRACT. This work presents an incremental improvement to abstract interpretation of higher order languages, similar to strong update, which we term strong function call. In an abstract interpretation, after a function call, we know which abstract closure was called and can deduce that any other values found at the same abstract address in the abstract store could not possibly exist in the corresponding concrete state. Thus they can be removed from the abstract store without loss of soundness. We provide the intuition behind this analysis along with a general overview of its soundness proof.

ABSTRACT. A careful investigation of the work by Naoki Kobayashi and Luke Ong reveals that priorities (or colors) behave in essentially the same way as the exponential modality of linear logic. From this follows a purely proof-theoretic reconstruction of their type system, based on an indexed and infinitary variant of tensorial logic. In this talk, we will describe the basic properties of the color modalities, and how to translate a minor variant of Kobayashi and Ong's type system into tensorial logic with colors.

Talk of 30 minutes.