Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |

berard:hal-01138787

B. Bérard, L. Hélouet, J. Mullins. Non-interference in partial order models. In ACSD 2015, ACSD 2015, Brussels, Belgium, June 2015.

Download [help]

Download paper: (link)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

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

Contact

Loic Hélouet http://people.irisa.fr/Loic.Helouet/

BibTex Reference

@InProceedings{berard:hal-01138787,
   Author = {Bérard, B. and Hélouet, L. and Mullins, J.},
   Title = {Non-interference in partial order models},
   BookTitle = {ACSD 2015},
   Series = {ACSD 2015},
   Publisher = {IEEE},
   Address = {Brussels, Belgium},
   Month = {June},
   Year = {2015}
}

EndNote Reference [help]

Get EndNote Reference (.ref)