Model and analysis of Role-Based Access Control in SELinux using Description Logic

Alan Ashton Dickerson

AbstractSecurity-Enhanced Linux (SELinux) is a version of Linux which, amongst other things, supports Role-Based Access Control (RBAC). The use of the access controls in SELinux have proven to be difficult to use and to perform maintenance upon, especially as the system evolves it may be difficult for the system administrators to comprehend the effects of the changes on the access control policy. Development of an analysis tool for RBAC in SELinux is therefore an important goal.

[Chen Zhao and Lin, 2005] discuss how elements of RBAC can be modeled using the Description Logic ALLQ , and demonstrate how a reasoner for ALCQ can be used for analysis.

The thesis presents a definition of the access controls of SELinux and shows how to formalize these in ALCQ . It introduces rules for use of an automated implementation of a tool that will model most SELinux configurations. It sketches out ways that the reasoner for an SELinux representation in ALCQ can be used for analysis by invoking queries.
KeywordsRole-Based Access Control, Description Logic, Security-Enhanced Linux, Formal models
TypeMaster's thesis [Academic thesis]
Year2006
PublisherInformatics and Mathematical Modelling, Technical University of Denmark, DTU
AddressRichard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby
SeriesIMM-Thesis-2006-20
NoteSupervised by Michael R. Hansen and Robin Sharp, IMM.
Electronic version(s)[pdf]
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering