Abstract
The ambient calculus is a calculus of computation that allows active processes (mobile ambients) to move between sites. A firewall is said to be protective whenever it denies entry to attackers not possessing the required passwords. We devise a polynomial time algorithm for rejecting proposed firewalls that are not guaranteed to be protective. This is based on a control flow analysis for recording what processes may turn up inside what other processes; in particular, we develop a syntaxdirected system for specifying the acceptability of an analysis, we prove that all acceptable analyses are semantically sound, and we demonstrate that each process admits a least analysis.
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.
References
M. Abadi: Secrecy by typing in security protocols. In Proceedings of Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science, pages 611–638, Springer Verlag, 1997.
A. Aiken: Set constraints: Results, applications and future directions. In Proceedings of the Second Workshop on the Principles and Practices of Concurrent Programming, volume 874 of Lecture Notes in Computer Science, pages 171–179, Springer Verlag, 1994.
C. Bodei, P. Degano, F. Nielson, H. R. Nielson: Control Flow Analysis for the πcalculus. In Proceedings CONCUR’98, volume 1466 of Lecture Notes in Computer Science, pages 84–98, Springer Verlag, 1998.
C. Bodei, P. Degano, F. Nielson, H. R. Nielson: Static analysis of processes for no readup and no write-down. In Proceedings FoSSaCS’99, volume 1578 of Lecture Notes in Computer Science, pages 120–134, Springer Verlag, 1999.
L. Cardelli, A. D. Gordon: Mobile Ambients. In Proceedings FoSSaCS’98, volume 1378 of Lecture Notes in Computer Science, pages 140–155, Springer Verlag, 1998.
L. Cardelli, A. D. Gordon: Types for Mobile Ambients. In Proceedings POPL’99, pages 79–92, ACM Press, 1999.
R. R. Hansen, J. G. Jensen: Flow Logics for Mobile Ambients. M.Sc.-thesis, 1999.
T. Jensen, D. LeMétayer, T. Thorn: Security and Dynamic Class Loading in Java: a formalisation. Report IRISA, Rennes, 1997.
F. Nielson, H. R. Nielson, C. Hankin: Principles of Program Analysis, Springer Verlag, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nielson, F., Nielson, H.R., Hansen, R.R., Jensen, J.G. (1999). Validating Firewalls in Mobile Ambients. In: Baeten, J.C.M., Mauw, S. (eds) CONCUR’99 Concurrency Theory. CONCUR 1999. Lecture Notes in Computer Science, vol 1664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48320-9_32
Download citation
DOI: https://doi.org/10.1007/3-540-48320-9_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66425-3
Online ISBN: 978-3-540-48320-5
eBook Packages: Springer Book Archive