Prof. Dr. Eric Bodden

Today I am proud to present our brand new Technical Report in which Patrick Lam, Laurie Hendren and me present how you can use static analysis to evaluate runtime monitoring properties ahead-of-time, i.e. at compile time opposed to at runtime.

We have been working on this topic for about a year now, with different approaches and it actually took us until some weeks ago to get it actually all worked out. The coolest thing is that the approach we found in the end is really surprisingly simple, yet very effective. All it needs is a good static abstraction and super-precise pointer analysis. That’s it. The problem that we had before was that we were tying to make things more complicated than they were.

Using this approach we actually found a bunch of "interesting" bugs and pieces of suspicious code in applications like Jython, Eclipse and PMD (excerpts are in the paper), the last one of which is actually a bug finding tool itself 🙂

I encourage you to have a look at our paper or try out some of our benchmarks. We also have uploaded a document that holds all our raw benchmark data.

This is the abstract of the paper:

Runtime monitoring enables developers to specify code that executes whenever certain sequences of events occur during program execution. In particular, runtime monitors can check for illegal API uses, such as attempts to read from already-closed files. This paper presents techniques for evaluating runtime monitoring properties ahead-of-time. Statically evaluating runtime monitors is advantageous for two reasons: 1) it enables the optimization and removal of unnecessary monitoring code; furthermore, 2) it can increase developers’ confidence that their programs conform to their stated correctness properties. In the best case, static analysis can successfully guarantee that a program never violates those properties at all.

Our work focuses on tracematches, a monitoring notation based on regular expressions with free variables over program events that bind these variables to heap objects. Statically deciding properties of tracematches is difficult: tracematches bind heap objects throughout the course of their evaluation. One might expect that an interprocedural flow-sensitive analysis would be required. However, our approach successfully analyzes tracematches by combining inexpensive whole-program summary information with a suite of carefully-designed intraprocedural flow-sensitive analyses. Our analyses use a novel abstraction which captures both positive information, indicating that an object could be associated with a particular monitor state, and negative information, indicating that the object is known not to be in a state. This abstraction enables us to eliminate unnecessary monitoring instrumentation.

We implemented our analyses and applied them to 43 program/tracematch combinations. In 18 cases, our analysis removes all instrumentation from the programs, statically verifying the tracematch property. In 12 more cases, our analysis leaves no more than 10 instrumentation points, and we easily verified (by hand) that these programs satisfied (or falsified) the stated property. In 36 of 43 cases, our techniques reduce runtime overhead to below 10%.