Advertisement

Seal: A Framework for Secure Mobile Computations

  • Jan Vitek
  • Giuseppe Castagna
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1686)

Abstract

The Seal calculus is a distributed process calculus with localities and mobility of computational entities called seals. Seal is also a framework for writing secure distributed applications over large scale open networks such as the Internet. This paper motivates our design choices, presents the syntax and reduction semantics of the calculus, and demonstrates its expressiveness by examples focused on security and management distributed systems.

Keywords

Mobile Agent Security Property Local Channel Mobile Computation Tuple Space 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The Spi calculus. In Proceedings of the Fourth ACM Conference on Computer and Communications Security, Zürich, April 1997. ACM Press, 1997. Long version as Technical Report 414, University of Cambridge.Google Scholar
  2. 2.
    ACM. Proceedings of the 23rd Annual Symposium on Principles of Programming Languages (POPL) (St. Petersburg Beach, Florida), Jan. 1996.Google Scholar
  3. 3.
    G. Agha. Actors — A model of concurrent computation in distributed systems. The MIT Press, 1986.Google Scholar
  4. 4.
    R. M. Amadio. On the reduction of CHOCS bisimulation to π-calculus bisimulation. In Best [8], pages 112–126. Extended version as Rapport de Recherche, INRIA-Lorraine, 1993.Google Scholar
  5. 5.
    R. M. Amadio. An asynchronous model of locality, failure, and process mobility. In Proceedings of COORDINATION’ 97. Springer-Verlag, 1997. Full version as Rapport Interne, LIM Marseille, and Rapport de Recherche RR-3109, INRIA Sophia-Antipolis, 1997.Google Scholar
  6. 6.
    F. M. auf der Heide and B. Monien, editors. 23rd Colloquium on Automata, Languages and Programming (ICALP) (Paderborn, Germany), volume 1099 of Lecture Notes in Computer Science. Springer-Verlag, 1996.Google Scholar
  7. 7.
    G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96:217–248, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    E. Best, editor. CONCUR’93, 4 th International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science. Springer-Verlag, 1993.Google Scholar
  9. 9.
    C. Bodei, P. Degano, and C. Priami. Mobile processes with a distributed environment. B. Monien, editors. 23rd Colloquium on Automata, Languages and Programming (ICALP) (Paderborn, Germany), volume 1099 of Lecture Notes in Computer Science In auf der Heide and Monien [6], pages 490–501. Full version as Università di Pisa Technical Report Handling Locally Names of Mobile Agents, 1996.Google Scholar
  10. 10.
    G. Boudol. Asynchrony and the π-calculus (Note). Rapport de Recherche 1702, INRIA Sofia-Antipolis, May 1992.Google Scholar
  11. 11.
    L. Cardelli. Abstractions for mobile computation. In J. Vitek and C. Jensen, editors, Secure Internet Programming: Security Issues for Distributed and Mobile Objects. Springer Verlag, 1999.Google Scholar
  12. 12.
    L. Cardelli and A. D. Gordon. Mobile Ambients. In M. Nivat, editor, Foundations of Software Science and Computational Structures, number 1378 in LNCE, pages 140–155. Springer-Verlag, 1998.Google Scholar
  13. 13.
    G. Castagna and J. Vitek. Commitment and confinement for the seal calculus. Technical report, Laboratoire d’Informatique de l’École Normale Supérieure, 1999.Google Scholar
  14. 14.
    R. De Nicola, G. Ferrari, and R. Pugliese. Coordinating mobile agents via black-boards and access rights. In Proceedings of COORDINATION’97. Springer-Verlag, 1997.Google Scholar
  15. 15.
    R. De Nicola, G. Ferrari, and R. Pugliese. Locality based Linda: programming with explicit localities. In Proceedings of FASE-TAPSOFT’97. Springer-Verlag, 1997.Google Scholar
  16. 16.
    P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors. 24rd Colloquium on Automata, Languages and Programming (ICALP) (Bologna, Italy), volume 1256 of Lecture Notes in Computer Science. Springer-Verlag, 1997.Google Scholar
  17. 17.
    B. Ford, B. Hibler, J. Lepreau, P. Tullmann, G. Back, and S. Clawson. Microkernels Meet Recursive Virtual Machines. In Proceedings Symposium on Operating Systems Design and Implementation(OSDI’96). ACM Press, Oct. 1996.Google Scholar
  18. 18.
    C. Fournet and G. Gonthier. The reflexive chemical abstract machine and the join-calculus. In POPL’96 [2], pages 372–385.Google Scholar
  19. 19.
    C. Fournet, G. Gonthier, J.-J. Lévy, L. Maranget, and D. Rémy. A calculus of mobile agents. In CONCUR96, pages 406–421, 1996.Google Scholar
  20. 20.
    D. Gelernter. Generative communication in Linda. ACM Trans. Prog. Lang. Syst., 7(1):80–112, Jan. 1985.zbMATHCrossRefGoogle Scholar
  21. 21.
    M. Hennessy and J. Riely. Type-safe execution of mobile agents in anonymous networks. In Proceedings of the Workshop on Internet Programming Languages, (WIPL). Chicago, Ill., 1998.Google Scholar
  22. 22.
    K. G. Larsen, S. Skyum, and G. Winskel, editors. 25rd Colloquium on Automata, Languages and Programming (ICALP) (Aalborg, Denmark), volume 1443 of Lecture Notes in Computer Science. Springer-Verlag, 1998.Google Scholar
  23. 23.
    R. Milner. The polyadic π-calculus: a tutorial. Technical Report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, UK, Oct. 1991. Also in Logic and Algebra of Specification, ed. F. L. Bauer, W. Brauer and H. Schwichtenberg, Springer-Verlag, 1993.Google Scholar
  24. 24.
    R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Parts I and II. Journal of Information and Computation, 100:1–77, Sept. 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    J. Noble, J. Vitek, and J. Potter. Flexible alias protection. In ECOOP’98 — Object-Oriented Programming, 12th European Conference Proceedings. Brussels, Belgium, Springer-Verlag, July 1998.Google Scholar
  26. 26.
    P. Pardyak, S. Savage, and B. N. Bershad. Language and runtime support for dynamic interposition of system code. Nov. 1995.Google Scholar
  27. 27.
    Proceedings of the Sixteenth Annual Symposium on Principles of Programming Languages (POPL) (Austin, TX). ACM Press, Austin Texas, January 1989.Google Scholar
  28. 28.
    J. Riely and M. Hennessy. Distributed processes and location failures. In R. Gorrieri, and A. Marchetti-Spaccamela, editors. 24rd Colloquium on Automata, Languages and Programming (ICALP) (Bologna, Italy), volume 1256 of Lecture Notes in Computer Science Degano et al. [16], pages 471–481. Full version as Report 2/97, University of Sussex, Brighton.Google Scholar
  29. 29.
    H. Rodrigues and R. Jones. Cyclic distributed garbage collection with group merger. In ECOOP’98 — Object-Oriented Programming, 12th European Conference Proceedings. Brussels, Belgium, Springer-Verlag, July 1998.Google Scholar
  30. 30.
    D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, Department of Computer Science, University of Edinburgh, UK, 1993.Google Scholar
  31. 31.
    F. Schneider. What Good are Models and What Models are Good? In S. Mullender, editor, Distributed Systems (2nd Ed.). ACM Frontier Press, 1993.Google Scholar
  32. 32.
    P. Sewell. Global/local subtyping and capability inference for a distributed π-calculus. In S. Skyum, and G. Winskel, editors. 25rd Colloquium on Automata, Languages and Programming (ICALP) (Aalborg, Denmark), volume 1443 of Lecture Notes in Computer Science. Springer-Verlag, 1998 Larsen et al. [22].CrossRefGoogle Scholar
  33. 33.
    P. Sewell and J. Vitek. Secure composition of insecure components. In Computer Security Foundations Workshop (CSFW-12). Mordano, Italy, June 1999.Google Scholar
  34. 34.
    P. Sewell, P. Wojciechowski, and B. Pierce. Location independence for mobile agents. In Proceedings of the 1998 Workshop on Internet Programming Languages, Chicago, Ill., May 1998.Google Scholar
  35. 35.
    B. Thomsen. A calculus of Higher Order Communicating Systems. In POPL’89 [27], pages 143–154.Google Scholar
  36. 36.
    B. Thomsen. Plain CHOCS. A second generation calculus for higher order processes. Acta Informatica, 30(1):1–59, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  37. 37.
    J. Vitek, C. Bryce, and W. Binder. Designing JavaSeal: or How to make Java safe for agents. In D. Tsichritzis, editor, Electronic Commerce Objects. University of Geneva, 1998.Google Scholar
  38. 38.
    J. Waldo, G. Wyant, A. Wollrath, and S. Kendall. A note on distributed computing. In J. Vitek and C. Tschudin, editors, Mobile Object Systems: Towards the programmable Internet. Springer-Verlag, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Jan Vitek
    • 1
  • Giuseppe Castagna
    • 2
  1. 1.Object Systems GroupCUI, Universit’e de GenèveSuisseFrance
  2. 2.Laboratoire d’Informatique de l’Ecole Normale Sup’erieureC.N.R.SParisFrance

Personalised recommendations