Static Analysis Techniques for Evaluating Runtime Monitoring Properties Ahead-of-Time
Eric Bodden, Patrick Lam, Laurie Jane Hendren · 2007
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%.