Access control for mobile agents: The calculus of boxed ambients

Abstract

Boxed Ambients are a variant of Mobile Ambients that result from dropping the open capability and introducing new primitives for ambient communication. The new model of communication is faithful to the principles of distribution and location-awareness of Mobile Ambients, and complements the constructs in and out for mobility with finer-grained mechanisms for ambient interaction. We introduce the new calculus, study the impact of the new mechanisms for communication of typing and mobility, and show that they yield an effective framework for resource protection and access control in distributed systems.

References

1. Amadio, R. and Prasad, S. 1994. Localities and failures. In FST&TCS. Lecture Notes in Computer Science, vol. 880. Springer-Verlag, Berlin, Germany, 206--216.]]
2. Bell, D. and Padula, L. L. 1976. Secure computer system: Unified exposition and multics interpretation,. Tech. rep. MTR-2997, MITRE Corporation, Bedford, MA.]]
3. Boudol, G. 1992. Asynchrony and the π-calculus. Res. Rep. 1702. INRIA. Available online at http://www.inria.fr/rrrt/rr-1702.html. Also available from http://www-sop.inria.fr/mimosa/personnel/Gerard.Boudol.html.]]
4. Bryce, C. and Vitek, J. 2001. The JavaSeal mobile agent kernel. Auton. Agents Multi-Agent Syst. 4, 4, 359--384.]]
5. Bugliesi, M. and Castagna, G. 2001. Secure safe ambients. In Proceedings of POPL'01. ACM Press, New York, NY, 222--235.]]
6. Bugliesi, M., Castagna, G., and Crafa, S. 2001a. Boxed ambients. In TACS'01. Lecture Notes in Computer Science, vol. 2215. Springer-Verlag, Berlin, Germany, 38--63.]]
7. Bugliesi, M., Castagna, G., and Crafa, S. 2001b. Reasoning about security in Mobile Ambients. In CONCUR'01. Lecture Notes in Computer Science, vol. 2154. Springer-Verlag, Berlin, Germany, 102--120.]]
8. Bugliesi, M., Crafa, S., Merro, M., and Sassone, V. 2002. Communication Interference in Mobile Boxed Ambients. In FSTTCS'02: Int. Conference on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 2556. Springer-Verlag, Berlin, Germany, 71--84.]]
9. Bugliesi, M., Crafa, S., Prelic, A., and Sassone, V. 2003. Secrecy in untrusted networks. In ICALP'03, International Colloquium on Automata Languages and Programming. Lecture Notes in Computer Science, vol. 2719. Springer-Verlag, Berlin, Germany, 969--983.]]
10. Cardelli, L. 1999. Abstractions for Mobile Computation. Lecture Notes in Computer Science, vol. 1603. Springer-Verlag, Berlin, Germany, 51--94.]]
11. Cardelli, L., Ghelli, G., and Gordon, A. 1999. Mobility types for Mobile Ambients. In Proceedings of ICALP '99. Lecture Notes in Computer Science, vol. 1644. Springer-Verlag, Berlin, Germany, 230--239.]]
12. Cardelli, L., Ghelli, G., and Gordon, A. D. 2000. Ambient groups and mobility types. In International Conference IFIP TCS. Lecture Notes in Computer Science, vol. 1872. Springer-Verlag, Berlin, Germany, 333--347.]]
13. Cardelli, L. and Gordon, A. 1998. Mobile Ambients. In Proceedings of F0SSaCS'98. Lecture Notes in Computer Science, vol. 1378. Springer-Verlag, Berlin, Germany, 140--155.]]
14. Cardelli, L. and Gordon, A. 1999a. Equational properties for Mobile Ambients. In Proceedings FoSSaCS '99. Lecture Notes in Computer Science, vol. 1578. Springer-Verlag, Berlin, Germany, 212--226.]]
15. Cardelli, L. and Gordon, A. 1999b. Types for Mobile Ambients. In Proceedings of POPL '99. ACM Press, New York, NY, 79--92.]]
16. Castagna, G., Ghelli, G., and Zappa Nardelli, F. 2001. Typing mobility in the Seal Calculus. In CONCUR'01. Lecture Notes in Computer Science, vol. 2154. Springer-Verlag, Berlin, Germany, 82--101.]]
17. Crafa, S., Bugliesi, M., and Castagna, G. 2002. Information flow security for Boxed Ambients. In F-WAN: International Workshop on Foundations of Wide Area Networks. Electron. Note Comp. Sci. 66, 3.]]
18. De Nicola, R., Ferrari, G., and Pugliese, R. 1998. KLAIM: A Kernel Language for Agents Interaction and Mobility. IEEE Trans. Softw. Eng. 24, 5, 315--330.]]
19. De Nicola, R., Ferrari, G., and Pugliese, R. 2000a. Programming access control: The KLAIM experience. In Proceedings of CONCUR'00. Lecture Notes in Computer Science, vol. 1877. Springer-Verlag, Berlin, Germany, 48--65.]]
20. De Nicola, R., Ferrari, G., Pugliese, R., and Venneri, B. 2000b. Types for access control. Theor. Comput. Sci. 240, 1, 215--254.]]
21. 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, Germany, 199--214.]]
22. Department of Defense. 1985. DoD trusted computer system evaluation criteria (the orange book). DOD 5200.28-STD. Department of Defense, Washington, DC.]]
23. Dezani-Ciancaglini, M. and Salvo, I. 2000. Security types for Safe Mobile Ambients. In Proceedings of ASIAN '00. Lecture Notes in Computer Science, vol. 1961. Springer-Verlag, Berlin, Germany, 215--236.]]
24. Focardi, R. and Gorrieri, R. 1997. Non-interference: Past, present and future. In Proceedings of DARPA Workshop on Foundations for Secure Mobile Code. 26--28.]]
25. Fournet, C., Gonthier, G., Lévy, J.-J., Maranget, L., and Rémy, D. 1996. A calculus of Mobile Agents. In 7th International Conference on Concurrency Theory (CONCUR '96). Lecture Notes in Computer Science, vol. 1119. Springer-Verlag, Berlin, Germany, 406--421.]]
26. Fournet, C., Levy, J.-J., and A, S. 2000. An asynchronous, distributed implementation of Mobile Ambients. In International Conference IFIP TCS. Lecture Notes in Computer Science, vol. 1872. Springer-Verlag, Berlin, Germany.]]
27. Goguen, J. and Meseguer, J. 1982. Security policy and security models. In Proceedings of Symposium on Security and Privacy. IEEE Computer Society, 11--20.]]
28. Gollmann, D. 1999. Computer Security. John Wiley & Sons Ltd., Chichester, U.K.]]
29. Hennessy, M. and Riely, J. 2002a. Information flow vs. resource access in the asynchronous π-calculus. ACM Trans. Program. Lang. Syst. 24, 5, 566--591.]]
30. Hennessy, M. and Riely, J. 2002b. Resource access control in systems of Mobile Agents. Inform. Comput. 173, 82--120.]]
31. Levi, F. and Sangiorgi, D. 2000. Controlling interference in ambients. In Proceedings of POPL '00. ACM Press, New York, NY, 352--364.]]
32. Merro, M. and Hennessy, M. 2002. Bisimulation conguences in Safe Ambients. In Proceedings of POPL'02. ACM Press, New York, NY, 71--80.]]
33. Merro, M. and Sassone, V. 2002. Typing and subtyping mobility in Boxed Ambients. In Proceedings of Concur'02. Lecture Notes in Computer Science, vol. 2421. Springer-Verlag, Berlin, Germany, 304--320.]]
34. Nestmann, U. 2000. What is a 'good' encoding of guarded choice? Inform. Comput. 156, 287--319.]]
35. Nielson, F., Nielson, H. R., Hansen, R. R., and Jensen, J. G. 1999. Validating firewalls in Mobile Ambients. In Proc. CONCUR '99. Lecture Notes in Computer Science, vol. 1664. Springer-Verlag, Berlin, Germany, 463--477.]]
36. Nielson, H. R. and Nielson, F. 2000. Shape analysis for Mobile Ambients. In Proceedings of POPL '00. ACM Press, New York, NY, 142--154.]]
37. Riely, J. and Hennessy, M. 1998. A typed language for distributed mobile processes. In Proceedings of POPL'98. ACM Press, New York, NY, 378--390.]]
38. Riely, J. and Hennessy, M. 1999. Trust and partial typing in open systems of Mobile Agents. In Proceedings of POPL '99. ACM Press, New York, NY, 93--104.]]
39. Sangiorgi, D. and A., V. 2001. A distributed abstract mathine for Safe Ambients. In Proceedings of ICALP'01. Lecture Notes in Computer Science, vol. 2076. Springer-Verlag, Berlin, Germany, 408--420.]]
40. Sewell, P. and Vitek, J. 2000. Secure composition of untrusted code: Wrappers and causality types. In Proceedings of the 13th IEEE Computer Security Foundations Workshop. Published in J. Comput. Sec. 11, 2, 135--187.]]
41. Vitek, J. and Castagna, G. 1999. Seal: A framework for secure mobile computations. In Internet Programming Languages. Lecture Notes in Computer Science, vol. 1686. Springer-Verlag, Berlin, Germany, 47--77.]]
42. Zimmer, P. 2000. Subtyping and typing algorithms for Mobile Ambients. In Proceedins of FoSSaCS '99. Lecture Notes in Computer Science, vol. 1784. Springer-Verlag, Berlin, Germany, 375--390.]]

Index Terms

• Computing methodologies

  • Distributed computing methodologies

    • Distributed programming languages

• Security and privacy

• Social and professional topics

  • Computing / technology policy

    • Computer crime

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language types

        • Distributed programming languages

• Theory of computation

  • Logic

    • Programming logic

  • Semantics and reasoning

    • Program constructs

      • Type structures

    • Program reasoning