Project Summary

Access-control (and similar) policies are increasingly written as separate program components using domain-specific languages. We aim to exploit this separation both to analyze policies independently of programs and to analyze the interactions between policies and programs. We are particularly interested in analyses, such as semantic differencing, that do not require users to write properties. Our work is motivated by problems we encountered writing real software with access-control components, and is yielding both papers and implementations.

More Detailed Description

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 combination operators specific to the domain of policies.
• They consult a dynamic environment comprised of information from many sources including the underlying program 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. At the same time, policies are becoming pervasive: there is growing support for industrially-driven standards such as XACML; the .NET framework now incorporates support for authoring and deploying access-control policies; and modern Web applications permit sharing and collaboration, thus enabling users to construct policies governing their data. Policy authors thus need increasingly strong tools to help understand the effects of their policies.

Building tools for policies requires a careful understanding of their use cases. In particular, the blind use of “verification” is not enough: we must account for common authoring scenarios. The typical policy author, for example, often has a policy that is known to “work” through some combination of (usually informal) methods; now he has a new policy that represents a desired change. Testing can help gain confidence that the changes do what is desired, but what about the effects that weren't expected (and are thus not subject to testing)? For such scenarios, it is far more useful to employ a process such as change-impact analysis, which semantically compares two policies in the absence of formal properties while respecting the dynamic nature of the environment.

The PIPA/Margrave project is developing the theoretical foundations and prototype tools for analyzing realistic access-control policies in their dynamic environments. PIPA stands for “Policy-Informed Program Analysis”, and captures the spirit of our multi-lingual analysis approach. Margrave is the name of our resulting toolsuite. Our analyses include both property-based verification and property-free analyses such as change-impact analysis. Our tools support industrial standard policy languages (such as XACML) as inputs. The novel components of this project are our fine-grained and rich model of the dynamic environment and our focus on property-free analyses that accommodate common authoring scenarios.