Abstract
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.
Work supported by the project Récré (ANR) and the MIUR PRIN project CINA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
Focardi, R., Gorrieri, R.: Classification of security properties (Part I: Information flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)
Ryan, P., Schneider, Y.: Process algebra and non-interference. Journal of Computer Security 9, 75–103 (2001)
Mantel, H.: Possibilistic definitions of security - an assembly kit. In: CSFW, pp. 185–199. IEEE Computer Society (2000)
Busi, N., Gorrieri, R.: Structural non-interference in elementary and trace nets. Mathematical Structures in Computer Science 19, 1065–1090 (2009)
Best, E., Darondeau, P., Gorrieri, R.: On the decidability of non interference over unbounded Petri nets. In: Proceedings of SecCo 2010. EPTCS, vol. 51, pp. 16–33 (2010)
Nielsen, M., Plotkin, G., Winskel, G.: Petri Nets, Event Structures and Domains, Part 1. TCS 13, 85–108 (1981)
Esparza, J., Heljanko, K.: Unfoldings - A Partial order Approach to Model Checking. EACTS Monographs in Theoretical Computer Science. Springer (2008)
Rodríguez, C., Schwoon, S.: Cunf: A tool for unfolding and verifying Petri nets with read arcs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 492–495. Springer, Heidelberg (2013)
Accorsi, R., Lehmann, A.: Automatic information flow analysis of business process models. In: Barros, A., Gal, A., Kindler, E. (eds.) BPM 2012. LNCS, vol. 7481, pp. 172–187. Springer, Heidelberg (2012)
Frau, S., Gorrieri, R., Ferigato, C.: Petri net security checker: Structural non-interference at work. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 210–225. Springer, Heidelberg (2009)
McMillan, K.L.: A technique of state space search based on unfolding. Form. Methods Syst. Des. 6, 45–65 (1995)
Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings. Acta Informatica 40, 95–118 (2003)
Meseguer, J., Montanari, U., Sassone, V.: Representation theorems for petri nets. In: Freksa, C., Jantzen, M., Valk, R. (eds.) Foundations of Computer Science. LNCS, vol. 1337, pp. 239–249. Springer, Heidelberg (1997)
Best, E., Grahlmann, B.: PEP Documentation and User Guide 1.8 (1998)
Frau, S., Gorrieri, R., Ferigato, C.: Petri net security checker: Structural non-interference at work. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 210–225. Springer, Heidelberg (2009)
Wolf, K.: Generating Petri net state spaces. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 29–42. Springer, Heidelberg (2007)
Dijkstra, E.: Solution of a problem in concurrent programming control. Communication of the ACM 8, 569 (1965)
Haar, S.: Types of asynchronous diagnosability and the reveals-relation in occurrence nets. IEEE Transactions on Automatic Control 55, 2310–2320 (2010)
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)
Devillers, R., Klaudel, H., Koutny, M.: A compositional Petri net translation of general pi-calculus terms. Formal Asp. Comput. 20, 429–450 (2008)
Meyer, R., Khomenko, V., Hüchting, R.: A polynomial translation of π-calculus (FCP) to safe Petri nets. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 440–455. Springer, Heidelberg (2012)
van Glabbeek, R., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems. Acta Informatica 37, 229–327 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baldan, P., Carraro, A. (2014). Non-interference by Unfolding. In: Ciardo, G., Kindler, E. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2014. Lecture Notes in Computer Science, vol 8489. Springer, Cham. https://doi.org/10.1007/978-3-319-07734-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-07734-5_11
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07733-8
Online ISBN: 978-3-319-07734-5
eBook Packages: Computer ScienceComputer Science (R0)