CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016

We describe the formalization of a correctness proof for a conflict detection algorithm for XACML (eXtensible Access Control Markup Language). XACML is a standardized declarative access control policy language that is increasingly used in industry. In practice it is common for rule sets to grow large, and contain unintended errors, often due to conflicting rules. A conflict occurs in a policy when one rule permits a request and another denies that same request. Such errors can lead to serious risks involving both allowing access to an unauthorized user as well as denying access to someone who needs it. Removing conflicts is thus an important aspect of debugging policies, and the use of a verified algorithm provides the highest assurance in a domain where security is important. In this paper, we focus on several complex XACML constructs, including time ranges and integer intervals, as well as ways to combine any number of functions using the boolean operators and, or, and not. The latter are the most complex, and add significant expressive power to the language. We propose an algorithm to find conflicts and then use the Coq Proof Assistant to prove the algorithm correct. We develop a library of tactics to help automate the proof.

Tue 19 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

14:00 - 15:30: Session 7: Verification for Concurrent and Distributed SystemsCPP at Room St Petersburg II
14:00 - 14:30
Johannes Å. PohjolaUppsala University, Joachim ParrowUppsala University
14:30 - 15:00
Doug WoosUniversity of Washington, James R. WilcoxUniversity of Washington, Steve AntonUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Michael D. ErnstUniversity of Washington, Thomas AndersonUniversity of Washington
15:00 - 15:30
Michel St-MartinUniversity of Ottawa, Amy FeltyUniversity of Ottawa