[Prev][Next][Index][Thread]

TR announcement: Resource Access Control in Systems of Mobile Agents

The following tech report is now available, discussing type systems
for controlling resources in a distributed pi-calculus.  The report
can be retrieved from:

  http://www.cogs.susx.ac.uk/cgi-bin/htmlcogsreps?cs

Comments appreciated.

Cheers,
James.
---------------------------------------------------------------------
Resource Access Control in Systems of Mobile Agents
Matthew Hennessy and James Riely

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.