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.
- Amadio, R. M. and Cardelli, L. 1993. Subtyping recursive types. ACM Trans. Program. Lang. Syst. 15, 4, 575--631.]] Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Cardelli, L. 1996. Type Systems, Handbook of Computer Science and Engineering. CRC Press.]]Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Cardelli, L. and Gordon, A. D. 1998b. Technical annex to Cardelli and Gordon {1998a}. Unpublished notes.]]Google Scholar
- 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 ScholarDigital Library
- Cardelli, L. and Gordon, A. D. 1999b. Equational properties of mobile ambients. Tech. Rep. MSR-TR-99-11, Microsoft Research.]]Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Gadducci, F. and Montanari, U. 2001. A concurrent graph semantics for mobile ambients. Electronic Notes in Computer Science, vol. 45. Elsevier.]]Google Scholar
- 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 Scholar
- Guan, X., Yang, Y., and You, J. 2001. Typing evolving ambients. Information Processing Letters 80, 5, 265--270.]] Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Milner, R. 1989. Communication and Concurrency. Prentice Hall.]] Google ScholarDigital Library
- Milner, R., Parrow, J., and Walker, D. 1992. A calculus of mobile processes, (Parts I and II). Information and Computation 100, 1--77.]] Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Pierce, B. and Sangiorgi, D. 1996. Typing and subtyping for mobile processes. J. Math. Struct. Comput. Sci. 6, 5, 409--454.]]Google ScholarCross Ref
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Sangiorgi, D. and Walker, D. 2001. The π-calculus: a Theory of Mobile Processes. Cambridge University Press.]] Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
Index Terms
Mobile safe ambients
Recommendations
Behavioural typing for safe ambients
We introduce a typed variant of Safe Ambients, named Secure Safe Ambients (SSA), whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both ...
Secure safe ambients
POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesSecure Safe Ambients (SSA) are a typed variant of Safe Ambients [9], whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both explicit and ...
Secure safe ambients
Secure Safe Ambients (SSA) are a typed variant of Safe Ambients [9], whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both explicit and ...
Comments