Réunion du 20 Mars 2000
The first meeting was held on March 20th at INRIA
Sophia-Antipolis.
Programme
- 10.30 Line Jakubiec (Oasis):
Formalisation of the JCVM in Coq.
Abstract We report on ongoing work to provide an
environment for proving security properties for Java Card
programs. In particular, we shall present:
- a complete formalization in Coq of the CAP (for
\underline{C}onverted \underline{AP}plet) file format;
- a formal specification in Coq of a substantial
fragment of the JCVM and JCRE.
The salient features of our formalizations are a tight adherence to
Sun's official specifications---we only depart from the original
specification by formalizing bytes as natural numbers---and the use of
advanced type-theoretical features, including dependent types and
implicit coercions, to capture Sun's specifications in a direct and
readable fashion.
- 11.15 Yves Bertot (Lemme):
Formalisation en Coq de la discipline de typage pour
l'assembleur JVM concernant l'initialisation des objets
Résumé Dans une expérience portant sur
un homme-mois et demi, nous
avons formalisé en Coq le contenu d'un article de Stephen & Freund sur
la vérification des contraintes d'initialisation d'objets dans la
machine virtuelle Java à l'aide d'un algorithme de typage.
Ce travail a été complété par la construction d'un algorithme effectif
utilisant un algorithme d'unification fourni dans les contribution de
Coq. Les enseignements tirés de cette expérience concernent en
particulier les aspects suivants:
- Utilisation des types dépendants pour décrire les objets de classes
différentes,
- Codage d'une structure de données dans un langage de termes
unifiables et preuves sur ce codage.
- 11.45 Pascal Brisset (France
Telecom): A Case Study in Java Software
Verification: Network Access Security
Abstract Run-time authorization of network communications between
untrusted applications and remote hosts is one of many
security features in the Java platform. We provide a
description of the corresponding security mechanism, which is
part of the runtime library, and observe that establishing its
correctness, even informally, requires a surprisingly complex
line of argument involving a number of salient features of the
Java language. This makes it a challenging case study in
formal verification of object-oriented software. Finally, we
give an overview of our current approach which is based on
refutation in temporal logic, Floyd/Hoare style semantics and
on-the-fly generation of program specifications.
- 14.15 Jean Goubault (Coq):
Presentation of Coq's research.
- Formalisation of BDDs in Coq.
- Towards self-certified code in Coq.
- 15.00 Thomas Jensen (Lande):
Presentation of Lande's research.
- Verification of control flow based security policies.
- Correctness of Java Card method lookup via logical relations and
its formalisation in Coq.
- 16.00 Discussion.
Participants
A. Baala (Lemme), G. Barthe (Oasis), A. Bouali (Tick), Y. Bertot
(Lemme), P. Brisset (France Telecom), D. Caromel (Oasis), F.
Chalaux (Oasis), C. Courbis (Oasis), J. Despeyroux (Certilab),
J. Goubault-Larrecq (Coq), B. Grégoire (Coq), L. Jakubiec
(Oasis), T. Jensen (Lande), J.-L. Lanet (Gemplus), C. Loiseaux (Trusted Logic),
E. Madelaine (RMI Sophia), D. Parigot (Oasis), L. Rideau (Lemme), M. Russo
(Oasis), D. Sangiorgi (Mimosa), B. Serpette (Oasis), R. de Simone (Tick),
S. Sousa (Oasis), B. Werner (Coq).
Back to the S-Java home page.
Gilles Barthe
Last modified: Mon Dec 4 10:03:40 MET 2000