Abstract
The Ambient Calculus and the Safe Ambient Calculus have been recently successfully proposed as models for the Web. They are based on the notions of ambient movement and ambient opening. Different type disciplines have been devised for them in order to avoid unwanted behaviours of processes. In the present paper we propose a type discipline for safe mobile ambients which is essentially motivated by ensuring security properties. We associate security levels to ambients and we require that an ambient at security level s can only be traversed or opened by ambients at security level at least s. Since the movement and opening rights can be unrelated, we consider two partial orders between security levels. We also discuss some meaningful examples of use of our type discipline.
Partially supported by MURST Cofin’ 99 TOSCA Project.
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
Michele Bugliesi and Giuseppe Castagna. Secure safe ambients. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages, 2001. To appear.
Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon. Mobility types for mobile ambients. In Jiří Wiederman, Peter van Emde Boas, and Mogens Nielsen, editors, ICALP 1999, volume 1644 of Lecture Notes in Computer Science, pages 230–239. Springer-Verlag, 1999.
Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon. Ambient groups and mobility types. In Jan van Leeuwen et al., editor, Theoretical Computer Science: Exploring New Frontiers in Theoretical Informatics, volume 1872 of Lecture Notes in Computer Science, pages 333–347. Springer-Verlag, 2000.
Luca Cardelli and Andrew D. Gordon. Mobile ambients. In Maurice Nivat, editor, FoSSaCS 1998, volume 1378 of Lecture Notes in Computer Science, pages 140–155. Springer-Verlag, 1998.
Luca Cardelli and Andrew D. Gordon. Types for mobile ambients. In POPL’99, pages 79–92, New York, NY, USA, 1999. ACM Press.
Matthew Hennessy and James Riely. Resource access control in systems of mobile agents (extended abstract). In Proc. of 3rd International Workshop on High-Level Concurrent Languages (HLCL’98), 1998. Vol. 16(3) of Electronic Notes in Theoretical Computer Science. Full version to appear in Information and Computation.
Matthew Hennessy and James Riely. Information flow vs. resource access in the asynchronous π-calculus. In Ugo Montanari, José Rolim, and Emo Welzl, editors, ICALP 2000, volume 1853 of Lecture Notes in Computer Science, pages 415–427. Springer-Verlag, 2000.
Francesca Levi and Chiara Bodei. Security analysis for mobile ambients. In Proceedings of the Workshop on Issues in the Theory of Security, (co-located with ICALP 2000), pages 18–23, 2000.
Francesca Levi and Davide Sangiorgi. Controlling interference in ambients. In POPL’00, pages 352–364, New York, NY, USA, 2000. ACM Press.
Rocco De Nicola, Gianluigi Ferrari, Rosario Pugliese, and Betty Venneri. Types for access control. Theoretical Computer Science, 2000. Special issue on Coordination. To appear, available at http://rap.dsi.unifi.it/papers.htm.
Benjamin Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. In Logic in Computer Science, 1993. Full version in Mathematical Structures in Computer Science, Vol. 6, No. 5, pages 409–454, 1996.
Pascal Zimmer. Subtyping and typing algorithms for mobile ambients. In Jerzy Tiuryn, editor, FoSSaCS 2000, volume 1784 of Lecture Notes in Computer Science, pages 375–390. Springer-Verlag, 2000.
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
Dezani-Ciancaglini, M., Salvo, I. (2000). Security Types for Mobile Safe Ambients. In: Jifeng, H., Sato, M. (eds) Advances in Computing Science — ASIAN 2000. ASIAN 2000. Lecture Notes in Computer Science, vol 1961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44464-5_16
Download citation
DOI: https://doi.org/10.1007/3-540-44464-5_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41428-5
Online ISBN: 978-3-540-44464-0
eBook Packages: Springer Book Archive