Eric Bodden, Ph.D.

11°C

Soon to appear at ACM TOPLAS:

Finite-state properties account for an important class of program properties, typically related to the order of operations invoked on objects. Many library implementations therefore include manually-written finite-state monitors to detect violations of finite-state properties at runtime. Researchers have recently proposed the explicit specification of finite-state properties and automatic generation of monitors from the specification. However, runtime monitoring only shows the presence of violations, and typically cannot prove their absence. Moreover, inserting a runtime monitor into a program under test can slow down the program by several orders of magnitude.
In this work, we therefore present a set of four static whole-program analyses that partially evaluate runtime monitors at compile time, with increasing cost and precision. As we show, ahead-of-time evaluation can often evaluate the monitor completely statically. This may prove that the program cannot violate the property on any execution or may prove that violations do exist. In the remaining cases, the partial evaluation converts the runtime monitor into a residual monitor. This monitor only receives events from program locations that the analyses failed to prove irrelevant. This makes the residual monitor much more efficient than a full monitor, while still capturing all property violations at runtime.
We implemented the analyses in Clara, a novel framework for the partial evaluation of AspectJ-based runtime monitors, and validated our approach by applying Clara to finite-state properties over several large-scale Java programs. Clara proved that most of the programs never violate our example properties. Some programs required monitoring, but in those cases Clara could often reduce the monitoring overhead to below 10%. We observed that several programs did violate the stated properties.

Download a preprint here.

And here is our second paper to appear at SOAP… Hope to see you all at Beijing!

The IFDS and IDE frameworks by Reps, Horwitz and Sagiv are two general frameworks for the inter-procedural analysis of data-flow problems with distributive flow functions over finite domains. Many data-flow problems do have distributive flow functions and are thus expressible as IFDS or IDE problems, reaching from basic analyses like truly-live variables to complex analyses for problems from the current literature such as typestate and secure information-flow.
In this work we describe our implementation of a generic IFDS/IDE solver on top of Soot and contrast it with an IFDS implementation in the Watson Libraries for Analysis (WALA), both from a user’s perspective and in terms of the implementation. While WALA’s implementation is geared much towards memory efficiency, ours is currently geared more towards extensibility and ease of use and we focus on efficiency as a secondary goal.
We further discuss possible extensions to our IFDS/IDE implementation that may be useful to support a wider range of analyses.

Download the paper here.

Accepted for publication at SOAP:

Java Specification Request (JSR) 292, which was realized with Java 7, defines a new java bytecode called invokedynamic, which can be used to call methods by name, without determining statically where the implementation of the called method is to be found. This mechanism eases the implementation of highly dynamic languages for the Java Virtual Machine.

In this work we explain how we extended the Soot framework for static analysis and transformation of Java programs to properly handle invokedynamic bytecodes. Our implementation required changes on all levels of Soot, as all intermediate representations needed to be adapted appropriately. We comment on the design decisions taken and how users can use our implementation to statically process or generate invokedynamic instructions.

Our support has been integrated into Soot release 2.5.0 and is thus already available for everyone to use.

Download the paper here.

Andreas Thies and I have just had accepted a paper for publication at this year’s ISSTA. I have just put our camera-ready copy online. We describe an approach to ensuring the correctness of refactorings for Java programs that use reflection:

If programs access types and members through reflection, refactoring tools cannot guarantee that refactorings on those programs are behavior preserving. Refactoring approaches for highly reflective languages like Smalltalk therefore check behavior preservation using regression testing.

In our recent paper accepted at the SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), we demonstrate how inter-procedural information-flow analyses for regular programs can be transparently lifted to software product lines (SPLs), so that they can deal with conditional-compilation constructs such as #ifdef. Out approach is based on the IFDS/IDE framework by Reps, Horwitz and Sagiv. Currently, our approach is constrained to direct information flow, but we are already considering an extension to indirect flow as well.

Read the full abstract and paper here:

A software product line encodes a potentially large variety of software products as variants of some common code base, e.g., through the use of #ifdef statements or other forms of conditional compilation. Traditional information-flow analyses cannot cope with such constructs. Hence, to check for possibly insecure information flow in a product line, one currently has to analyze each resulting product separately, of which there may be thousands, making this task intractable.

We report about ongoing work that will instead enable users to check the security of information flows in entire software product lines in one single pass, without having to generate individual products from the product line. Executing the analysis on the product line promises to be orders of magnitude more faster than analyzing products individually.

We discuss the design of our information-flow analysis and our ongoing implementation using the IFDS/IDE framework by Reps, Horwitz and Sagiv.

Download the paper here

3rd International Conference on Runtime Verification (RV 2012)
September 25 – September 28, 2012

Runtime verification is concerned with monitoring and analysis of software and hardware system executions. Runtime verification techniques are crucial for system correctness and reliability; they are significantly more powerful and versatile than conventional testing, and more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for verification and debugging purposes, and after deployment for ensuring reliability, safety and security, and for providing fault containment and recovery. Topics of interest to the conference include:

• specification languages and formalisms for traces
• specification mining
• program instrumentation
• monitor construction techniques
• logging, recording, and replay
• fault detection, localization, recovery and repair
• program steering and adaptation
• metrics and statistical information gathering
• combination of static and dynamic analyses
• program execution visualization

Abstract submissions are due on May 27th. Read more here.

Due to numerous requests for deadline extensions, we have decided to extend the deadline for SOAP by one week. So submissions are now due on April 4th.

I just delivered my keynote talk at FOAL on “Towards Typesafe Join Points for Modular Reasoning in Aspect-Oriented Programs”. You can find my slides here.