Title
Sophisticated Access Control via SMT and Logical Frameworks
Abstract
We introduce a new methodology for formulating, analyzing, and applying access-control policies. Policies are expressed as formal theories in the SMT (satisfiability-modulo-theories) subset of typed first-order logic, and represented in a programmable logical framework, with each theory extending a core ontology of access control. We reduce both request evaluation and policy analysis to SMT solving, and provide experimental results demonstrating the practicality of these reductions. We also introduce a class of canonical requests and prove that such requests can be evaluated in linear time. In many application domains, access requests are either naturally canonical or can easily be put into canonical form. The resulting policy framework is more expressive than XACML and languages in the Datalog family, without compromising efficiency. Using the computational logic facilities of the framework, a wide range of sophisticated policy analyses (including consistency, coverage, observational equivalence, and change impact) receive succinct formulations whose correctness can be straightforwardly verified. The use of SMT solving allows us to efficiently analyze policies with complicated numeric (integer and real) constraints, a weak point of previous policy analysis systems. Further, by leveraging the programmability of the underlying logical framework, our system provides exceptionally flexible ways of resolving conflicts and composing policies. Specifically, we show that our system subsumes FIA (Fine-grained Integration Algebra), an algebra recently developed for the purpose of integrating complex policies.
Year
DOI
Venue
2014
10.1145/2595222
ACM Trans. Inf. Syst. Secur.
Keywords
DocType
Volume
policy analysis,underlying logical framework,sophisticated policy analysis,programmable logical framework,access-control policy,previous policy analysis system,complex policy,resulting policy framework,composing policy,Sophisticated Access Control,Logical Frameworks,canonical form
Journal
16
Issue
ISSN
Citations 
4
1094-9224
9
PageRank 
References 
Authors
0.53
40
3
Name
Order
Citations
PageRank
Konstantine Arkoudas118619.63
Ritu Chadha213726.01
Jason Chiang3473.46