Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Aspects of Component Software

FACS 2014: Formal Aspects of Component Software pp 269–287Cite as

Intransitive Non-Interference by Unfolding

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8997))

Abstract

Non-interference characterises the absence of undesired information flows in a computing system, by asking that actions with higher level of confidentiality do not cause any observable effect at the lower levels. In many concrete applications, this requirement is too strict and the abstract model is enriched with some form of downgrading, namely with the possibility of declassifying information, thus allowing for a controlled form of leakage. This paper focuses on BINI (Bisimilarity-based Intransitive non-interference), a formalisation of non-interference with downgrading in the setting of Petri nets. Generalising some previous works, we provide a causal characterisation of BINI in terms of the unfolding semantics, a true concurrent semantics of Petri nets. Building on this, we design an algorithm for checking BINI on safe Petri nets which relies on the construction of suitable complete prefixes of the unfolding. The algorithm is implemented in a prototype tool and some preliminary tests are quite encouraging as they suggest that the management of downgrading does not cause any significant performance decay.

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  2. Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20 (1982)

    Google Scholar 

  3. Rushby, J.M.: Design and verification of secure systems. In: SOSP 1981, pp. 12–21. ACM (1981)

    Google Scholar 

  4. Haigh, J.T., Young, W.D.: Extending the noninterference version of mls for sat. IEEE Trans. Softw. Eng. 13(2), 141–150 (1987)

    Article  Google Scholar 

  5. Rushby, J.: Noninterference, transitivity and channel-control security policies. Technical report. Technical report CSL-92-02, SRI International (1992)

    Google Scholar 

  6. Mantel, H., Sands, D.: Controlled declassification based on intransitive noninterference. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 129–145. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Bossi, A., Piazza, C., Rossi, S.: Modelling downgrading in information flow security. In: CSFW2004, pp. 187–201. IEEE (2004)

    Google Scholar 

  8. Best, E., Darondeau, P., Gorrieri, R.: On the decidability of non interference over unbounded Petri nets. In: SecCo 2010. EPTCS, vol. 51, pp. 16–33 (2010)

    Google Scholar 

  9. Gorrieri, R., Vernali, M.: On intransitive non-interference in some models of concurrency. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2011. LNCS, vol. 6858, pp. 125–151. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  10. Focardi, R., Gorrieri, R., Martinelli, F.: Classification of security properties. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2001. LNCS, vol. 2946, pp. 139–185. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. McCullough, D.: Noninterference and the composability of security properties. In: IEEE Symposium on Security and Privacy, pp. 178–186. IEEE (1988)

    Google Scholar 

  12. Wittbold, J., Johnson, D.: Information flow in nondeterministic systems. In: IEEE Symposium on Security and Privacy, pp. 148–161. IEEE (1990)

    Google Scholar 

  13. Ryan, P., Schneider, Y.: Process algebra and non-interference. J. Comput. Secur. 9(1/2), 75–103 (2001)

    Google Scholar 

  14. Mantel, H.: Possibilistic definitions of security - an assembly kit. In: CSFW 2000, pp. 185–199. IEEE (2000)

    Google Scholar 

  15. Busi, N., Gorrieri, R.: Structural non-interference in elementary and trace nets. Math. Struct. Comput. Sci. 19(6), 1065–1090 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  16. Baldan, P., Carraro, A.: Non-interference by unfolding. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 190–209. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  17. Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, part 1. Theor. Comput. Sci. 13, 85–108 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  18. Esparza, J., Heljanko, K.: Unfoldings - A Partial order Approach to Model Checking. EACTS Monographs in Theoretical Computer Science. Springer, Heidelberg (2008)

    Google Scholar 

  19. Baldan, P., Burato, F., Carraro, A.: UBIC2: unfolding-based interference checker 2 (2014). https://bitbucket.org/fburato/ubic2/

  20. Technology, S.: ANICA: automated non-interference check assistant (2011). http://service-technology.org/anica

  21. McMillan, K.L.: A technique of state space search based on unfolding. Formal Meth. Syst. Des. 6(1), 45–65 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  22. Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings. Acta Informatica 40, 95–118 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  23. 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)

    Chapter  Google Scholar 

  24. Gorrieri, R., Montanari, U.: SCONE: a simple calculus of nets. CONCUR 1990. LNCS, vol. 458, pp. 2–31. Springer, Heidelberg (1990)

    Google Scholar 

  25. Devillers, R., Klaudel, H., Koutny, M.: A compositional Petri net translation of general pi-calculus terms. Formal Aspects Comput. 20(4–5), 429–450 (2008)

    Article  MATH  Google Scholar 

  26. Meyer, R., Khomenko, V., Hüchting, R.: A polynomial translation of \(\pi \)-calculus (FCP) to safe Petri nets. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 440–455. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  27. Baldan, P., Corradini, A., König, B., Schwoon, S., Rodríguez, C.: Efficient unfolding of contextual Petri nets. Theor. Comput. Sci. 449(1), 2–22 (2012)

    Article  MATH  Google Scholar 

  28. Best, E., Darondeau, P.: Deciding selective declassification of Petri nets. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 290–308. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  29. Bryans, J., Koutny, M., Ryan, P.: Modelling dynamic opacity using Petri nets with silent actions. In: Dimitrakos, T., Martinelli, F. (eds.) FAST. IIFIP, vol. 173, pp. 159–172. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  30. Haar, S.: Types of asynchronous diagnosability and the reveals-relation in occurrence nets. IEEE Trans. Autom. Control 55(10), 2310–2320 (2010)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

We are grateful to the the anonymous referees for their insightful comments and suggestions on the submitted version of this paper.

Author information

Authors and Affiliations

  1. Dipartimento di Matematica, Università di Padova, Padua, Italy

    Paolo Baldan & Francesco Burato

  2. DAIS, ANR Projet Récré, Università Ca’ Foscari, Venice, Italy

    Alberto Carraro

Authors
  1. Paolo Baldan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Francesco Burato
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alberto Carraro
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Paolo Baldan .

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, University of bologna, Bologna, Italy and Inria Sophia Antipolis - Méditerranée, Sophia Antipolis, France

    Ivan Lanese

  2. Inria Sophia Antipolis - Méditerranée, Sophia Antipolis, France

    Eric Madelaine

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Baldan, P., Burato, F., Carraro, A. (2015). Intransitive Non-Interference by Unfolding. In: Lanese, I., Madelaine, E. (eds) Formal Aspects of Component Software. FACS 2014. Lecture Notes in Computer Science(), vol 8997. Springer, Cham. https://doi.org/10.1007/978-3-319-15317-9_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-15317-9_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-15316-2

  • Online ISBN: 978-3-319-15317-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation