Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal Methods

Abstract

The topic of access control has received a new lease of life in recent years as the need for assurance that the correct access control policy is in place is seen by many as crucial to providing assurance to individuals that their data is being treated appropriately. This trend is likely to continue with the increase in popularity of social networking sites and shifts to ‘cloud’-like commercial services: in both contexts, a clear statement of “who can do what” to one’s data is key in engendering trust. While approaches such as role-based access control (RBAC) provide a degree of abstraction, therefore increasing manageability and accessibility, policy languages such as the XML-based XACML provide greater degrees of expressibility—and, as a result, increased complexity. In this paper we explore how the mutual benefits of both RBAC and XACML, and Alloy and Z, may be used to best effect. RBAC is used as an accessible conceptual model; XACML is used as a language of implementation. Our concern is to facilitate the construction and reuse of role-based policies, which may subsequently be deployed in terms of XACML. We wish to provide assurance that these representations and transformations are, in some sense, correct. To this end, we consider formal models of both RBAC and XACML in terms of Z. We also describe how we have taken initial steps in utilising the Alloy Analyzer tool to provide a level of assurance that the two representations are consistent.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{SlaymakerPS10,
  author       = {Mark Slaymaker and
                  David J. Power and
                  Andrew Simpson},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {Formalising and Validating RBAC-to-XACML Translation Using Lightweight
                  Formal Methods},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {349--362},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_26},
  doi          = {10.1007/978-3-642-11811-1\_26},
  timestamp    = {Thu, 20 Jun 2024 12:26:13 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/SlaymakerPS10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}