Localised access control policies and global reasoning

In distributed systems, the traditional way of enforcing security is by means of access control security policies. We propose a framework and some analyses that can be done over it. The framework allows attaching security policies in the various locations of the system, following a realistic and practical fashion. As the runtime system involves interaction of locations, groups of policies may be relevant thereby needing a logic and consistent way of combining them. This leads to a complex system of networks and security policies that are only sometimes relevant. The resulting global system cannot then be trivially certified by static means. We propose a model checking that does not explore the entire state space but is inspired in static analysis techniques instead. Our aim is to have a formal framework with which it is possible to design distributed systems with adaptable and certifiable security.