DISPO

Disponibilité de services dans des composants logiciels


Projet labellisé dans le cadre de l'ACI Sécurité Informatique du ministère délégué à la Recherche et aux Nouvelles Technologies (2003-2006).


RÉSUMÉ

L'objectif du projet DISPO est de proposer des méthodes de construction et de validation de logiciels sécurisés avec une focalisation sur les propriétés liées à la disponibilité et l'absence de déni de service d'un logiciel. Les méthodes proposées seront basées sur la formalisation de politiques de sécurité à l'aide de logiques modales (temporelles, déontiques,...). Le projet vise à concevoir des techniques de validation de logiciel qui prennent en compte les méthodes récentes de conception et de structuration de logiciels en composants et aspects. Plus précisément, nous allons développer des techniques d'analyse et de transformation de programmes qui permettent d'assurer qu'une propriété soit satisfaite par un composant. Ces techniques feront usage de l'interprétation abstraite et la vérification de modèle ainsi que la nouvelle technique de tissage d'aspect d'un programme.

PARTENAIRES


THÈMES DE RECHERCHE

DISPONIBILITÉ

Avec la confidentrialité et l'intégrité, la disponibilité constitue une des trois propriétés fondamentales de la sécurité informatiques. Les travaux existants sur la propriété de disponibilité se sont intéressés aux modèles d'allocation de ressources, notamment dans les systèmes d'exploitation. L'objectif principal est de spécifier des conditions suffisantes pour empêcher des attaques en déni de service.

(la suite ...)
COMPOSANTS

La recherche en composants logiciels vise à créer une
industrie et un marché de « pièces  détachées » comme il en existe dans bien d'autres secteurs industriels arrivés à maturité. Comme pour toute pièce détachée, l'utilisation d'un composant pour la fabrication d'un assemblage (on parlera aussi de composition) requiert d'en connaître précisément  ses « propriétés ». 

(la suite ...)
ANALYSE ET TISSAGE D'ASPECTS

L'arrivée de langages de programmation de haut niveau incluant des mécanismes de sécurité ouvre la
possibilité de concevoir et de raisonner sur la sécurité d'un logiciel en s'appuyant sur des techniques proposées dans le contexte de l'analyse statique et de la transformation de programmes, en s'inspirant de la  technique de tissage de la programmation par aspects.

(la suite ...)


Publications (articles, rapports de recherche, présentations).

Thomas Jensen and al. DISPO : Disponibilité de services et composants logiciels sécurisés.
Rapport Intermédaire de l'ACI Sécurité Informatique DISPO, Avril 2005.

Julien Brunel. Deontic Logic for the Specification of System Availability.
In 6th school on MOdeling and VErifying parallel Processes MOVEP'04 (student papers),
pages 40-45, décembre 2004.

Julien Brunel. Logique déontique pour la disponibilité.
Rapport de stage DEA PS 2003-2004, IRIT, Université Paul Sabatier, Toulouse, 2004.

Julien Brunel, Jean-Paul Bodeveix, and Mamoun Filali. A state/event temporal deontic logic.
Eighth International Workshop on Deontic Logic in Computer Science (DEON2006),
Springer LNAI 4048, pages 85-100, juillet 2006.

