A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules

被引:13
作者
St-Martin, Michel [1 ]
Felty, Amy P. [1 ]
机构
[1] Univ Ottawa, Sch Elect Engn & Comp Sci, Ottawa, ON K1N 6N5, Canada
来源
PROCEEDINGS OF THE 5TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP'16) | 2016年
关键词
program correctness; formal verification; access control; policy analysis; Coq; XACML;
D O I
10.1145/2854065.2854079
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页码:166 / 175
页数:10
相关论文
共 18 条
  • [1] [Anonymous], COQ PROOF ASS REF MA
  • [2] Bertot Y., 2004, TEXT THEORET COMP S
  • [3] Capretta V, 2007, FMSE'07: PROCEEDINGS OF THE 2007 ACM WORKSHOP ON FORMAL METHODS IN SECURITY ENGINEERING, P22
  • [4] CHOMICKI J, 2000, 7 INT C PRINC KNOWL
  • [5] Dougherty DJ, 2007, LECT NOTES COMPUT SC, V4734, P578
  • [6] Fisler K, 2005, PROC INT CONF SOFTW, P196
  • [7] Graham H., 2008, International Journal on Software Tools for Technology Transfer (STTT), Special issue on selected papers from workshop on Web Quality, Verification and Validation, V10, P473
  • [8] Huonder F., 2010, THESIS
  • [9] MANKAI M., 2005, NOTERE, P85
  • [10] OASIS, 2004, EXTENSIBLE ACC CONTR