Advertisement

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.

Keywords

High Transition State Explosion Problem Reachable Marking Undesired Information Causal Reduct 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Ryan, P., Schneider, Y.: Process algebra and non-interference. Journal of Computer Security 9, 75–103 (2001)CrossRefGoogle Scholar
  4. 4.
    Mantel, H.: Possibilistic definitions of security - an assembly kit. In: CSFW, pp. 185–199. IEEE Computer Society (2000)Google Scholar
  5. 5.
    Busi, N., Gorrieri, R.: Structural non-interference in elementary and trace nets. Mathematical Structures in Computer Science 19, 1065–1090 (2009)MathSciNetCrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Nielsen, M., Plotkin, G., Winskel, G.: Petri Nets, Event Structures and Domains, Part 1. TCS 13, 85–108 (1981)CrossRefGoogle Scholar
  8. 8.
    Esparza, J., Heljanko, K.: Unfoldings - A Partial order Approach to Model Checking. EACTS Monographs in Theoretical Computer Science. Springer (2008)Google Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    McMillan, K.L.: A technique of state space search based on unfolding. Form. Methods Syst. Des. 6, 45–65 (1995)CrossRefGoogle Scholar
  13. 13.
    Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings. Acta Informatica 40, 95–118 (2003)MathSciNetCrossRefGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Best, E., Grahlmann, B.: PEP Documentation and User Guide 1.8 (1998)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Wolf, K.: Generating Petri net state spaces. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 29–42. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Dijkstra, E.: Solution of a problem in concurrent programming control. Communication of the ACM 8, 569 (1965)CrossRefGoogle Scholar
  19. 19.
    Haar, S.: Types of asynchronous diagnosability and the reveals-relation in occurrence nets. IEEE Transactions on Automatic Control 55, 2310–2320 (2010)MathSciNetCrossRefGoogle Scholar
  20. 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
  21. 21.
    Devillers, R., Klaudel, H., Koutny, M.: A compositional Petri net translation of general pi-calculus terms. Formal Asp. Comput. 20, 429–450 (2008)CrossRefGoogle Scholar
  22. 22.
    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)CrossRefGoogle Scholar
  23. 23.
    van Glabbeek, R., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems. Acta Informatica 37, 229–327 (2001)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Paolo Baldan
    • 1
  • Alberto Carraro
    • 2
    • 3
  1. 1.Dipartimento di MatematicaUniversitá di PadovaItaly
  2. 2.DAISUniversità Ca’ Foscari di VeneziaItaly
  3. 3.ANR Projet RécréFrance

Personalised recommendations