Abstract
We propose an extension of the asynchronous π-calculus in which a variety of security properties may be captured using types. These are an extension of the Input/Output types for the π-calculus in which I/O capabilities are assigned specific security levels.
We define a typing system which ensures that processes running at security level σ cannot access resources with a security level higher than σ. The notion of access control guaranteed by this system is formalized in terms of a Type Safety theorem.
We then show that, for a certain class of processes, our system prohibits implicit information flow from high-level to low-level processes. We prove that low-level behaviour can not be influenced by changes to high-level behaviour. This is formalized as a Non-interference Theorem with respect to may testing.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Martín Abadi. Secrecy by typing in security protocols. In Proceedings of TAGS’97, volume 1281 of Lecture Notes in Computer Science, pages 611–637. Springer Verlag, 1997.
D. E. Bell and L. J. LaPadula. Secure computer system: Unified exposition and multics interpretation. Technical report MTR-2997, MITRE Corporation, 1975.
C. Bodei, P. Degano, F. Nielson, and H. R. Nielson. Control flow analysis for the 7r-calculus. In Proc. GONGUR’98, number 1466 in Lecture Notes in Computer Science, pages 84–98. Springer-Verlag, 1998.
C. Bodei, P. Degano, F. Nielson, and H. R. Nielson. Static analysis of processes for no read-up and no write-down. In Proc. FOSSAGS’99, number 1578 in Lecture Notes in Computer Science, pages 120–134. Springer-Verlag, 1999.
G. Boudol. Asynchrony and the π-calculus. Technical Report 1702, INRIA-Sophia Antipolis, 1992.
Ilaria Castellani and Matthew Hennessy. Testing theories for asynchronous languages. In V Arvind and R Ramanujam, editors, 18th Conference on Foundations of Software Technology and Theoretical Computer Science (Chennai, India, December 17–19, 1998), LNCS 1530. Springer-Verlag, December 1998.
D. Denning. Certification of programs for secure information flow. Communications of the ACM, 20:504–513, 1977.
Riccardo Focardi, Anna Ghelli, and Roberto Gorrieri. Using non interference for the analysis of security protocols. In Proceedings of DIM ACS Workshop on Design and Formal Verification of Security Protocols, 1997.
Riccardo Focardi and Roberto Gorrieri. A classification of security properties for process algebras. Journal of Computer Security, 3(1), 1995.
Riccardo Focardi and Roberto Gorrieri. The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering, 23, 1997.
Riccardo Focardi and Roberto Gorrieri. Non interference: Past, present and future. In Proceedings of DARPA Workshop on Foundations for Secure Mobile Code, 1997.
C. Fournet, G. Gonthier, J.J. Levy, L. Marganget, and D. Remy. A calculus of mobile agents. In U. Montanari and V. Sassone, editors, CONCUR: Proceedings of the International Conference on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 406–421, Pisa, August 1996. Springer-Verlag.
R. Reitmas G. Andrews. An axiomatic approach to information flow in programs. ACM Transactions on Programming Languages and Systems, 2(1):56–76, 1980.
J. A. Goguen and J. Meseguer. Security policies and security models. In IEEE Symposium on Security and privacy, 1992.
Nevin Heintz and Jon G. Riecke. The SLam calculus: Programming with secrecy and integrity. In Conference Record of the ACM Symposium on Principles of Programming Languages, San Diego, January 1998.
Matthew Hennessy and James Riely. Information flow vs. resource access in the asynchronous pi-calculus. Technical report 2000: 03, University of Sussex, 2000. Available from http://www.cogs.susx.ac.uk/.
Kohei Honda and Mario Tokoro. On asynchronous communication semantics. In P. Wegner M. Tokoro, O. Nierstrasz, editor, Proceedings of the ECOOP’ 91 Workshop on Object-Based Concurrent Computing, volume 612 of LNCS 612. Springer-Verlag, 1992.
Kohei Honda, Vasco Vasconcelos, and Nobuko Yoshida Honda. Secure information flow as typed process behaviour. In Proceedings of European Symposium on Programming (ESOP) 2000. Springer-Verlag, 2000.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
R. Milner, J. Parrow, and D. Walker. Mobile logics for mobile processes. Theoretical Computer Science, 114:149–171, 1993.
R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 24:83–113, 1984.
Benjamin Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409–454, 1996. Extended abstract in LICS’ 93.
Benjamin C. Pierce and David N. Turner. Pict: A programming language based on the pi-calculus. Technical Report CSCI 476, Computer Science Department, Indiana University, 1997. To appear in Proof, Language and Interaction: Essays in Honour of Robin Milner, Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, MIT Press.
James Riely and Matthew Hennessy. Resource access control in systems of mobile agents (extended abstract). In Proceedings of 3rd International Workshop on High-Level Concurrent Languages, Nice, France, September 1998. Full version available as Computer Science Technical Report 2/98, University of Sussex, 1997. Available from http://www.cogs.susx.ac.uk/.
A.W. Roscoe, J.C.P. Woodcock, and L. Wulf. Non-interference through determinism. In European Symposium on Research in Computer Security, volume 875 of LNCS, 1994.
P.Y.A. Ryan and S.A. Schneider. Process algebra and non-interference. In CSFW 12. IEEE, 1997.
Geoffrey Smith and Dennis Volpano. Secure information flow in a multi-threaded imperative language. In Conference Record of the ACM Symposium on Principles of Programming Languages, San Diego, January 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hennessy, M., Riely, J. (2000). Information Flow vs. Resource Access in the Asynchronous Pi-Calculus (Extended Abstract). In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds) Automata, Languages and Programming. ICALP 2000. Lecture Notes in Computer Science, vol 1853. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45022-X_35
Download citation
DOI: https://doi.org/10.1007/3-540-45022-X_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67715-4
Online ISBN: 978-3-540-45022-1
eBook Packages: Springer Book Archive