Abstract
We use Abstract Interpretation to automatically prove safety properties of mobile ambients with name communications. We introduce a non-standard semantics in order to distinguish different recursive instances of agents. This allows us to specify explicitly both the link between agents and the ambient names they have declared, and the link between agents and the ambients they have activated.
Then we derive from this non-standard semantics an abstract semantics which focuses on interactions between agents. This abstract semantics describes non uniformly which agents can be launched in which ambients and which ambient names can be communicated to which agents. Such a description is required to prove security properties such as non-interference or confinement for instance.
This work was supported by the RTD project IST-1999-20527 ”DAEDALUS” of the European FP5 programme.
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
L. Cardelli, G. Ghelli, and A. D. Gordon. Ambient groups and mobility types. In Proc. TCS’00, LNCS, pages 333–347. Springer, 2000.
L. Cardelli and A. D. Gordon. Types for mobile ambients. In Proc. POPL’99, pages 79–92. ACM, 1999.
L. Cardelli and A. D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Proc. POPL’00, pages 365–377. ACM Press, 2000.
Luca Cardelli and A. D. Gordon. Mobile ambients. Theoretical Computer Science, 240(1):177–213, June 2000.
P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303–342. Prentice-Hall, Inc., Englewood Cliffs, 1981.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. POPL’77, pages 238–252, Los Angeles, California, U.S.A., 1977.
P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of logic and computation, 2(4):511–547, 1992.
P. Cousot and R. Cousot. Comparing the Galois connection and widening-narrowing approaches to abstract interpretation. In Proc. PLILP’92, LNCS, pages 269–295. Springer, 1992.
J. Feret. Confidentiality analysis of mobile systems. In Proc. SAS’00, LNCS, pages 135–154. Springer, 2000.
J. Feret. Occurrence counting analysis for the pi-calculus. Electronic Notes in Theoretical Computer Science, 39(2), 2001.
R. R. Hansen, J. G. Jensen, F. Nielson, and H. Riis Nielson. Abstract interpretation of mobile ambients. In Proc. SAS’99, LNCS, pages 134–148. Springer, 1999.
M. Hennessy and J. Riely. Resource access control in systems of mobile agents. In Proc. HLCL’98, ENTCS. Elsevier, 1998.
M. Hennessy and J. Riely. A typed language for distributed mobile processes. In Proc. POPL’98. ACM Press, 1998.
M. Karr. Affine relationships among variables of a program. Acta Informatica, pages 133–151, 1976.
F. Levi and D. Sangiorgi. Controlling interference in ambients. In Proc. POPL’00, pages 352–364. ACM Press, 2000.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. Information and Computation, pages 1–77, 1992.
F. Nielson, H. Riis Nielson, R. R. Hansen, and J. G. Jensen. Validating firewalls in mobile ambients. In Proc. CONCUR’99, LNCS, pages 463–477. Springer, 1999.
H. Riis Nielson and F. Nielson. Shape analysis for mobile ambients. In Proc. POPL’00, pages 142–154. ACM Press, 2000.
R. J. Parikh. On context-free languages. Journal of the ACM, 13:570–581, 1966.
A. Venet. Automatic determination of communication topologies in mobile systems. In Proc. SAS’98, LNCS, pages 152–167. Springer, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Feret, J. (2001). Abstract Interpretation-Based Static Analysis of Mobile Ambients. In: Cousot, P. (eds) Static Analysis. SAS 2001. Lecture Notes in Computer Science, vol 2126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47764-0_24
Download citation
DOI: https://doi.org/10.1007/3-540-47764-0_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42314-0
Online ISBN: 978-3-540-47764-8
eBook Packages: Springer Book Archive