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:
-
high-level specifications;
- refinement and object oriented programming;
- generation and resolution of proof obligations; and
- error detection.
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:
-
access control: a command is not executed except in
authenticated mode;
- integrity: data cannot be modified except in
authenticated mode by a trusted partner;
- confidentiality: data can only be accessed in
authenticated mode by a trusted partner;
- availability of service: a request is always followed by an
answer;
- safety: exceptions of a certain kind are never raised; and
- methods are only called in a particular order, methods are only
called a limited number of times etc.
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.