Search

If an access control policy promises that a resource is protected in a system, how do we know it is really protected? To give an answer we formalise in this paper the Role-Compatibility Model–a framework, introduced by Ott, in which access control policies can be expressed. We also give a dynamic model determining which security related events can happen while a system is running. We prove that if a policy in this framework ensures a resource is protected, then there is really no sequence of events that would compromise the security of this resource. We also prove the opposite: if a policy does not prevent a security compromise of a resource, then there is a sequence of events that will compromise it. Consequently, a static policy check is sufficient (sound and complete) in order to guarantee or expose the security of resources before running the system. Our formal model and correctness proof are mechanised in the Isabelle/HOL theorem prover using Paulson's inductive method for reasoning about valid sequences of events. Our results apply to the Role-Compatibility Model, but can be readily adapted to other role-based access control models.

Directory Service is used widely in modern communication networks. In this paper, we proposed and implemented a management system based on event bus pattern to manage directory service network constructed by improving OpenLDAP [1]. The management system presents good architecture while implementing complex management functions. The principles and use of event bus pattern in the system is described in detail and experience shows that this pattern makes the system have considerable flexibility, maintainability, extensibility and a general applicability to many other applications.