×

zbMATH — the first resource for mathematics

Types for access control. (English) Zbl 0954.68025
Summary: KLAIM is an experimental programming language that supports a programming paradigm where both processes and data can be moved across different computing environments. This paper presents the mathematical foundations of the KLAIM type system; this system permits checking access rights violations of mobile agents. Types are used to describe the intentions (read, write, execute, \(\ldots)\) of processes relative to the different localities with which they are willing to interact, or to which they want to migrate. Type checking then determines whether processes comply with the declared intentions, and whether they have been assigned the necessary rights to perform the intended operations at the specified localities. The KLAIM type system encompasses both subtyping and recursively defined types. The former occurs naturally when considering hierarchies of access rights, while the latter is needed to model migration of recursive processes.

MSC:
68N15 Theory of programming languages
Software:
KLAIM; Linda
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M., Secrecy by typing in cryptographic protocols, (), 611-638
[2] Abadi, M.; Gordon, A.D., A calculus for cryptographic protocols: the spi calculus, Inform. and comput., 148, 1, 1-70, (1999) · Zbl 0924.68073
[3] M. Abadi, R. Stata, A type system for Java Bytecode subroutines, Proc. ACM Symp. on Principles of Programming Languages, ACM Press, New York, 1998, pp. 149-160. ACM Trans. Programm. Languages Systems, to appear.
[4] Amadio, R., An asynchronous model of locality, failure and process mobility, (), 374-391
[5] Amadio, R.; Cardelli, L., Subtyping recursive types, ACM trans. programm. languages systems, 15, 4, 575-631, (1993)
[6] Amadio, R.; Prasad, S., Localities and failures, (), 205-216 · Zbl 1044.68682
[7] Arnold, A.; Gosling, J., The Java programming language, (1996), Addison-Wesley Reading, MA · Zbl 0876.68015
[8] L. Bettini, R. De Nicola, G. Ferrari, R. Pugliese, Interactive mobile agents in X-K\scLAIM, Proc., IEEE 7th Internat. Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, IEEE Computer Society Press, Silverspring, MD, 1998.
[9] Bodei, C.; Degano, P.; Nielson, F.; Nielson, H.R., Control flow analysis for the \(π\)-calculus, (), 611-638
[10] M. Boreale, D. Sangiorgi, Bisimulation in naming-passing calculi without matching, Proc. 13th IEEE Symp. on Logic in Computer Science (LICS ’98), IEEE Computer Society Press, Silverspring, MD, 1998, pp. 165-175.
[11] Boudol, G., Typing the use of resources in a concurrent calculus, (), 239-253 · Zbl 0891.03009
[12] Brandt, M.; Henglein, F., Coinductive axiomatization of recursive type equality and subtyping, (), 63-81 · Zbl 1063.03510
[13] Cardelli, L.; Gordon, A., Mobile ambients, (), 140-155 · Zbl 0954.68108
[14] L. Cardelli, A. Gordon, Types for mobile ambients, Proc. ACM Symp. on Principles of Programming Languages, ACM Press, New York, 1999, pp. 79-92.
[15] Carriero, N.; Gelernter, D., Linda in context, Comm. ACM, 32, 4, 444-458, (1989)
[16] N. Carriero, D. Gelernter, J. Leichter, Distributed data structures in Linda, Proc. ACM Symp. on Principles of Programming Languages, ACM Press, New York, 1986, pp. 236-242.
[17] De Nicola, R.; Ferrari, G.; Pugliese, R., Coordinating mobile agents via blackboards and access rights, (), 220-237
[18] De Nicola, R.; Ferrari, G.; Pugliese, R., K\sclaim: a kernel language for agents interaction and mobility, IEEE trans. software eng., 24, 5, 315-330, (1998)
[19] R. De Nicola, R. Pugliese, A process algebra based on Linda, in: P. Ciancarini, C. Hankin (Eds.), COORDINATION’96, Proc. Lecture Notes in Computer Science, vol. 1061, Springer, Berlin, 1996, pp. 160-178. (Theoret. Comput. Sci., to appear.)
[20] Dezani-Ciancaglini, M.; de Liguoro, U.; Piperno, A., A filter model for concurrent \(λ\)-calculi, SIAM J. comput., 27, 5, 1376-1419, (1998) · Zbl 0916.03017
[21] Fournet, C.; Gonthier, G.; Lévy, J.-L.; Maranget, L.; Rémy, D., A calculus of mobile agents, (), 406-421
[22] Gelernter, D., Generative communication in linda, ACM trans. programm. languages systems, 7, 1, 80-112, (1985) · Zbl 0559.68030
[23] D. Gelernter, N. Carriero, S. Chandran et al., Parallel programming in Linda, Proc. IEEE Internat. Conf. on Parallel Programming, IEEE Computer Society Press, Silverspring, MD, 1985, pp. 255-263.
[24] N. Heintz, J.G. Riecke, The SLam calculus: programming with secrecy and integrity, Proc. ACM Symp. on Principles of Programming Languages, ACM Press, New York, 1998, pp. 365-377.
[25] M. Hennessy, J. Riely, Resource access control in systems of mobile agents, Proc. Internat. Workshop on High-Level Concurrent Languages, Electronic Notes in Theoretical Computer Science, vol. 16, Elsevier, Amsterdam, 1998. · Zbl 0917.68047
[26] N. Kobayashi, B. Pierce, D. Turner, Linearity and the \(π\)-calculus, Proc. ACM Symp. on Principles of Programming Languages, ACM Press, New York, 1996.
[27] Kozen, D.; Palsberg, J.; Schwartzbach, M., Efficient recursive subtyping, Mathematical structures in computer science, 5, 113-125, (1999) · Zbl 0840.03007
[28] Milner, R., Communication and concurrency, (1989), Prentice-Hall Int. Englewood Cliffs, NJ · Zbl 0683.68008
[29] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes (parts I and II), Inform. and comput., 100, 1-77, (1992)
[30] G. Necula, Proof-carrying code, Proc. ACM Symp. on Principles of Programming Languages, ACM Press, New York, 1997, pp. 106-119.
[31] U. Nestmann, B.C. Pierce, Decoding choice encodings, in: U. Montanari, V. Sassone (Eds.), CONCUR’96, Proc., Lecture Notes in Computer Science, vol. 1119, Springer, Berlin, 1996, pp. 179-194. · Zbl 1003.68080
[32] Pierce, B.; Sangiorgi, D., Typing and subtyping for mobile processes, Math. struct. comput. sci., 6, 5, 409-454, (1996) · Zbl 0861.68030
[33] R. Pugliese, Semantic theories for asynchronous languages, Ph.D. Thesis VIII-96-6, Univ. di Roma “La Sapienza”, Dip. Scienze dell’Informazione, 1996.
[34] J. Riely, M. Hennessy, Trust and partial typing in open systems of mobile agents, Proc. ACM Symp. on Principles of Programming Languages, ACM Press, New York, 1999. · Zbl 1069.68076
[35] P. Sewell, Global\(/\)local subtyping and capability inference for a distributed \(π\)-calculus, in: K.G. Larsen, S. Skyum, G. Winskel (Eds.), Internat. Colloquium on Automata, Languages and Programming (ICALP’98), Proc., Lecture Notes in Computer Science, vol. 1443, Springer, Berlin, 1998, pp. 695-706.
[36] R. Statman, Recursive types and the subject reduction theorem, Technical Report 94-164, Carnegie Mellon University, 1994.
[37] J. Vitek, G. Castagna, Towards a calculus of secure mobile computations, Proc. Workshop on Internet Programming Languages, Chicago, 1998.
[38] Volpano, D.; Smith, G., A typed-based approach to program security, (), 607-621
[39] D. Volpano, G. Smith, Secure information flow in a multi-threaded imperative language, Proc. ACM Symp. on Principles of Programming Languages, ACM Press, New York, 1998, pp. 355-364.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.