On the Construction and Verification of Self-modifying Access Control Policies

摘要

Typically, access control policies are either static or depend on independently maintained external state to achieve some notion of dynamism. While it is possible to fully verify the properties of static policies, any reference to external state will necessarily limit the scope of such verification. In this paper we explore the feasibility of describing self-modifying policies which contain both rules for granting access and rules for the modification of the policy. Policy level constraints are used to define validity. Using these constraints it becomes possible to verify both the current state of the policy and any possible future states. A working prototype is described which utilises a relational model finder to perform the verification. The prototype is capable of generating instances of failure cases and presenting them via a simple user interface.