Verification Of Rules In Spatial Access Control Systems Through Model Checking

In order to achieve the necessary safety requirements, the role-based access control model Spatial-RBAC, with the spatial characteristics, must meet the three constraints: the constraint on spatial region, the spatial separation of duty constraint and the constraint on cardinality of spatial role activation. It is very crucial to ensure the security of the access control system that verifying whether the access control system meet the three constraints.In this paper, the model checking method was used to verify whether the rules of spatial access control system meet the corresponding constraints. Model checking technology is a widely used automated analysis method in verifying finite-state systems, and the basic idea is to establish a model of finite-state system, and then verify whether the system meet the properties by searching the states in the model. The main contents of this paper as follows:(1)A method of representing spatial access control system, which is based on predicate logic was proposed. In this method, the system consists of predicates and rules, in which the predicate indicates the relationship of the spatial class object, the rules reflect the authorities of reading and writing the predicates. Spatial information processed by the mapping function is one of the conditions authorized as a system to ensure that the system described in the specification and concise.(2)The representing method and detecting algorithm of properties to be verified were given. The representation of constraint attributes in the Spatial-RBAC were given in a unified form, and a new algorithm detecting the rules of spatial access control system was proposed in the base of existing model checking method. The algorithm uses the user's knowledge of the system to indicate system status, and puts the reading and writing authority as a condition of state change, starting from the target state after the forward traversal from the system state space to identify the operation needed to achieve targets sequence, if the search is successful, it means that some space constraints are not satisfied in the system.(3)The function of model checking tool ACPEG was improved. By adding the spatial information processing capacity and modifying the source code to achieve the detection algorithm, the tool could meet the need of detecting spatial access control system rules. Finally, an example of access control system was analyzed and the result shows that the proposed detection method is correct and effective.