Next: , Previous: Introduction, Up: Introduction

1.1 Motivation - Specification and Verification of Bytecode

Traditionally, program specification and verification is done at the level of source code. The use of high-level language constructs, and the higher level of abstraction, helps to structure the verification tasks. However, applications are executed at the level of bytecode, and to provide a full correctness guarantee, one needs techniques to specify and verify also at the level of bytecode. In some cases, correctness can be ensured by the compiler, but often it is necessary to reason at the level of bytecode directly.

In particular, often small applications are developed directly at the bytecode level, either to achieve better optimisation, or because one does not trust the compiler, and one needs to ensure that all possible security threats are avoided. Thus, it is essential to have the means to specify and verify an application directly at this level, without the use of a compiler. Therefore we need both specification and verification techniques that are tailored directly to the particularities of executable code. Moreover, in order to capture all relevant security requirements, the specification language used should be expressive enough for this.

The availability of analysis techniques at bytecode level allows to take into account aspects of computation which can be easily overlooked at the source code level, or cannot be modelled satisfactorily (e.g., the granularity of operations in the multi-threaded context). Moreover, proofs concerning the bytecode application can sometimes lead to a speed-up in JIT compilation [Quigley04][Courbot-Pavlova-Grimaud-Vandewalle06].

Also when an application is developed at source code level, often it is only distributed in the bytecode format (or if the source code is available, one does not not trust the compiler to preserve the behaviour of the program). In such a case, if an independent software distributor wishes to certify a program, it is essential that the intended behaviour of the application is described at the same level as the implementation that will be verified, i.e., at bytecode level.

Proof Carrying Code (PCC) is a typical example where the possibility to specify and verify executable code directly is imperative, in particular when one wishes to capture complex security policies that cannot be checked with a type checker. PCC is a possible solution to support the secure downloading of applications on a mobile device. The executable code of an application comes together with a specification, and the necessary evidence from which the code client can easily establish that the application respects its specification. In such a scenario, the code producer, who has to produce a correctness proof, will often prefer to do the verification at source code level, and then compile the specification and the proof into the level of executable code. Realising a platform to support this scenario is one of the goals of the Mobius project (the development of BML is a spin-off of this project).

The fact that BML is designed to be very closely related to JML is motivated by the interest in PCC. Given the close correspondence between source code and bytecode, and source code specifications and bytecode specifications, it is not too complicated to transform a certificate for a JML annotated Java program into a certificate for a BML annotated bytecode program (see e.g., [Barthe-Gregoire-Kunz-Rezk06]).