Access-Control Policies via Belnap Logic: Effective and Efficient Composition and Analysis

It is difficult to develop and manage large, multi-author access control policies without a means to compose larger policies from smaller ones. Ideally, an access-control policy language will have a small set of simple policy combinators that allow for all desired policy compositions. In cite{BH07}, a policy language was presented having policy combinators based on Belnap logic, a four-valued logic in which truth values correspond to policy results of "grant", "deny", "conflict", and "undefined". We show here how policies in this language can be analyzed, and study the expressiveness of the language. To support policy analysis, we define a query language in which policy analysis questions can be phrased. Queries can be translated into a fragment of first-order logic for which satisfiability and validity checks are computable by SAT solvers or BDDs. We show how policy analysis can then be carried out through model checking, validity checking, and assume-guarantee reasoning over such translated queries. We also present static analysis methods for the particular questions of whether policies contain gaps or conflicts. Finally, we establish expressiveness results showing that all {em data independent} policies can be expressed in our policy language.