DANSAS 2011, Odense, August 18

Preliminary Program

09:00 - 09:30Coffee and breakfast rolls
09:30 - 09:40Welcome
09:40 - 10:25Program Analysis for Engineering Secure Web Applications (invited talk)
Zhendong Su
10:30 - 11:00Fruit Break
11:00 - 11:25Programming in Biomolecular Computation
Neil D. Jones
11:35 - 12:00Formalizing Elections for Tractable Test Generation using Model Checking
Joseph Kiniry and Dermot Cochran
12:05 - 13:35Lunch
13:35 - 14:00Tool-supported Refactoring for JavaScript
Asger Feldthaus
14:10 - 14:35Finding Resource-Release Omission Faults in Linux
Suman Saha
14:45 - 15:10Guarded Type Promotion
Johnni Winther
15:15 - 15:45Coffee Break
15:45 - 16:10Monotonicity Constraint Transition Systems and Complexity Analysis
Amir M. Ben-Amram
16:20 - 16:45Static Analysis for a Dynamic Language: the Crankshaft JavaScript Compiler
Kevin Millikin
16:50 - 17:00Announcement of best student presentation and wrap-up

Program Analysis for Engineering Secure Web Applications (invited talk)

Zhendong Su

University of California, Davis

Web applications enable much of today's online business. Anyone with a web browser can access them, and the data they manage typically has significant value both to the users and to the service providers. Thus, they have become increasing targets of attacks. Since 2005, the most frequently reported classes of vulnerabilities have been for web applications. There are two broad classes of web application vulnerabilities: 1) application-agnostic injection flaws, and 2) application-specific access control flaws. Their detection and prevention pose an interesting challenge for program analysis. In this talk, I will present two simple, yet general characterizations of these vulnerabilities and a set of program analysis techniques to detect them.

About speaker: Zhendong Su is a Professor and Chancellor's Fellow at University of California, Davis. He received his PhD in Computer Science from University of California, Berkeley. His research focuses on developing practical techniques and tools for improving software quality and programming productivity. He serves as an Associate Editor for ACM Transactions on Software Engineering and Methodology (ACM TOSEM), co-chaired the 2009 Static Analysis Symposium (SAS), and is the program chair of the 2012 International Symposium on Software Testing and Analysis (ISSTA).

Programming in Biomolecular Computation

Neil D. Jones

University of Copenhagen

In spite of widespread discussion about connections between biology and computation, one question seems notable by its absence: Where are the programs? We take the question seriously, and propose a model of computation that is at the same time biologically plausible: the model's functioning is defined by a relatively small set of chemical-like reaction rules; programmable (by programs reminiscent of low-level computer machine code); uniform: new "hardware" is not needed to solve new problems; universal: all computable functions can be computed (in natural ways and without arcane encodings of data and algorithm); stored-program: programs are the same as data, so programs are not only executable, but are also compilable and interpretable; and (last but not least) Turing complete in a strong sense: a universal algorithm exists, able to execute any program, and not asymptotically inefficient.

The model has been designed and implemented (for now in silico on a conventional computer). This work opens new perspectives on just how computation may be specified at the biological level. One goal is to provide a top-down approach to biomolecular computation.

(joint work with Lars Hartmann and Jakob Grue Simonsen)

Slides available as .pdf

Formalizing Elections for Tractable Test Generation using Model Checking

Joseph Kiniry and Dermot Cochran

IT University of Copenhagen

E-voting software, particularly tallying software that computes the final outcome of elections, is notoriously under-specified and poorly tested. Elections are critical systems, and yet virtually all election systems, including those used in national and EU elections, have no formal specification. Moreover, even though the state space of non-trivial election algorithms is astronomically large, virtually all commercial and open source election system include only a handful of manual systems tests. Perhaps shockingly, counting systems are, at best, tested via the random generation of ballot boxes which are counted by multiple implementations of the tallying algorithm. Consequently, such a test method exercises a microscopically small fraction of the state space. I will summarize our research in using the Alloy model checker to formalize elections to better understand elections, discover legal irregularities, and generate a complete set of non-isomorphic ballot boxes to guarantee that every election outcome is exercised during system testing.

Slides available as .pdf

Tool-supported Refactoring for JavaScript

Asger Feldthaus

Aarhus University

