A Causal View on Non-Interference

• Autorzy: Baldan P. , Carraro A.

Identyfikatory

DOI

10.3233/FI-2015-1243

• Języki publikacji: EN

Abstrakty

EN

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 (Bisimilarity-based Non-Deducibility on Composition) property, 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 algorithms for checking BNDC on various classes of Petri nets, based on the construction of suitable complete prefixes of the unfolding. We also developed a prototype tool UBIC (Unfolding-Based Interference Checker), working on safe Petri nets, which provides promising results in terms of efficiency.

Słowa kluczowe

EN

Petri nets; non-interference; bisimilarity-based non-deducibility on composition; BNDC; unfolding; true concurrency; verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2015
• Tom: Vol. 140, nr 1
• Strony: 1--38
• Opis fizyczny: Bibliogr. 40 poz., rys., tab.

Twórcy

autor

Baldan P.

• Dipartimento di Matematica, Universita di Padova Via Trieste, 63 35121 Padova, Italy

autor

Carraro A.

• DAIS, Universit`a Ca’ Foscari Venezia Dorsoduro 3246 - 30123 Venezia, Italy

Bibliografia

• [1] Accorsi, R., Lehmann, A.: Automatic Information Flow Analysis of Business Process Models, in: Proceedings of BPM’12 (A. Barros, A. Gal, E. Kindler, Eds.), vol. 7481 of LNCS, Springer, 2012, 172–187.
• [2] Baldan, P., Burato, F., Carraro, A.: Intransitive Non-interference by Unfolding, in: Proceedings of FACS’14 (I. Lanese, E. Madelaine, Eds.), vol. 8997 of LNCS, Springer, 2014, 269–287.
• [3] Baldan, P., Carraro, A.: Non-interference by Unfolding, in: Proceedings of Petri Nets’14 (G. Ciardo, E. Kindler, Eds.), vol. 8489 of LNCS, Springer, 2014, 190–209.
• [4] Best, E., Darondeau, P., Gorrieri, R.: On the Decidability of Non Interference over Unbounded Petri Nets, in: Proceedings of SecCo’10 (K. Chatzikokolakis, V. Cortier, Eds.), vol. 51 of EPTCS, Open Publishing Association, 2010, 16–33.
• [5] Best, E., Grahlmann, B.: PEP Documentation and User Guide 1.8, 1998.
• [6] Bossi, A., Piazza, C., Rossi, S.: Modelling Downgrading in Information Flow Security, in: Proceedings of CSFW’04, IEEE Computer Society, 2004, 187–201.
• [7] Bryans, J., Koutny, M., Ryan, P.: Modelling Dynamic Opacity Using Petri Nets with Silent Actions, in: Proceedings of FAST’05 (T. Dimitrakos, F. Martinelli, Eds.), vol. 173 of LNCS, Springer, 2005, 159–172.
• [8] Busi, N., Gorrieri, R.: Structural non-interference in elementary and trace nets, Mathematical Structures in Computer Science, 19(6), 2009, 1065–1090.
• [9] Denning, D. E.: A Lattice Model of Secure Information Flow, Communication of the ACM, 19(5), 1976, 236–243.
• [10] Desel, J., Juhàs, G., Neumair, C.: Finite Unfoldings of Unbounded Petri Nets, in: Proceedings of ATPN’04, vol. 3099 of LNCS, Springer, 2004, 157–176.
• [11] Devillers, R., Klaudel, H., Koutny, M.: A compositional Petri net translation of general pi-calculus terms, Formal Asp. Comput., 20(4-5), 2008, 429–450.
• [12] Dijkstra, E.: Solution of a problem in concurrent programming control, Communication of the ACM, 8(9), 1965, 569.
• [13] Esparza, J., Heljanko, K.: Unfoldings - A Partial order Approach to Model Checking, EACTS Monographs in Theoretical Computer Science, Springer, 2008.
• [14] Esparza, J., Römer, S., Vogler, W.: An Improvement of McMillan’s Unfolding Algorithm, Formal Methods in System Design, 20(20), 2002, 285–310.
• [15] Focardi, R., Gorrieri, R.: Classification of Security Properties (Part I: Information Flow), in: Proceedings of FOSAD’00, Springer, 2001, 331–396.
• [16] Frau, S., Gorrieri, R., Ferigato, C.: Petri Net Security Checker: Structural Non-interference at Work, in: Proceedings of FAST’08 (P. Degano, F. Guttman, J. Martinelli, Eds.), vol. 5491 of LNCS, Springer, 2008, 210–225.
• [17] van Glabbeek, R., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems, Acta Informatica, 37(4/5), 2001, 229–327.
• [18] Goguen, J. A., Meseguer, J.: Security policies and security models, in: Proceedings of the IEEE Symposium on Security and Privacy, IEEE Computer Society, 1982, 11–20.
• [19] Gorrieri, R., Montanari, U.: SCONE: A Simple Calculus of Nets, in: Proceedings of CONCUR’90 (J. C. M. Baeten, J. W. Klop, Eds.), vol. 458 of LNCS, Springer, 1990, 2–31.
• [20] Gorrieri, R., Vernali, M.: On Intransitive Non-interference in Some Models of Concurrency, in: Proceedings of FOSAD’11 (A. Aldini, R. Gorrieri, Eds.), vol. 6858 of LNCS, Springer, 2011, 125–151.
• [21] Haar, S.: Types of Asynchronous Diagnosability and the Reveals-Relation in Occurrence Nets, IEEE Transactions on Automatic Control, 55(10), 2010, 2310–2320.
• [22] Hack, M.: Decidability Questions for Petri Nets, Outstanding Dissertations in the Computer Sciences, Garland Publishing, 1975.
• [23] Heljanko, K.: Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets, Fundamenta Informaticae, 37(3), 1999, 247–268.
• [24] Khomenko, V.: Model checking based on prefixes of Petri Net unfoldings, Ph.D. Thesis, University of New Castle Upon Tyne, 2003, https://theses.ncl.ac.uk/dspace/bitstream/10443/743/1/ Khomenko03.pdf.
• [25] Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings, Acta Informatica, 40, 2003, 95–118.
• [26] Mantel, H.: Possibilistic Definitions of Security - An Assembly Kit, in: Proceedings of CSFW’00, IEEE Computer Society, 2000, 185–199.
• [27] McCullough, D.: Noninterference and the Composability of Security Properties, in: IEEE Symposium on Security and Privacy, IEEE Computer Society, 1988, 178–186.
• [28] McMillan, K. L.: A technique of state space search based on unfolding, Form. Methods Syst. Des., 6(1), 1995, 45–65.
• [29] Melzer, S., R¨omer, S.: Deadlock Checking Using Net Unfoldings, in: Proceedings of CAV’97 (O. Grumberg, Ed.), vol. 1254 of LNCS, Springer, 1997, 352–363.
• [30] Meseguer, J., Montanari, U., Sassone, V.: Representation Theorems for Petri Nets, in: Foundations of Computer Science: Potential - Theory - Cognition (C. Freksa, M. Jantzen, R. Valk, Eds.), vol. 1337 of LNCS, Springer, 1997, 239–249.
• [31] Meyer, R., Khomenko, V., H¨utchting, R.: A Polynomial Translation of pi-calculus FCPs to Safe Petri Nets, Logical Methods in Computer Science, 9(3), 2013.
• [32] Mokhov, A., Khomenko, V., Yakovlev, A.: Flat Arbiters, Fundamenta Informaticae, 108(1-2), 2011, 63–90.
• [33] Nielsen, M., Plotkin, G., Winskel, G.: Petri Nets, Event Structures and Domains, Part 1, Theoretical Computer Science, 13, 1981, 85–108.
• [34] Rodríguez, C.: CUNF, https://code.google.com/p/cunf/.
• [35] Rodríguez, C., Schwoon, S.: Cunf: A Tool for Unfolding and Verifying Petri Nets with Read Arcs, in: Proceedings of ATVA’13 (D. Van Hung, M. Ogawa, Eds.), vol. 8172 of LNCS, Springer, 2013, 492–495.
• [36] Rushby, J. M.: Design and Verification of Secure Systems, in: Proceedings of SOSP’81, ACM, 1981, 12–21.
• [37] Ryan, P., Schneider, Y.: Process Algebra and Non-Interference, Journal of Computer Security, 9(1/2), 2001, 75–103.
• [38] Schwoon, S.: MOLE - A Petri Net Unfolder, http://www.lsv.ens-cachan.fr/~schwoon/tools/mole/.
• [39] Wittbold, J., Johnson, D.: Information Flow in Nondeterministic Systems, in: IEEE Symposium on Security and Privacy, IEEE Computer Society, 1990, 148–161.
• [40] Wolf, K.: Generating Petri Net State Spaces, in: Proceedings of ICATPN’07, vol. 4546 of LNCS, Springer, 2007, 29–42.