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.
This work has been partially supported by the MURST project “Modelli formali per la sicurezza” and the EU Contract IST-2001-32617 “Models and Types for Security in Mobile Distributed Systems” (MyThS).
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
Abadi, M., Lamport, L.: Conjoining Specifications. ACM Transactions on Programming Languages and Systems (TOPLAS) 17(3), 507–535 (1995)
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)
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)
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)
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
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)
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)
McCullough, D.: A Hookup Theorem for Multilevel Security. IEEE Transactions on Software Engineering 16(6), 563–568 (1990)
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)
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)
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)
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)
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)
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)
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)
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)
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)
McLean, J.: A General Theory of Composition for a Class of “Possibilistic” Security Properties. IEEE Transactions on Software Engineering 22(1), 53–67 (1996)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
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)
Ryan, P., Schneider, S.: Process Algebra and Non-Interference. Journal of Computer Security 9(1/2), 75–103 (2001)
Sabelfeld, A., Myers, A.C.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communication 21(1), 5–19 (2003)
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)
Sangiorgi, D., Walker, D.: The π-calculus. Cambridge University Press, Cambridge (2001)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bossi, A., Macedonio, D., Piazza, C., Rossi, S. (2003). Information Flow Security and Recursive Systems. In: Blundo, C., Laneve, C. (eds) Theoretical Computer Science. ICTCS 2003. Lecture Notes in Computer Science, vol 2841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45208-9_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-45208-9_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20216-5
Online ISBN: 978-3-540-45208-9
eBook Packages: Springer Book Archive