Non-interference in Partial Order Models
- 1 June 2015
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE) in 2015 15th International Conference on Application of Concurrency to System Design
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.Keywords
This publication has 12 references indexed in Scilit:
- Non-interference by UnfoldingLecture Notes in Computer Science, 2014
- Deciding Selective Declassification of Petri NetsLecture Notes in Computer Science, 2012
- On the Decidability of Non Interference over Unbounded Petri NetsElectronic Proceedings in Theoretical Computer Science, 2011
- On Intransitive Non-interference in Some Models of ConcurrencyLecture Notes in Computer Science, 2011
- Structural non-interference in elementary and trace netsMathematical Structures in Computer Science, 2009
- Secure Requirements Elicitation Through Triggered Message Sequence ChartsLecture Notes in Computer Science, 2004
- High-Level Message Sequence Charts and ProjectionsLecture Notes in Computer Science, 2003
- Information Flow Control and Applications — Bridging a Gap —Lecture Notes in Computer Science, 2001
- Message Sequence Graphs and Decision Problems on Mazurkiewicz TracesLecture Notes in Computer Science, 1999
- Security Policies and Security ModelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982