摘要

Safety and security is key aspect for successful application of the mobile computation. We introduce Confined-pi calculus to deal with secure movement and secure intercommunication of agents. Our system extends Nomadic-pi with objective migration primitive and confined region which serves as annotation labels of agents and channels. The confined region labels are used to uniquely identify the constraints on the mobility and communication of agents, so the agents could be confined in a secure subsystem and the inter-agent communication could be confined between agents located on trusted sites during computation. We give an operational semantics for the calculus, and develop a type system that enforces security properties called confined migration and confined communication.