High-level Formal Modeling and Verication of Mandatory Access Control Policies Across Multiple Security-Enhanced Linux Devices Thesis uri icon



  • Thesis (M.S., Computer Science) -- University of Idaho, 2016 | The evolution of technological progress continually presents new information security challenges for large enterprises. Organizations must actively implement security policies to mitigate modern threats. Access control policies which define the way in which an organization's principals can interact with a system are particularly vital to enforce and verify. Accordingly, this thesis demonstrates that policies from an enterprise Linux implementation of a mandatory access control scheme can be used to populate a useful and efficient policy model. This model can be queried from a high-level to verify proper implementation of policies across one or more devices in a networked environment. It provides the user with both 1) a graphical representation of one or more policy implementations and 2) a means for an analyst to ensure whether specified actions between subjects and objects are permitted or not, aiding in providing them with an intuitive understanding of the higher-level organizational security policy.

publication date

  • June 1, 2016