Skip to main content
SpringerLink
Log in

Enforcing Security Policies via Types

  • Conference paper
Security in Pervasive Computing

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2802))

Abstract

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.

This work has been partially supported by EU within the FET – Global Computing initiative, project MIKADO IST-2001-32222, and by MIUR project NAPOLI. The funding bodies are not responsible for any use that might be made of the results presented here.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Gordon, A.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  2. Arnold, K., Freeman, E., Hupfer, S.: JavaSpaces Principles, Patterns and Practice. Addison-Wesley, Reading (1999)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  8. Cardelli, L., Ghelli, G., Gordon, A.D.: Types for the ambient calculus. Journal of Information and Computation (2002)

    Google Scholar 

  9. Cardelli, L., Gordon, A.D.: Types for mobile ambients. In: Proceedings of POPL 1999, pp. 79–92 (1999)

    Google Scholar 

  10. Cardelli, L., Gordon, A.D.: Mobile ambients. Theoretical Computer Science 240(1), 177–213 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  11. Carriero, N., Gelernter, D.: Linda in context. Communications of the ACM 32(4), 444–458 (1989)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  15. De Nicola, R., Ferrari, G., Pugliese, R.: Types as Specifications of Access Policies. In: Vitek, J., Jensen, C. (eds.) [35], pp. 117–146

    Google Scholar 

  16. De Nicola, R., Ferrari, G., Pugliese, R., Venneri, B.: Types for Access Control. Theoretical Computer Science 240(1), 215–254 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  17. Deugo, D.: Choosing a Mobile Agent Messaging Model. In: Proc. of ISADS 2001, pp. 278–286. IEEE, Los Alamitos (2001)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  19. Gelernter, D.: Generative Communication in Linda. ACM Transactions on Programming Languages and Systems 7(1), 80–112 (1985)

    Article  MATH  Google Scholar 

  20. Gong, L.: Inside Java 2 platform security: architecture, API design, and implementation. Addison-Wesley, Reading (1999)

    Google Scholar 

  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 http://rap.dsi.unifi.it/~pugliese/DOWNLOAD/muklaim-full.pdf

  22. Gorla, D., Pugliese, R.: Enforcing Security Policies via Types. Research report, Dipartimento di Sistemi e Informatica, Università di Firenze (2003), Available at http://rap.dsi.unifi.it/~pugliese/DOWNLOAD/spc-full.pdf

  23. Graw, G.M., Felten, E.: Securing Java. John Wiley and Son, Chichester (1999)

    Google Scholar 

  24. Hennessy, M., Riely, J.: Type-Safe Execution of Mobile Agents in Anonymous Networks. In: Vitek, J and Jensen, C [35], pp. 95–115

    Google Scholar 

  25. Hennessy, M., Riely, J.: Resource Access Control in Systems of Mobile Agents. Information and Computation 173, 82–120 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  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. Levi, F., Sangiorgi, D.: Controlling interference in ambients. In: Proceedings of POPL 2000, pp. 352–364. ACM Press, New York (2000)

    Google Scholar 

  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 Agents

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Rowstron, A.: WCL: A web co-ordination language. World Wide Web Journal 1(3), 167–179 (1998)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  33. Sun Microsystems. Javaspace specification (1999), available at http://java.sun.com/

  34. Vitek, J., Bryce, C., Oriol, M.: Coordinationg processes with secure spaces. Science of Computer Programming (2002)

    Google Scholar 

  35. Vitek, J., Jensen, C. (eds.): Secure Internet Programming. LNCS, vol. 1603. Springer, Heidelberg (1999)

    Google Scholar 

  36. Wyckoff, P., McLaughry, S., Lehman, T., Ford, D.: TSpaces. IBM Systems Journal 37(3), 454–474 (1998)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Sistemi e Informatica, Università di Firenze,  

    Daniele Gorla & Rosario Pugliese

Authors
  1. Daniele Gorla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rosario Pugliese
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DFKI, Stuhlsatzenhausweg 3, D-66123, Saarbrücken, Germany

    Dieter Hutter

  2. Institute of Computer Science and Social Studies, Department of Telematics, Albert-Ludwig University Freiburg, Germany

    Günter Müller

  3. German Research Center for Artificial Intelligence, DFKI GmbH,  

    Werner Stephan

  4. Federal Office for Information Security (BSI), Godesberger Allee 185-189, 53175, Bonn, Germany

    Markus Ullmann

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gorla, D., Pugliese, R. (2004). Enforcing Security Policies via Types. In: Hutter, D., Müller, G., Stephan, W., Ullmann, M. (eds) Security in Pervasive Computing. Lecture Notes in Computer Science, vol 2802. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39881-3_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-39881-3_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20887-7

  • Online ISBN: 978-3-540-39881-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation