Controlling Security Policies in a Distributed Environment

Abstract

This thesis proposes a typing discipline to control the migration of code in a distributed, mobile environment. Our approach is to express security policies as types, to characterise security faults as typing errors, and to use a type system to statically enforce a given security policy. We prove a type safety result that ensures that well-typed programs do not violate the prescribed security policy. We start by analysing a simple, yet non-trivial, approach to control the access to resources in a concurrent language (the $\pi-$calculus). In the concurrent framework we study the control of actions at program level and, in a finer-grained scenario, at resource level. Moving into a distributed, concurrent platform (using the D$\pi$-calculus as the underlying language), we analyse the impact of code mobility in the verification of security. In a first stage, we control mobility by specifying security policies at site level, and by considering only the source site, the target site, and the action to be executed, as the relevant information to decide if an action should be performed. This approach revealed some vulnerabilities, namely that a site cannot control by itself its own security: it always need to trust in third-parties. Aiming at overcoming this undesired lacuna, as well as simplifying the writing and maintenance of security policies, we introduce the concepts of groups, a cluster of sites that share the same security polices, and of path to account for the sequence of sites visited by migrating code. We define security at group level, avoiding the replication of polices by the sites that are members of the same group. Granting privileges to migrating paths allows for a site to precisely select the action that it grants permission to be executed (without needing to depend on third-parties). Our major result is that, recalling Milners motto, well-typed programs do not go wrong, in the sense that, if a network has no typing error, then it does not incur in a security fault.