Formal verification of cross-domain access control policies using model checking
Date
2011-12-30
DOI
Authors
Reynolds, Mark
Bestavros, Azer
Version
OA Version
Citation
Reynolds, Mark; Bestavros, Azer. "Formal Verification of Cross-Domain Access Control Policies Using Model Checking", Technical Report BUCS-TR-2011-031, Computer Science Department, Boston University, December 30, 2011. [Available from: http://hdl.handle.net/2144/11388]
Abstract
In assigning access permissions to users, formal policies fill a key role in mapping access from user attributes to resources. In a single domain a policy should be both sound (no false positives) and also complete (no false negatives). When policies from different domains are combined, several issues can arise. The most immediate issue is mapping potentially disparate attributes, roles and sources from one domain model to the other. Once this has been addressed, however, a more serious problem can arise: even if the domain policies are individually self-consistent, they may not be mutually consistent. To date, the typical approach has been a brute-force enumeration of all possible aggregate states in what might be termed “analysis of composition”. This approach is manifestly not scalable. This paper describes first steps toward a new “composition of analysis” approach. This approach uses the Alloy modeling language to cast the resource accessibility problem as a constrained graph reachability problem. An Alloy model is created for each domain policy, and these models are then composed in a sound and efficient manner. This paper will describe results for the two domain and three domain cases, and sketch a general, scalable approach that can be applied to compositions of arbitrary complexity.