Enforcing Security Policies via Types

  • Daniele Gorla
  • Rosario Pugliese
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2802)


Security is a key issue for distributed systems/applications with code mobility, like, e.g., e-commerce and on-line bank transactions. In a scenario with code mobility, traditional solutions based on cryptography cannot deal with all security issues and additional mechanisms are necessary. In this paper, we present a flexible and expressive type system for security for a calculus of distributed and mobile processes. The type system has been designed to supply real systems security features, like the assignment of different privileges to users over different data/resources. Type soundness is guaranteed by using a combination of static and dynamic checks, thus enforcing specific security policies on the use of resources. The usefulness of our approach is shown by modeling the simplified behaviour of a bank account management system.


Type System Mobile Agent Security Policy Operational Semantic Mobile Process 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Gordon, A.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Arnold, K., Freeman, E., Hupfer, S.: JavaSpaces Principles, Patterns and Practice. Addison-Wesley, Reading (1999)Google Scholar
  3. 3.
    Bugliesi, M., Castagna, G., Crafa, S.: Boxed ambients. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 38–63. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Bugliesi, M., Castagna, G., Crafa, S.: Reasoning about security in mobile ambients. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 102–120. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Busi, N., Gorrieri, R., Lucchi, R., Zavattaro, G.: Secspaces: a data-driven coordination model for environments open to untrusted agents. To appear in FOCLASA 2002, ENTCS (2002)Google Scholar
  6. 6.
    Cardelli, L., Ghelli, G., Gordon, A.D.: Mobility types for mobile ambients. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 230–239. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Cardelli, L., Ghelli, G., Gordon, A.D.: Ambient groups and mobility types. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 333–347. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  8. 8.
    Cardelli, L., Ghelli, G., Gordon, A.D.: Types for the ambient calculus. Journal of Information and Computation (2002)Google Scholar
  9. 9.
    Cardelli, L., Gordon, A.D.: Types for mobile ambients. In: Proceedings of POPL 1999, pp. 79–92 (1999)Google Scholar
  10. 10.
    Cardelli, L., Gordon, A.D.: Mobile ambients. Theoretical Computer Science 240(1), 177–213 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Carriero, N., Gelernter, D.: Linda in context. Communications of the ACM 32(4), 444–458 (1989)CrossRefGoogle Scholar
  12. 12.
    Castagna, G., Ghelli, G., Nardelli, F.Z.: Typing mobility in the seal calculus. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 82–101. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. 13.
    Ciancarini, P., Tolksdorf, R., Vitali, F., Rossi, D., Knoche, A.: Coordinating multiagent applications on the WWW: A reference architecture. IEEE Transactions on Software Engineering 24(5), 362–366 (1998)CrossRefGoogle Scholar
  14. 14.
    De Nicola, R., Ferrari, G., Pugliese, R.: KLAIM: a Kernel Language for Agents Interaction and Mobility. IEEE Transactions on Software Engineering 24(5), 315–330 (1998)CrossRefGoogle Scholar
  15. 15.
    De Nicola, R., Ferrari, G., Pugliese, R.: Types as Specifications of Access Policies. In: Vitek, J., Jensen, C. (eds.) [35], pp. 117–146Google Scholar
  16. 16.
    De Nicola, R., Ferrari, G., Pugliese, R., Venneri, B.: Types for Access Control. Theoretical Computer Science 240(1), 215–254 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Deugo, D.: Choosing a Mobile Agent Messaging Model. In: Proc. of ISADS 2001, pp. 278–286. IEEE, Los Alamitos (2001)Google Scholar
  18. 18.
    Dezani-Ciancaglini, M., Salvo, I.: Security types for mobile safe ambients. In: He, J., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 215–236. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  19. 19.
    Gelernter, D.: Generative Communication in Linda. ACM Transactions on Programming Languages and Systems 7(1), 80–112 (1985)zbMATHCrossRefGoogle Scholar
  20. 20.
    Gong, L.: Inside Java 2 platform security: architecture, API design, and implementation. Addison-Wesley, Reading (1999)Google Scholar
  21. 21.
    Gorla, D., Pugliese, R.: Resource access and mobility control with dynamic privileges acquisition. Research report, Dipartimento di Sistemi e Informatica, Università di Firenze (2002), Available at
  22. 22.
    Gorla, D., Pugliese, R.: Enforcing Security Policies via Types. Research report, Dipartimento di Sistemi e Informatica, Università di Firenze (2003), Available at
  23. 23.
    Graw, G.M., Felten, E.: Securing Java. John Wiley and Son, Chichester (1999)Google Scholar
  24. 24.
    Hennessy, M., Riely, J.: Type-Safe Execution of Mobile Agents in Anonymous Networks. In: Vitek, J and Jensen, C [35], pp. 95–115Google Scholar
  25. 25.
    Hennessy, M., Riely, J.: Resource Access Control in Systems of Mobile Agents. Information and Computation 173, 82–120 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    Kirli, D.: Confined mobile functions. In: Proc. of the 14th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos (2001)Google Scholar
  27. 27.
    Levi, F., Sangiorgi, D.: Controlling interference in ambients. In: Proceedings of POPL 2000, pp. 352–364. ACM Press, New York (2000)Google Scholar
  28. 28.
    Omicini, A., Zambonelli, F.: Coordination for internet application development. Autonomous Agents and Multi-agent Systems 2(3), 251–269 (1999); Special Issue on Coordination Mechanisms and Patterns for Web AgentsCrossRefGoogle Scholar
  29. 29.
    Picco, G., Murphy, A., Roman, G.-C.: LIME: Linda Meets Mobility. In: Garlan, D. (ed.) Proc. of the 21st Int. Conference on Software Engineering (ICSE 1999), pp. 368–377. ACM Press, New York (1999)CrossRefGoogle Scholar
  30. 30.
    Riely, J., Hennessy, M.: Trust and partial typing in open systems of mobile agents. In: Proceedings of POPL, pp. 93–104 (1999)Google Scholar
  31. 31.
    Rowstron, A.: WCL: A web co-ordination language. World Wide Web Journal 1(3), 167–179 (1998)CrossRefGoogle Scholar
  32. 32.
    Schneider, F.B., Morrisett, G., Harper, R.: A language-based approach to security. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 86–101. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  33. 33.
    Sun Microsystems. Javaspace specification (1999), available at
  34. 34.
    Vitek, J., Bryce, C., Oriol, M.: Coordinationg processes with secure spaces. Science of Computer Programming (2002)Google Scholar
  35. 35.
    Vitek, J., Jensen, C. (eds.): Secure Internet Programming. LNCS, vol. 1603. Springer, Heidelberg (1999)Google Scholar
  36. 36.
    Wyckoff, P., McLaughry, S., Lehman, T., Ford, D.: TSpaces. IBM Systems Journal 37(3), 454–474 (1998)CrossRefGoogle Scholar
  37. 37.
    Yoshida, N., Hennessy, M.: Subtyping and locality in distributed higher order processes. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 557–572. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  38. 38.
    Yoshida, N., Hennessy, M.: Assigning types to processes. In: Proceedings of LICS 2000, pp. 334–348. IEEE Computer Society Press, Los Alamitos (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Daniele Gorla
    • 1
  • Rosario Pugliese
    • 1
  1. 1.Dipartimento di Sistemi e InformaticaUniversità di Firenze 

Personalised recommendations