David Cachera, Thomas Jensen, David Pichardie, and Gerardo Schneider. Certified memory usage analysis.
In Proc. Formal Methods (FM'05), 2005.

Nora Cuppens and Frédéric Cuppens : Modélisation de la disponibilité.

Frédéric Cuppens, Nora Cuppens-Boulahia, and Thierry Sans. Nomad : a security model with non atomic actions and deadlines.
In Proc. 18th IEEE Computer Security Foundations Workshop (CSFW'05), juin 2005.

Frédéric Cuppens,Nora Cuppens-Boulahia and Tony Ramard, Availability Enforcement by Obligations and Aspects Identification,
The First International Conference on Availability, Reliability and Security (AReS), Avril 2006.

Seila Nuon. Analyse de la disponibilité dans les réseaux Ad hoc.
Mémoire de DNM recherche, Université de Rennes 1, juin 2006.

Ghassan Oreiby. Spécification et Vérification du protocole OLSR.
Mémoire de DNM recherche, Université de Bordeaux 1, juin 2006.

P. Fradet and S. Hong Tuan Ha. Network Fusion.
In Wei-Ngan Chin, editor,  Second Asian Symposium, APLAS 2004, volume Springer LNCS vol. 3302, pages 21-40, 2004.

P. Fradet and S. Hong Tuan Ha. Systèmes de gestion de ressources et aspects de disponibilité.
2ème Journée Francophone sur le Développement de Logiciels par Aspects (JFDLPA 2005), septembre 2005.

P. Fradet and S. Hong Tuan Ha. Systèmes de gestion de ressources et aspects de disponibilité.
RTSI-L'objet, vol. 12/2-3, pages 183-210, 2006.

Olivier Marechal, Pascal Poizat, and Jean-Claude Royer. Checking asynchronously communicating components using Symbolic Transition Systems.
In On The Move to Meaningful Internet Systems 2004 : CoopIS, DOA, and OD- BASE,
number 3291 in Lecture Notes in Computer Science, pages 1502-1519. Springer- Verlag, 2004.

Jacques Noyé, Sebastian Pavel, and Jean-Claude Royer. A PVS experiment with asynchronous communicating components.
In 17th Workshop on Algebraic Development Techniques, Barcelona, Spain, March 2004.

S.Pavel, J.Noyé et J-C Royer : Un modèle de composant avec protocole symbolique, Journée du groupe Objets, Composants et Modèles, Mars 2005

Sebastian Pavel, Jacques Noyé, Pascal Poizat, and Jean-Claude Royer. Java Implementation of a Component Model with Explicit Symbolic Protocols.
In Proceedings of the 4th International Workshop on Software Composition (SC'05), Lecture Notes in Computer Science. Springer-Verlag, 2005.

Sebastian Pavel, Jacques Noyé, and Jean-Claude Royer. Dynamic configuration of software product lines in ArchJava.
In Robert L. Nord, editor, Software Product Lines : Third International Conference, SPLC 2004,
number 3154 in Lecture Notes in Computer Science, pages 90-109. Software Engineering Institute, Springer-Verlag, August 2004.

Pascal Poizat, Jean-Claude Royer, and Gwen Salaün. Formal methods for component description, coordination and adaptation.
In Proceedings of the ECOOP Workshop on Coordination and Adaptation Techniques for Software Entities (WCAT'04), Oslo, Norway, June 2004.

J-C Royer : Etude de cas : Systèmes de réservation de billets.

Jean-Claude Royer. A framework for the GAT temporal logic.
In Proceedings of the 13th International Conference on Intelligent and Adaptive Systems and Software Engineering (IASSE'04),
pages 275-280, Nice, France, July 2004. ISCA.

Jean-Claude Royer and Michael Xu. Analysing Mailboxes of Asynchronous Communicating Components.
In D. C. Schmidt R. Meersman, Z. Tari and al., editors, On The Move to Meaningful Internet Systems 2003 : Coopis, DOA, and ODBASE,
volume 2888 of Lecture Notes in Computer Science, pages 1421-1438. Springer-Verlag, 2003.


Références.

Modèles de disponibilité :
Taxonomies de ressources
Modèles de composants :


BIBLIOGRAPHIE du projet.




Réunion, 18 novembre 2003, IRISA.


Réunion, 24 mars 2004, Enst Bretagne.


Réunion, 23 septembre 2004, EMN.


Réunion, 10 mai 2005, IRIT.


Réunion, 23 septembre 2005, IRISA.


Réunion, 8 et 9 juin 2006, Luchon.


Réunion, 22 septembre 2006, IRISA.