Nos partenaires

CNRS

Rechercher





Accueil du site > Français > Thèmes de recherche > Thème 7 - Sûreté de développement du logiciel > Equipe MACAO > Propositions de stages, thèses et post-doc > Stages de Master 2

Langage de spécification des propriétés et des contraintes de sécurité pour les patrons (23/12/2013)

Contact : Brahim Hamid

Laboratoire IRIT — Thème 7 — Equipe MACAO

Direction et unité d’accueil

Contexte

Dans le cadre de projets collaboratifs, nous développons un ensemble de DSML pour faire face à un ensemble de préoccupations liées au développement de systèmes embarqués contraints en ressources, en présence de forte exigences de sécurité et de fiabilité. Dans nos travaux, le patron de sécurité est l’élément central pour décrire des solutions de modélisation des architectures logicielles sécurisées. Il est spécifié par des spécialistes de sécurité pour être utilisé par des développeurs afin d’intégrer l’ingénierie de sécurité et l’ingénierie logicielle. Un DSL pour spécifier les patrons de sécurité ainsi qu’un DSL pour spécifier les systèmes de patrons ont été proposés au sein de notre équipe. Dans ce méta-modèle, le patron de sécurité est représenté sous la forme d’un sous-système fournissant un ensemble d’interfaces et visant des propriétés de sécurité. Les interfaces exhibent les fonctionnalités du patron, afin de gérer son application et de gérer les interactions avec les protocoles et les primitives de sécurité liés au domaine du système.

Objectif

L’objectif de ce stage est de proposer un langage de spécification des propriétés et des contraintes de sécurité visées et satisfaites, respectivement par le patron. Ce langage est étroitement lié à un framework formel, de spécification et de validation des propriétés de sécurité, étudié dans le cadre du projet TERESA. En outre, ce langage permettra de manipuler un ensemble d’artefacts définis sous la forme de bibliothèques de catégories et d’unités de mesures. Il sera demandé également d’implanter un éditeur xtext et ses transformations pour étendre la suite d’outils Semcomdt que nous avons développé. Il offrira la possibilité de générer, d’éditer /spécifier des propriétés et des contraintes pour les patrons et leur validation.

Domaines de spécialité requis

Génie logiciel (EG), MDE, DSL, UML, patrons, sécurité, bon niveau d’anglais requis

Langages

Java, XML, XSD

Environnement et Logiciels

Eclipse, EMF, Xtext, Papyrus, Linux

Formation souhaitée (niveau)

Master recherche / Ecole d’ingénieur

Bibliographie

  • (1) B. Hamid, C. Percebois. Model-based Specification and Validation of Security and Dependability Patterns. International Symposium on Foundations & Practice of Security (FPS 2013), Springer.
  • (2) B. Hamid, S. Gurgens, C. Jouvray, N. Desnos : Enforcing S&D Pattern Design in RCES with Modeling and Formal Approaches. MoDELS 2011
  • (3) A. Fuchs, Sigrid Gurgens, C. Rudolph. Formal Notions of Trust andConfidentiality - Enabling Reasoning about S ystem Security. Journal of Information Processing, 19:274–291, 2011
  • (4) Deliverables TERESA