Non-interference by Unfolding
The concept of non-interference has been introduced to characterise the absence of undesired information flows in a computing system. Although it is often explained referring to an informal notion of causality - the activity involving the part of the system with higher level of confidentiality should not cause any observable effect at lower levels - it is almost invariably formalised in terms of interleaving semantics. Here we focus on Petri nets and on the BNDC property (Bisimilarity-based Non-Deducibility on Composition), a formalisation of non-interference widely studied in the literature. We show that BNDC admits natural characterisations based on the unfolding semantics - a classical true concurrent semantics for Petri nets - in terms of causalities and conflicts between high and low level activities. This leads to an algorithm for checking BNDC for safe Petri nets which relies on the construction of suitable complete prefixes of the unfolding. A prototype tool provides very promising results.
KeywordsHigh Transition State Explosion Problem Reachable Marking Undesired Information Causal Reduct
Unable to display preview. Download preview PDF.
- 1.Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 11–20. IEEE Computer Society (1982)Google Scholar
- 4.Mantel, H.: Possibilistic definitions of security - an assembly kit. In: CSFW, pp. 185–199. IEEE Computer Society (2000)Google Scholar
- 8.Esparza, J., Heljanko, K.: Unfoldings - A Partial order Approach to Model Checking. EACTS Monographs in Theoretical Computer Science. Springer (2008)Google Scholar
- 15.Best, E., Grahlmann, B.: PEP Documentation and User Guide 1.8 (1998)Google Scholar
- 20.Gorrieri, R., Montanari, U.: SCONE: A simple calculus of nets. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 2–30. Springer, Heidelberg (1990)Google Scholar