Types for access control

KLAIM is an experimental programming language that supports a programming p aradigm where both processes and data can be moved across different computi ng environments. This paper presents the mathematical foundations of the KL AIM type system; this system permits checking access rights violations of m obile agents. Types are used to describe the intentions (read, write, execu te,...) of processes relative to the different localities with which they a re willing to interact, or to which they want to migrate. Type checking the n determines whether processes comply with the declared intentions, and whe ther they have been assigned the necessary rights to perform the intended o perations at the specified localities. The KLAIM type system encompasses bo th subtyping and recursively defined types. The former occurs naturally whe n considering hierarchies of access rights, while the latter is needed to m odel migration of recursive processes. (C) 2000 Elsevier Science B.V. All r ights reserved.