Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Journal articles

Non-interference in partial order models

Béatrice Bérard 1, * Loïc Hélouët 2 John Mullins 3 
* Corresponding author
1 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
2 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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 of behaviors. Observations are naturally captured by partial order au-tomata, a formalism that generalizes HMSCs and permits to assemble partial orders. We show that equivalence or inclusion properties for HMSCs (hence for partial order automata) are undecidable, which means in particular that NI is undecidable for HMSCs. We hence consider decidable subclasses of partial order automata and HMSCs. Finally, we define 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.
Document type :
Journal articles
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Loic Helouet Connect in order to contact the contributor
Submitted on : Tuesday, October 11, 2016 - 3:18:24 PM
Last modification on : Monday, April 4, 2022 - 9:28:21 AM
Long-term archiving on: : Saturday, February 4, 2017 - 7:28:36 PM


Files produced by the author(s)



Béatrice Bérard, Loïc Hélouët, John Mullins. Non-interference in partial order models. ACM Transactions on Embedded Computing Systems (TECS), ACM, 2017, Application and Theory of Petri Nets and Other Models of Concurrency: Special Issue of Selected Papers from Petri Nets 2015, 16 (2), pp.44:1-44:34. ⟨10.1145/2984639⟩. ⟨hal-01379451⟩



Record views


Files downloads