Work Package 3 Logic-based Verification

This work package develops scalable logical techniques for the specification and verification of functional and security properties of multi-threaded Java, both at source code and byte code level, and realizes a program verification environment that provides tool support for these techniques.

Scientific Objectives

The scientific objective of this work package is to develop modular logical techniques for verifying security and functional properties of programs at the source and byte code level. Specifications will be written in a more or less standard annotation language - in the style of JML - for expressing preconditions, postconditions, invariants and frame properties, extended with primitives that also allow resource and information flow properties to be expressed.

One innovative aspect of the work package is that we want to support specification and verification not only at source code level, but also at byte code level. Support for byte code level is needed to enable Proof Carrying Code, as only the byte code is available for checking by the code consumer.

A program verification environment will be developed that supports the techniques developed in the project. This will be used in the experiments on case studies in WP5. The program verification environment will be based on existing verification tools (in particular ESC/Java2 and JACK).

Existing results

An important basis of the work is extensive experience with the specification and verification of single-threaded Java source code. This includes the specification language JML for single-threaded Java and the program verification technologies that underlie program verification tools such as ESC/Java2, JACK, Jive, KEY, LOOP, Boogie, and Krakatoa.

The work in Task 3.1 and Task 3.2 can also benefit from the experience in dealing with resource properties developed in the MRG project.

Structure of the work package

The work package is structured into seven tasks. The first 6 all start within the first 12 months of the project.

Task 3.1 Byte Code Specification and Verification

We will develop a specification language and a program logic for single-threaded code at byte code level.

Task 3.2 Logic for Resources and Information Flow

We will study how the specification language developed in the previous task can be used to express properties about resource usage and information flow, and where necessary extend the language and the associated logic. Ultimately, the logic will cover the properties described in Task 1.1 and Task 1.2.

Task 3.3 Multi-threading

We will develop a logic-based verification technique for multi-threaded programs including a general, sound verification method. To make verification feasible, we will identify conditions that easily can be checked and under which verification can be simplified, based on case studies from the concurrency framework provided in the Java 1.5 API by the java.util.concurrent package.

Task 3.4 Modular Verification

We will develop a practical modular verification technique for class invariants and frame properties that can handle interesting implementation patterns including inheritance, call backs, recursive object structures, transactions, and concurrency. Modular verification of these properties is essential for scalability. The technique will be applicable to both source and byte code programs.

Task 3.5 Combining Type-based and Logical Verification

We will develop a framework that facilitates the interaction of type-based and logic-based analyses of programs. This will extend the reach of type-based analyses and it will make verification more efficient. The latter has the effect of making proof objects smaller, which is important for feasibility of Proof Carrying Code. Part of the effort is targeted at the byte code level.

Task 3.6 Program Verification Environment

We will realize a program verification environment for a substantial subset of multi-threaded Java source code and byte code that utilizes the results of this work package. The verification environment will produce the output necessary for the construction of the logic-oriented certificates used for Proof Carrying Code in WP4, and will be used in the experiments on case studies in WP5.

Task 3.7 Annotation Generation

Because the process of annotating code is very labour-intensive and costly, we will develop automated support for annotating code, and integrate this support in the program verification environment.