A framework for automatic generation of security controller

Abstract : This paper concerns the study, the development and the synthesis of mechanisms for guaranteeing the security of complex systems, i.e., systems composed by several interacting components. A complex system under analysis is described as an open system, i.e., a system in which an unspecified component (a component whose behaviour is not fixed in advance) interacts with the known part of the system. Within this formal approach, we propose techniques that aim to synthesize controller programs able to guarantee that, for all possible behaviours of the unspecified component, the system should work properly, e.g., it should be able to satisfy a certain property. For performing this task, we first need to identify the set of necessary and sufficient conditions that the unspecified component has to satisfy in order to ensure that the whole system is secure. Hence, by exploiting satisfiability procedures for temporal logic, we automatically synthesize an appropriate controller program that forces the unspecified component to meet these conditions. This will ensure the security of the whole system.
Type de document :
Article dans une revue
Software Testing, Verification and Reliability, Wiley, 2010, 〈10.1002/000〉
Liste complète des métadonnées

Littérature citée [51 références]  Voir  Masquer  Télécharger

Contributeur : Emmanuelle Grousset <>
Soumis le : mardi 16 novembre 2010 - 19:01:21
Dernière modification le : jeudi 18 novembre 2010 - 12:52:40
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 15:46:21


Fichiers produits par l'(les) auteur(s)




Fabio Martinelli, Ilaria Matteucci. A framework for automatic generation of security controller. Software Testing, Verification and Reliability, Wiley, 2010, 〈10.1002/000〉. 〈inria-00536752〉



Consultations de la notice


Téléchargements de fichiers