Project Summary

Computer systems teem with policies that govern their behavior. For instance:

• An access-control policy for a medical records system might dictate that a patient has access to all of her records, a doctor only to the patient's records pertaining to his specialty, and an orderly only to the doctor's instructions on the record.
• A firewall policy determines which sub-networks may and may not communicate with each other.
• A NAT translates names from one space to another.
• Policy-based routing applies user-defined policies to network traffic (to, for instance, address QoS needs).
• Security-Enhanced Linux (SELinux) consults rules on confidentiality and integrity requirements.
• Rules dictate desirable interoperation between compartments provided by a hypervisor (e.g., Xen).

Getting these policies right matters. Errors can be embarassing, costly, and even have legal consequences. But making mistakes is easy! These policies are rule-based, may be geographically distributed, encode complex dependencies, and interact with environments that change frequently. Furthermore, the global policy may be expressed in a collection of different and somewhat dissimilar languages that somehow interact. Policies are thus difficult to author, and will become even more so as they grow in complexity and scope.

Margrave is a tool for the static analysis of policies. Margrave can answer verification queries, namely checking whether a policy exhibits a certain property in all possible contexts. Of course, this only works when a user has concrete goals in mind, and it doesn't help them understand what they weren't thinking about. Thus, Margrave also supports property-free analysis. Imagine that an author has a policy that is known to ``work'' through some combination of (formal and informal) methods; now he has a new policy that represents a desired change, sometimes as a result of an emergency (as when a security leak is identified). While the author can test that the new policy implements the desired change, the edit may have had unintended consequences on other policy decisions. The author really needs to know, Will something break if I make this change?

Margrave answers this question by computing the set of access requests that yield different answers under the old and new policies. As this set can be quite large in practice, Margrave provides forensic tools to investigate these changes. The intutions of policy authors can be turned into a series of “smell-tests” that are applied to policies. These tests effectively become queries against either a policy or its changes. Margrave answers queries such as:

• Is the new policy equivalent to the old one?
• If there are changes, what are the changes when restricted to a certain type? (For example, restricting attention to those data formerly denied but now permitted access can identify inadvertent leakage.)
• What are the “hot-spots”, e.g., one rule change that altered the effect of a large percentage of outcomes?
• What roles or resources had their permissions changed?