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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Gordon, A.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999)
Arnold, K., Freeman, E., Hupfer, S.: JavaSpaces Principles, Patterns and Practice. Addison-Wesley, Reading (1999)
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)
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)
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)
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)
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)
Cardelli, L., Ghelli, G., Gordon, A.D.: Types for the ambient calculus. Journal of Information and Computation (2002)
Cardelli, L., Gordon, A.D.: Types for mobile ambients. In: Proceedings of POPL 1999, pp. 79–92 (1999)
Cardelli, L., Gordon, A.D.: Mobile ambients. Theoretical Computer Science 240(1), 177–213 (2000)
Carriero, N., Gelernter, D.: Linda in context. Communications of the ACM 32(4), 444–458 (1989)
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)
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)
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)
De Nicola, R., Ferrari, G., Pugliese, R.: Types as Specifications of Access Policies. In: Vitek, J., Jensen, C. (eds.) [35], pp. 117–146
De Nicola, R., Ferrari, G., Pugliese, R., Venneri, B.: Types for Access Control. Theoretical Computer Science 240(1), 215–254 (2000)
Deugo, D.: Choosing a Mobile Agent Messaging Model. In: Proc. of ISADS 2001, pp. 278–286. IEEE, Los Alamitos (2001)
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)
Gelernter, D.: Generative Communication in Linda. ACM Transactions on Programming Languages and Systems 7(1), 80–112 (1985)
Gong, L.: Inside Java 2 platform security: architecture, API design, and implementation. Addison-Wesley, Reading (1999)
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
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
Graw, G.M., Felten, E.: Securing Java. John Wiley and Son, Chichester (1999)
Hennessy, M., Riely, J.: Type-Safe Execution of Mobile Agents in Anonymous Networks. In: Vitek, J and Jensen, C [35], pp. 95–115
Hennessy, M., Riely, J.: Resource Access Control in Systems of Mobile Agents. Information and Computation 173, 82–120 (2002)
Kirli, D.: Confined mobile functions. In: Proc. of the 14th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos (2001)
Levi, F., Sangiorgi, D.: Controlling interference in ambients. In: Proceedings of POPL 2000, pp. 352–364. ACM Press, New York (2000)
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
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)
Riely, J., Hennessy, M.: Trust and partial typing in open systems of mobile agents. In: Proceedings of POPL, pp. 93–104 (1999)
Rowstron, A.: WCL: A web co-ordination language. World Wide Web Journal 1(3), 167–179 (1998)
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)
Sun Microsystems. Javaspace specification (1999), available at http://java.sun.com/
Vitek, J., Bryce, C., Oriol, M.: Coordinationg processes with secure spaces. Science of Computer Programming (2002)
Vitek, J., Jensen, C. (eds.): Secure Internet Programming. LNCS, vol. 1603. Springer, Heidelberg (1999)
Wyckoff, P., McLaughry, S., Lehman, T., Ford, D.: TSpaces. IBM Systems Journal 37(3), 454–474 (1998)
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)
Yoshida, N., Hennessy, M.: Assigning types to processes. In: Proceedings of LICS 2000, pp. 334–348. IEEE Computer Society Press, Los Alamitos (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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