@MASTERSTHESIS\{IMM2006-04446,
    author       = "A. A. Dickerson",
    title        = "Model and analysis of Role-Based Access Control in SELinux using Description Logic",
    year         = "2006",
    keywords     = "Role-Based Access Control, Description Logic, Security-Enhanced Linux, Formal models",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Michael R. Hansen and Robin Sharp, {IMM}.",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/4446-full.html",
    abstract     = "Security-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."
}