Resource access control in systems of mobile agents.

*(English)*Zbl 1009.68081Summary: We describe a typing system for a distributed \(\pi\)-calculus which guarantees that distributed agents cannot access the resources of a system without first being granted the capability to do so. The language studied allows agents to move between distributed locations and to augment their set of capabilities via communication with other agents. The type system is based on the novel notion of a location type, which describes the set of resources available to an agent at a location. Resources are themselves equipped with capabilities, and thus an agent may be given permission to send data along a channel at a particular location without being granted permission to read data along the same channel. We also describe a tagged version of the language, where the capabilities of agents are made explicit in the syntax. Using this tagged language we define access violations as runtime errors and prove that well-typed systems are incapable of such errors.

##### MSC:

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

PDF
BibTeX
XML
Cite

\textit{M. Hennessy} and \textit{J. Riely}, Inf. Comput. 173, No. 1, 82--120 (2002; Zbl 1009.68081)

Full Text:
DOI

##### References:

[1] | Amadio, R.; Prasad, S., Localities and failures, Proc. 14th foundations of software technology and theoretical computer science, (1994), Springer-Verlag Berlin · Zbl 1044.68682 |

[2] | Amadio, R.; Prasad, S., Modelling IP mobility, (1997), Laboratoire d’Informatique de Marseille |

[3] | Amadio, R., An asynchronous model of locality, failure, and process mobility, Coordination ’97, (1997), Springer-Verlag Berlin |

[4] | Berry, G.; Boudol, G., The chemical abstract machine, Conference record of the ACM symposium on principles of programming languages, San Francisco, (1990), Assoc. Comput. Mach New York, p. 81-94 |

[5] | Boudol, G.; Amadio, R.; Lhoussaine, C., The receptive distributed pi-calculus, Proceedings of the FST-TCS’99, (1990), Springer-Verlag Berlin, p. 304-315 · Zbl 0958.68117 |

[6] | Cardelli, L.; Gordon, A.D., Mobile ambients, Proceedings FOSSACS’98, (1998), Springer-Verlag Berlin · Zbl 0954.68108 |

[7] | Cardelli, L., A language with distributed scope, Comput. systems, 8, 27-59, (1995) |

[8] | Carriero, N.; Gelernter, D., Linda in context, Comm. assoc. comput. Mach., 32, 444-458, (1989) |

[9] | Carriero, N.; Gelernter, D.; Zuck, L., Bauhaus linda, Object-based models and languages for concurrent systems, (1995), Springer-Verlag Berlin, p. 66-76 |

[10] | De Nicola, R.; Ferrari, G.; Pugliese, R., Klaim: A kernel language for agents interaction and mobility, IEEE trans. software engrg., 24, 315-330, (1988) |

[11] | Mani, Chandy K., A world-wide distributed system using Java and the Internet, IEEE international symposium on high performance distributed computing, (1996), IEEE Press New York |

[12] | Fournet, C.; Gonthier, G., The reflexive CHAM and the join-calculus, Conference record of the ACM symposium on principles of programming languages, Paris, January 1996, (1996), Assoc. Comput. Mach New York |

[13] | Fournet, C.; Gonthier, G.; Levy, J.J.; Marganget, L.; Remy, D., A calculus of mobile agents, (), 406-421 |

[14] | Fournet, C.; Laneve, C.; Maranget, L.; Rémy, D., Implicit typing à la ml for the join-calculus, CONCUR: Proceedings of the international conference on concurrency theory, Warsaw, August, 1997, (1997), Springer-Verlag Berlin |

[15] | General Magic Inc. 1997, Agent technology, available at, http://www.genmagic.com/html/agentoverview.html. |

[16] | Giacalone, A.; Mishra, P.; Prasad, S., A symmetric integration of concurrent and functional programming, Internat. J. parallel programming, 18, 121-160, (1989) |

[17] | Heintz, N.; Riecke, J.G., The slam calculus: programming with secrecy and integrity, Conference record of the ACM symposium on principles of programming languages, San Diego, January 1998, (1988), Assoc. Comput. Mach New York |

[18] | Hennessy, M.; Riely, J., Type-safe execution of mobile agents in anonymous networks, Secure Internet programming: security issues for distributed and mobile objects, (1999), Springer-Verlag Berlin |

[19] | IBM Corp. 1996, The IBM aglets workbench, available at, http://www.trl.ibm.co.jp/aglets/. |

[20] | Karjoth, G.; Lange, D.B.; Oshima, M., A security model for aglets, IEEE Internet comput., 1, 68-77, (1997) |

[21] | Kobayashi, N.; Pierce, B.C.; Turner, D.N., Linearity and the pi-calculus, Conference record of the ACM symposium on principles of programming languages, Paris, January 1996, (1996), Assoc. Comput. Mach New York |

[22] | Milner, R., The polyadic π-calculus: A tutorial, (1991), University of EdinburghDepartment of Computer Science |

[23] | Milner, R. Also 1993, inLogic and Algebra of SpecificationF. L. Bauer, W. Brauer, and H. Schwichtenberg, Eds., Springer-Verlag, Berlin. |

[24] | Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, parts I and II, Inform. and comput., 100, 1-77, (1992) |

[25] | ObjectSpace Inc. 1997, Objectspace voyager, available at, http://www.objectspace.com/voyager. |

[26] | Perkins, C., IP mobility support, (1996) |

[27] | Pierce, B.; Sangiorgi, D., Typing and subtyping for mobile processes, Math. structures comput. sci., 6, 409-454, (1996) · Zbl 0861.68030 |

[28] | Riely, J.; Hennessy, M., A typed language for distributed mobile processes, Conference record of the ACM symposium on principles of programming languages, San Diego, January 1998, (1998), Assoc. Comput. Mach New York · Zbl 0917.68047 |

[29] | Riely, J.; Hennessy, M., Trust and partial typing in open systems of mobile agents, Conference record of the ACM symposium on principles of programming languages, san antonio, January 1999, (1999), Assoc. Comput. Mach New York · Zbl 1069.68076 |

[30] | Sewell, P., Global/local subtyping for a distributed π-calculus, (1997), Cambridge UniversityComputer Laboratory |

[31] | Sun Microsystems Inc. 1995, Java home page, available at, http://www.javasoft.com/. |

[32] | Turner, D., The polymorphic pi-calculus: theory and implementation, (1995), Edinburgh University |

[33] | Vitek, J.; Castagna, G., A calculus of secure mobile computations, Secure Internet programming: security issues for distributed and mobile objects, (1999), Springer-Verlag Berlin |

[34] | Wojciechowski, P.T.; Sewell, P., Nomadic pict: language and infrastructure design for mobile agents, IEEE concurrency, 8, 42-52, (2000) |

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.