Show simple item record

dc.contributor.authorReynolds, Marken_US
dc.contributor.authorBestavros, Azeren_US
dc.date.accessioned2015-06-24T19:48:43Z
dc.date.available2015-06-24T19:48:43Z
dc.date.issued2011-12-30
dc.identifier.citationReynolds, 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]
dc.identifier.urihttps://hdl.handle.net/2144/11388
dc.description.abstractIn 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.en_US
dc.language.isoen_US
dc.publisherComputer Science Department, Boston Universityen_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2011-031
dc.subjectAlloyen_US
dc.subjectPolicy modelingen_US
dc.subjectCompositional analysisen_US
dc.titleFormal verification of cross-domain access control policies using model checkingen_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record