Calcul d'Objets Sécurisé


Les calculs d'objets permettent de modéliser de manière formelle des systèmes d'objets répartis. Nous avons conçu le calcul ASP (Asynchronous Sequential Processes) pour modéliser le comportement de la bibliothèque ProActive, une bibliothèque 100% Java, qui propose les caractéristiques suivantes:
    o la création d'objets distants et actifs,
    o des appels asynchrones avec futurs transparents,
    o de la migration d'objets actifs (mobilité),
le tout offrant des mécanismes de synchronisation de haut niveau qui simplifient la programmation répartie.

Le calcul ASP  permet de modéliser une distribution des activités qui communiquent par
requêtes asynchrones. Le calcul a des propriétés de confluence et de déterminisme qui sont particulièrement intéressantes pour un calcul distribué.

L'objectif général de ce stage de DEA consiste à étudier et étendre le calcul ASP avec un modèle de sécurité proposé, en prenant en compte les aspects suivants:
       o niveau d'autorisation des utilisateurs
       o niveau de confidentialité des informations
Le principe étant bien sur que seuls les utilisateurs possédant un niveau d'autorisation
suffisant ont accès à une information (objet) donnée.

Il s'agit dans ce travail de DEA faire un double travail de connaissance du domaine (il existe plusieurs calculs proposant des mécanismes de sécurité) et de proposition d'extension du Calcul ASP pour la sécurité des flots d'information.

Dans un premier temps, l'objectif est de disposer d'un modèle formel permettant de comprendre le modèle de sécurité proposé, étudier le comportement en présence d'objet actif, avec passage par copie, communication asynchrone avec diffusion de futurs, etc.

Un second objectif sera d'identifier clairement:
        o les contrôles à effectuer
        o les points de ces contrôles
afin de tester et d'assurer dynamiquement un accès autorisé à l'information.

A plus long terme, il s'agira de vérifier statiquement qu'une application ne déclenche pas dynamiquement des violations de l'accès. Cette analyse pourra se baser sur deux techniques
principales: analyse de flot de données, et model-checking.

L'étudiant travaillera en équipe, avec les membres de l'équipe Oasis, et en particulier les concepteurs du calcul ASP et du modèle de sécurité pour la bibliothèque ProActive.
Ces travaux pourront naturellement se poursuivre en Thèse de Doctorat.


Encadrement :    Isabelle Attali & Denis Caromel
Téléphone : 04 92 38 79 10 & 04 92 38 76 31
Emails : Isabelle.Attali@inria.fr et Denis.Caromel@inria.fr
Laboratoire ou équipe : INRIA Sophia Antipolis -- I3S-CNRS, Projet OASIS

Prérequis : langages à objets, programmation répartie, des bases en réseau, standards W3C
Matériel et logiciels utilisés : Stations de travail

Lieu du stage: INRIA Sophia Antipolis, France


Références:

     Towards Seamless Computing and Metacomputing in Java
     D. Caromel, W. Klauser, J. Vayssiere,
     pp. 1043--1061 in Concurrency Practice and Experience,
     September-November 1998, 10(11--13), Editor Geoffrey C. Fox, Published by Wiley & Sons.
    Available here

     A Theory of Objects - Martin Abadi and Luca Cardelli - Springer Verlag - 1996.