skip to main content
article
Open Access

Mobile safe ambients

Published:01 January 2003Publication History
Skip Abstract Section

Abstract

Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences, which are similar to the interferences one finds in CCS and π-calculus; and grave interferences, which are more dangerous and may be regarded as programming errors. To control interferences, the MA movement primitives are modified; the resulting calculus is called Mobile Safe Ambients (SA).The modification also has computational significance. In the MA interaction rules, an ambient may enter, exit, or open another ambient. The second ambient undergoes the action; it has no control on when the action takes place. In SA this is rectified: any movement takes place only if both participants agree.Existing type systems for MA can be easily adapted to SA. The type systems for controlling mobility, however, appear to be more powerful in SA, in that (i) type systems for MA may give more precise information when transplanted onto SA , and (ii) new type systems may be defined. Two type systems are presented that remove all grave interferences.Other advantages of SA are: a useful algebraic theory; programs sometimes more robust (they require milder conditions for correctness) and/or simpler. All these points are illustrated in several examples.

References

  1. Amadio, R. M. and Cardelli, L. 1993. Subtyping recursive types. ACM Trans. Program. Lang. Syst. 15, 4, 575--631.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. Amtoft, T., Kfoury, A. J., and Pericas-Geertsen, S. M. 2001. What are Polymorphically-Typed Ambients? In Proceedings of ESOP '01. Lecture Notes in Computer Science, vol. 2028. Springer Verlag, Berlin, 206--220.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. Bugliesi, M. and Castagna, G. 2001. Secure Safe Ambients. In Proceedings of the 28th Annual Symposium on Principles of Programming Languages. ACM, New York.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. Cardelli, L. 1996. Type Systems, Handbook of Computer Science and Engineering. CRC Press.]]Google ScholarGoogle Scholar
  5. Cardelli, L., Ghelli, G., and Gordon, A. D. 1999. Mobility types for mobile ambients. In Proceedings of ICALP '99. Lecture Notes in Computer Science, vol. 1644. Springer Verlag, Berlin, 230--239.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. Cardelli, L. and Gordon, A. D. 1998a. Mobile ambients. In Proceedings of FoSSaCS '98, M. Nivat, Ed. Lecture Notes in Computer Science, vol. 1378. Springer Verlag, Berlin, 140--155.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. Cardelli, L. and Gordon, A. D. 1998b. Technical annex to Cardelli and Gordon {1998a}. Unpublished notes.]]Google ScholarGoogle Scholar
  8. Cardelli, L. and Gordon, A. D. 1999a. Equational properties of mobile ambients. In Proceedings of FoSSaCS '99, W. Thomas, Ed. Lecture Notes in Computer Science, vol. 1578. Springer Verlag, Berlin, 212--226.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. Cardelli, L. and Gordon, A. D. 1999b. Equational properties of mobile ambients. Tech. Rep. MSR-TR-99-11, Microsoft Research.]]Google ScholarGoogle Scholar
  10. Cardelli, L. and Gordon, A. D. 1999c. Types for mobile ambients. In Proceedings of the 26th Annual Symposium on Principles of Programming Languages. ACM, New York, 79--92.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. Degano, P., Levi, F., and Bodei, C. 2000. Safe Ambients: Control Flow Analysis and Security. In Proceedings of ASIAN '00. Lecture Notes in Computer Science, vol. 1961. Springer Verlag, Berlin, 199--214.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. Dezani-Ciancaglini, M. and Salvo, I. 2000. Security types for mobile safe ambients. In Proceedings of ASIAN '00. Lecture Notes in Computer Science, vol. 1961. Springer Verlag, Berlin, 215--236.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. Fournet, C., Gonthier, G., Lévy, J.-J., Maranget, L., and Rémy, D. 1996. A calculus of mobile processes. In Proceedings of CONCUR '96, U. Montanari and V. Sassone, Eds. Lecture Notes in Computer Science, vol. 1119. Springer Verlag, Berlin, 406--421.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. Gadducci, F. and Montanari, U. 2001. A concurrent graph semantics for mobile ambients. Electronic Notes in Computer Science, vol. 45. Elsevier.]]Google ScholarGoogle Scholar
  15. Guan, X., Yang, Y., and You, J. 2000. Making ambients more robust. In Proceedings of the International Conference on Software: Theory and Practice. 377--384.]]Google ScholarGoogle Scholar
  16. Guan, X., Yang, Y., and You, J. 2001. Typing evolving ambients. Information Processing Letters 80, 5, 265--270.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. Hennessy, M. and Riely, J. 1998. A typed language for distributed mobile processes. In Proceedings of the 25th Annual Symposium on Principles of Programming Languages. ACM, New York, 378--390.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. Kobayashi, N., Pierce, B., and Turner, D. 1996. Linearity and the pi-calculus. In Proceedings of the 23th Annual Symposium on Principles of Programming Languages. ACM, New York, 358--371.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. Merro, M. and Hennessy, M. 2002. Bisimulation congruences in Safe Ambients. In Proceedings of the 29th Annual Symposium on Principles of Programming Languages. ACM, New York.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. Milner, R. 1989. Communication and Concurrency. Prentice Hall.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. Milner, R., Parrow, J., and Walker, D. 1992. A calculus of mobile processes, (Parts I and II). Information and Computation 100, 1--77.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. Milner, R. and Sangiorgi, D. 1992. Barbed bisimulation. In Proceedings of ICALP '92, W. Kuich, Ed. Lecture Notes in Computer Science, vol. 623. Springer Verlag, Berlin, 685--695.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. Nielson, H. R., Nielson, F., Hansen, R. R., , and Jensen, J. G. 1999. Validating firewalls in mobile ambients. In Proceedings of CONCUR '99, J. Baeten and S. Mauw, Eds. Lecture Notes in Computer Science, vol. 1664. Springer Verlag, Berlin, 463--478.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. Pierce, B. and Sangiorgi, D. 1996. Typing and subtyping for mobile processes. J. Math. Struct. Comput. Sci. 6, 5, 409--454.]]Google ScholarGoogle ScholarCross RefCross Ref
  25. Reynolds, J. 1978. Syntactic control of interference. In Proceedings of the 5th Annual Symposium on Principles of Programming Languages. ACM, New York, 39--46.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. Sangiorgi, D. 1997. The name discipline of uniform receptiveness. In Proceedings of ICALP '97. Lecture Notes in Computer Science, vol. 1256. Springer Verlag, Berlin.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. Sangiorgi, D. and Valente, A. 2001. A distributed abstract machine for Safe Ambients. In Proceedings of ICALP '01. Lecture Notes in Computer Science, vol. 2076. Springer Verlag, Berlin.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. Sangiorgi, D. and Walker, D. 2001. The π-calculus: a Theory of Mobile Processes. Cambridge University Press.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. Sewell, P. 1998. Global/local subtyping and capability inference for a distributed π-calculus. In Proceedings of ICALP '98. Lecture Notes in Computer Science, vol. 1443. Springer Verlag, Berlin.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. Vitek, J. and Castagna, G. 1999. Seal: A framework for secure mobile computations. In Proceedings of the Conference on Internet Programming Languages. Lecture Notes in Computer Science, vol. 1686. Springer Verlag, Berlin.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. Zimmer, O. 2000. On the expressiveness of pure mobile ambients. In Proceedings of EXPRESS '00, L. Aceto and B. Victor, Eds. Electronic Notes in Computer Science, vol. 39. Elsevier.]]Google ScholarGoogle Scholar

Index Terms

  1. Mobile safe ambients

                  Recommendations

                  Comments

                  Login options

                  Check if you have access through your login credentials or your institution to get full access on this article.

                  Sign in

                  Full Access

                  • Published in

                    cover image ACM Transactions on Programming Languages and Systems
                    ACM Transactions on Programming Languages and Systems  Volume 25, Issue 1
                    January 2003
                    158 pages
                    ISSN:0164-0925
                    EISSN:1558-4593
                    DOI:10.1145/596980
                    Issue’s Table of Contents

                    Copyright © 2003 ACM

                    Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

                    Publisher

                    Association for Computing Machinery

                    New York, NY, United States

                    Publication History

                    • Published: 1 January 2003
                    Published in toplas Volume 25, Issue 1

                    Permissions

                    Request permissions about this article.

                    Request Permissions

                    Check for updates

                    Qualifiers

                    • article

                  PDF Format

                  View or Download as a PDF file.

                  PDF

                  eReader

                  View online with eReader.

                  eReader