Access-control policies have grown from simple matrices to non-trivial specifications in their own right: they are written, separately from the applications that use them, in domain-specific languages; they are often composed of (sometimes geographically distributed) fragments, which are combined using semantically rich policy-combination operators; and they consult a dynamic environment comprised of information from many sources including the underlying application and the operating environment of the system. These features make policies hard to get right, in part because policy authors must understand how their policies will interact with an environment that is constantly changing.
Policy authors thus need increasingly strong tools to help understand the effects of their policies. These tools must support common authoring scenarios. Authors often have a policy that "works" and a new policy that encapsulates a desired change. Testing can foster confidence that the changes do what is desired, but generally miss effects that weren't expected. For such scenarios, it is far more useful to employ a process such as change-impact analysis, which semantically compares two policies while respecting the dynamic nature of the environment. Traditional property-based analyses such as formal verification, while useful, do not support this scenario.
This project is developing the theoretical foundations and prototype tools for analyzing realistic access-control policies in their dynamic environments. The tools support both property-based verification and property-free analyses such as change-impact analysis for industrial standard policy languages (such as XACML). The novel components of this project are its fine-grained and rich model of the dynamic environment and its focus on property-free analyses that accommodate common authoring scenarios.
