Access-control policies, firewall configurations, hypervisor configurations, social-network privacy settings, ...
Modern computing systems are teeming with policies. Errors in policies can be embarassing, costly, and have legal consequences. But making mistakes is easy! Policies may be geographically distributed, encode complex dependencies, and interact with environments that change frequently. Enforcing an organization's security goals may require the cooperation of several policies in different languages and at different levels of abstraction.
How can a policy author gain confidence in their settings?
Margrave is a policy-analysis tool with several powerful capabilities:
It computes exhaustive sets of scenarios that yield different results under a pair of policies.
Imagine that you have just edited an existing policy, either to fix a bug or add a feature. It is easy to test that the edit had the desired effect, but how do you test that the edit yields no undesirable side effects? Margrave's change-impact analysis lets you compare the effects of multiple policies. It provides the benefits of static verification without requiring authors to write formal properties!
It supports query-based verification and provides query-based views of policies.
It supports reasoning about the combined effects of policies written in different configuration languages, such as a firewall filter and a static router, or a firewall combined with an access-control policy (perhaps on a different component).
It supports many standard configuration input languages, such as XACML 1 and 2, and Cisco's IOS. A documented intermediate language enables third-party extensions to support other input languages.
It supports firewall features—such as NAT, static routing, and reflexive access lists—which many other policy analyzers ignore.
Margrave is available for free download. Both the tutorial for our latest version and one of our recent conference talks provide a high-level overview of the tool. Our papers describe the technical underpinnings.