Refactoring is a popular technique for improving the structure of existing programs while maintaining their behavior. For statically typed programming languages such as Java, a wide variety of refactorings have been described, and tool support for performing refactorings and ensuring their correctness is widely available in modern IDEs.

For the JavaScript programming language, however, existing refactoring tools are less mature and often unable to ensure that program behavior is preserved. This lack of robust tool support is due to the dynamic nature of JavaScript, because refactoring algorithms that have been developed for statically typed languages are not applicable.

We propose a framework for specifying and implementing JavaScript refactorings based on pointer analysis. We describe novel refactorings motivated by best practice recommendations for JavaScript programming, and demonstrate how they can be described concisely in terms of queries provided by our framework. Experiments performed with a prototype implementation on a suite of existing applications show that our approach is well-suited for developing practical refactoring tools for JavaScript.

(Joint work with Max Schäfer, Todd Millstein, Frank Tip, and Anders Møller)

Finding Resource-Release Omission Faults in Linux

Suman Saha

University of Copenhagen / University of Paris 6

The management of the releasing of allocated resources is a continual problem in ensuring the robustness of systems code. Missing resource-releasing operations lead to memory leaks and deadlocks. A number of approaches have been proposed to detect such problems, but they often have a high rate of false positives, or focus only on commonly used functions. In this paper we observe that resource-releasing operations are often found in error-handling code, and that the choice of resource-releasing operation may depend on the context in which it is to be used. We propose an approach to finding resource-release omission faults that takes into account these issues. We use our approach to find over 100 faults in the drivers directory of Linux 2.6.34, with a false positive rate of only 16%, well below the 30% that has been found to be acceptable to developers.

(To be presented at the workshop Programming Languages and Operating Systems, October 2011)

Slides available as .pdf

Guarded Type Promotion

Johnni Winther

Aarhus University

In Java, explicit casts are ubiquitous since they bridge the gap between compile-time and runtime type safety. Since casts potentially throw a ClassCastException, many programmers use a defensive programming style of guarded casts. In this programming style casts are protected by a preceding conditional using the instanceof operator and thus the cast type is redundantly mentioned twice. We propose a new typing rule for Java called Guarded Type Promotion aimed at eliminating the need for the explicit casts when guarded. This new typing rule is backward compatible and has been fully implemented in a Java 6 compiler. Through our extensive testing of real-life code we show that guarded casts account for approximately one fourth of all casts and that Guarded Type Promotion can eliminate the need for 95 percent of these guarded casts.

(also presented at the 2011 Workshop on Formal Techniques for Java-like Programs)

Slides available as .pdf

Monotonicity Constraint Transition Systems and Complexity Analysis

Amir M. Ben-Amram

University of Copenhagen / Tel Aviv Academic College

Monotonicity Constraint Transition Systems over the integers - concisely (MC,Z)-CTS - are a program abstraction where termination is decidable (an extension of the well-known Size-Change Termination). A transition system is bounded terminating when there is a function that bounds the number of transitions, in terms of the input.

We have now proved that the Bounded Termination problem for these transition-systems is also decidable (in PSPACE). Interestingly, an (MC,Z)-CTS is bounded-terminating if and only if it has a polynomial bound. Furthermore, the degree of the polynomial is also PSPACE-computable.

The significance of such bounds for a source program depends on the abstraction (the "front end"). In the most natural and obvious situation it will mean a time bound. In others, it can mean, for example, a space bound. We claim that focusing on an abstraction which is expressive while being decidable is a profitable approach to studying a program analysis question, which worked nicely for termination. It should also be applicable to Complexity Analysis.

(Joint work with Michael Vainer, Tel Aviv Academic College)

Slides available as .pdf

Static Analysis for a Dynamic Language: the Crankshaft JavaScript Compiler

Kevin Millikin

Google

The JavaScript programming language is inherently dynamic, and thus a challenge for static analysis. Objects of different shapes can flow to a given site in a program. A single object can change shape over its lifetime. The language's 'eval' function can introduce code at runtime. All of these dynamic characteristics reduce the precision of static analysis. In addition, the typical language implementation is a client web browser that receives raw JavaScript source code over a network. Webpage load time is crucially important in this environment, and so only the most inexpensive analyses can normally be performed.

In this talk we describe how Crankshaft, the optimizing compiler in Google's V8 JavaScript engine, addresses these challenges. Crankshaft optimizes code based on online type feedback collected from unoptimized code. We describe the suite of static analyses currently performed by the Crankshaft compiler.