Generation of Certified Code for Object Oriented Applications
specification, refinement, proof and error detection
Summary
This project aims at developing methods and tools for the design of object-oriented systems that require a high degree of security. The methods and tools will be developed to be integrated, i.e. together they will form a coherent design method from specification to certified code generation using refinement, simulation, testing and verification techniques. In particular, the project focuses on the design of smart card applications, written in a subset of Java (like JavaCard), annotated with JML specifications. JML, the Java Modeling Language, is a source code level behavioural specification language for Java that is designed to be easy to understand for people with Java knowledge. Several tools exist which manipulate JML annotated programs, e.g. to generate documentation or tests (either dynamic or unitary) or to do automatic or interactive verification. The readability of JML specifications and the wide range of tools available for JML make it attractive for industry to integrate formal methods (in the form of JML specifications) in their software development process.

However, experiences with using JML for industrial applications also have revealed several of its shortcomings which this project proposes to attack. First of all, it is important that the requirements on the application can be expressed formally, and at an abstract level, from the beginning of the development process. Subsequently, these specifications can then be refined, until an executable and efficient program has been constructed. These refinement steps can give rise to proof obligations, for which we need to have proof procedures which can handle most of these proof obligations automatically. And since it rarely is the case that a specification and a program are correct from the start, it is important to have testing and simulation techniques to detect errors as soon as possible. Finally, sometimes it is (practically) impossible to prove the correctness of an implementation. Therefore, we want to be able to generate defensive code, which can be validated using the testing and simulation techniques.

In all this work, the notion of proof is central. Each step in the development process should be formally justified and whenever possible, the justification should be mechanised with a computer. Because of undecidability results, in general it is impossible to prove automatically the correctness of all required properties. To show them by hand is theoretically feasible, however in practice this often is too much work. Therefore, it is necessary to (1) develop automatic methods tailored to the specific class of problems encountered when adressing security properties of object-oriented programs and (2) to combine interactive and automatic techniques. In particular, one can combine static or dynamic tests and verification techniques in order to eventually obtain correct executable code.

The project will focus on four main topics, which correspond to the different development steps for software with high degree security requirements: A fifth task focuses on integration of the different components in an environment for developing certified programs.

For each of the topics, we will briefly discuss what we expect to achieve within this project.

High-level specifications
We shall identify a high-level specification language for describing common security policies, for example: Many of these properties cannot directly be expressed on the level of methods, so therefore we need a higher level of specification, which can be used to restrict the interaction between different methods (and objects). We define a semantics for this language, and clarify the role of invariants and encapsulation in object-oriented modeling in order to compose specifications in a modular way without redoing the proofs.

Refinement and object oriented programming
The specification language that we will define should be suitable for development by refinement. The refinement proces should also be integrated with the object-oriented development model, which based on inheritance and overriding. A first objective is to study refinement at the level of classes and methods. Next, we will extend the work to refinement of components and the construction of specifications by composition of specifications. An important issue is to study under which conditions security properties are preserved by refinement.

Generation and resolution of proof obligations
The correctness of refinement steps and possibly of the code is established by generating and subsequently solving proof obligations. The complexity of properties depends on the theory in which they are expressed and on our requirements on what has to be proved. For example, existing tools only ensure partial correctness of recursive methods, and often do not check possible overflows in arithmetic computations. Within this project, we will aim at handling this kind of properties. However, in many cases one might only be interested in exception propagation or the non-modification of some fields. For such more restricted properties, we will developed appropriate automated techniques. In general, it is necessary to relate interesting security properties and proof techniques, in order to improve the automatic resolution of proof obligations.

Error detection
It is also possible to use specification annotations in the code in order to do early error detection. If at some control point in the program, a proof obligation cannot be solved automatically, it is possible to replace verification by testing. There are different ways in which this can be done: one can generate adequate inputs to reach the control point or one can introduce dynamic tests in the generated code. Partial evaluation and simulation using constraint resolution may also be interesting methods to detect errors in the code or in the specification at an early stage.

Environment
The teams collaborating in this project have complementary skills in the domains of security, modeling object oriented programs, and interactive and automatic program verification. Collaborations already exist: the tool Why for program verification has been adapted to produce proof-obligations that can be solved by the automatic solver haRVey . The people at LIFC and LORIA are part of a common INRIA team CASSIS. They collaborate with the VasCo team in the national RNTL project B-OM. This project studies optimisation of generated code using the B-method for execution on a smartcard. Lemme and LogiCal participate in the european IST project VERIFICARD which is in particular concerned with verification of JavaCard applets using JML specifications.

This document was translated from LATEX by HEVEA.