Non-interference in partial order models

Béatrice Bérard 1 Loïc Hélouët 2 John Mullins 3
1 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
2 SUMO - SUpervision of large MOdular and distributed systems
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : Non-interference (NI) is a property of systems stating that confidential actions should not cause effects observable by unauthorized users. Several variants of NI have been studied for many types of models, but rarely for true concurrency or unbounded models. This work investigates NI for High-level Message Sequence Charts (HMSC), a scenario language for the description of distributed systems, based on composition of partial orders. We first propose a general definition of security properties in terms of equivalence among observations, and show that these properties, and in particular NI are undecidable for HMSCs. We hence consider weaker local properties, describing situations where a system is attacked by a single agent, and show that local NI is decidable. We then refine local NI to a finer notion of causal NI that emphasizes causal dependencies between confidential actions and observations, and extend it to causal NI with (selective) declassification of confidential events. Checking whether a system satisfies local and causal NI and their declassified variants are PSPACE-complete problems.
Type de document :
Communication dans un congrès
ACSD'15 - 15th International Conference on Application of Concurrency to System Design, Jun 2015, Brussels, Belgium. IEEE, pp.80-89, 〈http://www.ulb.ac.be/di/verif/pn2015acsd2015/index.html〉. 〈10.1109/ACSD.2015.11〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01138787
Contributeur : Loic Helouet <>
Soumis le : jeudi 2 avril 2015 - 16:35:10
Dernière modification le : vendredi 31 août 2018 - 09:25:57
Document(s) archivé(s) le : mardi 18 avril 2017 - 09:37:26

Fichier

niacsd.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Béatrice Bérard, Loïc Hélouët, John Mullins. Non-interference in partial order models. ACSD'15 - 15th International Conference on Application of Concurrency to System Design, Jun 2015, Brussels, Belgium. IEEE, pp.80-89, 〈http://www.ulb.ac.be/di/verif/pn2015acsd2015/index.html〉. 〈10.1109/ACSD.2015.11〉. 〈hal-01138787〉

Partager

Métriques

Consultations de la notice

946

Téléchargements de fichiers

134