Avancement Tache 1 du projet GECCOO
Sylvain Boulmé, janvier 2004

Dans la tâche 1 du projet Geccoo, nous travaillons sur les sujets
suivants:

- le développement d'un langage de spécification pour des propriétés de
sécurité de haut niveau
- la sémantique des spécifications.
- spécifications modulaires et composables pour la programmation
  orientée-objet

L'équipe Everest s'intéresse plutôt aux deux premiers points, l'équipe
VasCo aux deux derniers. Le deuxième point (la sémantique des
spécifications) ne fait pas l'objet d'un travail spécifique, mais il
est développé pendant le travail des deux autres points.

Depuis le début de Geccoo, nous nous sommes concentré sur le premier
point. Premièrement, nous avons fait un inventaire des propriétés de
sécurité, basé sur des documents fournis par des industriels de la
carte à puce. Nous distinguons deux niveaux des sécurité: le niveau le
plus haut décrit des propriétés générales, et puis un niveau inférieur
où nous identifions des règles concrètes, qui doivent être suivies par
l'implémentation. Un expert de la sécurité fait une traduction des
propriétés générales en règles concrètes. Puis, le développeur de
l'application doit respecter cette ensemble des règles, qui sont
ensuite vérifiées par un audit de sécurité.

Jusqu'à présent, cet audit de sécurité est fait manuellement, nous
avons développé un outil qui permet d'automatiser certaine phase de
cet audit.

Notre outil prend une règle de sécurité et la traduit dans des
annotations JML. Puis, nous vérifions si l'application respecte les
annotations JML, en utilisant des outils comme Jack et Krakatoa. Si
les annotations sont acceptées, nous pouvons conclure que
l'application est correcte vis à vis de la règle traitée.
Ce travail est décrit dans :

Enforcing High-Level Security Properties For Applets
M. Pavlova, G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet
INRIA Technical Report, nr. RR-5061
2003

Dans les mois qui viennent, nous prévoyons d'étendre notre méthode et
notre outil, afin que l'outil puisse prendre un automate de sécurité
arbitraire comme règle en entrée. Nous travaillons également sur une
preuve formelle de la correction de la méthode.

En plus, nous avons prévu d'étudier de plus près la relation entre les
deux niveaux de spécification: propriétés de sécurité et règles de
sécurité.

Pour le troisième point, on essaye de concevoir un langage de
spécification qui offre un support pour le développement formel par
composant. Notre objectif est de proposer un langage de spécifications
ayant des aspects objets et ayant de bonnes propriétés vis-à-vis des
preuves: notion forte d'invariant (les invariants des objets sont
garantis vérifiés dans les états observables des objets, par
construction), relation de raffinement entre classes, modularité des
spécifications. Cela amènera de nombreuses restrictions sur le langage
de programmation (récursivité ouverte, visibilité des états des
objets, présence d'alias, etc). Mais ca semble le prix à payer en
l'état actuel des connaissances. Partant des concepts introduits dans
la méthode B (théorie des substitutions généralisées et du
raffinement, langage de "machines"), on cherche à les étendre avec des
aspects objets. Si certains traits de la méthode B (composants,
encapsulation d'états, développement par raffinements) la rapproche de
la philosophie des langages OO (orientés objet), certains traits des
langages OO ne peuvent pas être exprimés en B.

Jusqu'ici, on a travaillé sur deux types d'extensions de B. La
première porte sur le langage de substitutions généralisées: on
introduit de l'ordre supérieur pour exprimer que les objets sont des
valeurs qui peuvent "transporter" du code. En effet, il est commun
d'écrire des programmes OO paramétrés par du code effectuant des
effets de bords (cf. patron de l'observateur). Pour traiter ce genre
de programmes, on a décrit en Coq un langage de substitutions
généralisées qui permet spécifier et prouver par raffinement des
fonctions ML d'ordre supérieur avec effets de bord (modifications d'un
état global et exceptions). Ce travail donne lieu à un rapport de
recherche du LSR en cours de rédaction:
  Specifying and reasonning with non-purely-functional programs in type
  theory using refinement calculus. Sylvain Boulmé.
La deuxième extension porte sur la modularité de B: on propose de
mieux concilier la spécification modulaire et le partage d'états. D'un
côté, on veut écrire des spécifications modulaires qui puissent être
raffinées de manière indépendante, et telle que la cohérence globale
des raffinements soit garantie avec un faible effort de preuve: en B,
il n'y a aucune preuve à faire, mais chaque variable ne peut être
modifiée que par un seul module. D'un autre côté, on souhaite que les
modules partagent des espaces d'états communs. Le partage d'état
simplifie souvent les implémentations et donne du code plus
efficace. Il est d'ailleurs abondamment utilisé en programmation OO
comme moyen de communication entre objets. On clarifie et on
généralise les mécanismes de B sur ce point dans un rapport de
recherche du LSR:
  Formal Specification and Development: Compositional Aspects in the
  B-Method. Marie-Laure Potet.

On fera le point sur les travaux du troisième point à la réunion de
mai.