Advertisement

Information Flow Security and Recursive Systems

  • Annalisa Bossi
  • Damiano Macedonio
  • Carla Piazza
  • Sabina Rossi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2841)

Abstract

Information flow security in a multilevel system aims at guaranteeing that no high level information is revealed to low level users, even in the presence of any possible malicious process. Persistent_BNDC (P_BNDC, for short) is an information-flow security property which is suitable to deal with processes in dynamic contexts. In this work we show that P_BNDC is compositional with respect to the replication operator. Then, by exploiting the compositionality properties of the class of P_BNDC processes, we define a proof system which provides a very efficient technique for the stepwise development and the verification of recursively defined P_BNDC processes.

Keywords

Proof System Security Property Parallel Composition Recursive Process Replication Operator 
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.
    Abadi, M., Lamport, L.: Conjoining Specifications. ACM Transactions on Programming Languages and Systems (TOPLAS) 17(3), 507–535 (1995)CrossRefGoogle Scholar
  2. 2.
    Bodei, C., Degano, P., Nielson, F., Nielson, H.: Static Analysis for the π-calculus with Applications to Security. Information and Computation 168(1), 68–92 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Bossi, A., Focardi, R., Piazza, C., Rossi, S.: Transforming Processes to Ensure and Check Information Flow Security. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 271–286. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Bossi, A., Focardi, R., Piazza, C., Rossi, S.: A Proof System for Information Flow Security. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, Springer, Heidelberg (2003) (to appear)CrossRefGoogle Scholar
  5. 5.
    Bossi, A., Macedonio, D., Piazza, C., Rossi, S.: P BNDC and Replication. Technical Report CS-2003-6, Dipartimento di Informatica, Università Ca’ Foscari di Venezia, Italy (2003), http://www.dsi.unive.it/ricerca/TR/index.htm
  6. 6.
    Braghin, C., Cortesi, A., Focardi, R.: Control Flow Analysis of Mobile Ambients with Security Boundaries. In: Proc. Int. Conference on Formal Methods for Open Object-Based Distributed Systems (IFIPM 2002), pp. 197–212. Kluwer, Dordrecht (2002)Google Scholar
  7. 7.
    Busi, N., Gabbrielli, M., Zavattaro, G.: Replication vs. Recursive Definitions in Channel Based Calculi. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, Springer, Heidelberg (2003) (to appear) CrossRefGoogle Scholar
  8. 8.
    McCullough, D.: A Hookup Theorem for Multilevel Security. IEEE Transactions on Software Engineering 16(6), 563–568 (1990)CrossRefGoogle Scholar
  9. 9.
    Focardi, R., Gorrieri, R.: Classification of Security Properties (Part I: Information Flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, p. 331. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. 10.
    Focardi, R., Gorrieri, R., Martinelli, F.: Non Interference for the Analysis of Cryptographic Protocols. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 744–755. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  11. 11.
    Focardi, R., Rossi, S.: Information Flow Security in Dynamic Contexts. In: Proc. of the IEEE Computer Security Foundations Workshop (CSFW 2002), pp. 307–319. IEEE Comp. Soc. Press, Los Alamitos (2002)Google Scholar
  12. 12.
    Foley, S.N.: A Universal Theory of Information Flow. In: Proc. of the IEEE Symposium on Security and Privacy, pp. 116–122. IEEE Comp. Soc. Press, Los Alamitos (1987)Google Scholar
  13. 13.
    Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proc. of the IEEE Symposium on Security and Privacy, pp. 11–20. IEEE Comp. Soc. Press, Los Alamitos (1982)Google Scholar
  14. 14.
    Hennessy, M., Riely, J.: Information Flow vs. Resource Access in the Asynchronous Pi-calculus. ACM Transactions on Programming Languages and Systems (TOPLAS) 24(5), 566–591 (2002)CrossRefGoogle Scholar
  15. 15.
    Mantel, H.: On the Composition of Secure Systems. In: Proc. of the IEEE Symposium on Security and Privacy, pp. 88–101. IEEE Comp. Soc. Press, Los Alamitos (2002)Google Scholar
  16. 16.
    Martinelli, F.: Partial Model Checking and Theorem Proving for Ensuring Security Properties. In: Proc. of the IEEE Computer Security Foundations Workshop (CSFW 1998), pp. 44–52. IEEE Comp. Soc. Press, Los Alamitos (1998)Google Scholar
  17. 17.
    McLean, J.: Security Models and Information Flow. In: Proc. of the IEEE Symposium on Security and Privacy, pp. 180–187. IEEE Comp. Soc. Press, Los Alamitos (1990)Google Scholar
  18. 18.
    McLean, J.: A General Theory of Composition for a Class of “Possibilistic” Security Properties. IEEE Transactions on Software Engineering 22(1), 53–67 (1996)CrossRefGoogle Scholar
  19. 19.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  20. 20.
    Milner, R.: The Polyadic Pi-calculus: a tutorial. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification, pp. 203–246. Springer, Heidelberg (1993)Google Scholar
  21. 21.
    Ryan, P., Schneider, S.: Process Algebra and Non-Interference. Journal of Computer Security 9(1/2), 75–103 (2001)Google Scholar
  22. 22.
    Sabelfeld, A., Myers, A.C.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communication 21(1), 5–19 (2003)CrossRefGoogle Scholar
  23. 23.
    Sabelfeld, A., Sands, D.: Probabilistic Noninterference for Multi-threaded Programs. In: Proc. of the IEEE Computer Security Foundations Workshop (CSFW 2000), pp. 200–215. IEEE Comp. Soc. Press, Los Alamitos (2000)CrossRefGoogle Scholar
  24. 24.
    Sangiorgi, D., Walker, D.: The π-calculus. Cambridge University Press, Cambridge (2001)Google Scholar
  25. 25.
    Widom, J., Gries, D., Schneider, F.B.: Trace-based Network Proof Systems: Expressiveness and Completeness. ACM Transactions on Programming Languages and Systems (TOPLAS) 14(3), 396–416 (1992)CrossRefGoogle Scholar
  26. 26.
    Zakinthinos, A., Lee, E.S.: A General Theory of Security Properties. In: Proc. of the IEEE Symposium on Security and Privacy, pp. 74–102. IEEE Comp. Soc. Press, Los Alamitos (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Annalisa Bossi
    • 1
  • Damiano Macedonio
    • 1
  • Carla Piazza
    • 1
  • Sabina Rossi
    • 1
  1. 1.Dipartimento di InformaticaUniversità Ca’ Foscari di Venezia 

Personalised recommendations