A logical specification and analysis for SELinux MLS policy

Boniface Hicks, Sandra Rueda, Luke St. Clair, Trent Jaeger, Patrick McDaniel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

16 Scopus citations

Abstract

The SELinux mandatory access control (MAC) policy has recently added a multi-level security (MLS) model which is able to express a fine granularity of control over a subject's access rights. The problem is that the richness of this policy makes it impractical to verify, by hand, that a given policy has certain important information flow properties or is compliant with another policy. To address this, we have modeled the SELinux MLS policy using a logical specification and implemented that specification in the Prolog language. Furthermore, we have developed some analyses for testing the properties of a given policy as well an algorithm to determine whether one policy is compliant with another. We have implemented these analyses in Prolog and compiled our implementation into a tool for SELinux MLS policy analysis, called PALMS. Using PALMS, we verified some important properties of the SELinux MLS reference policy, namely that it satisfies the simple security condition and -property defined by Bell and LaPadula [2].

Original languageEnglish (US)
Title of host publicationSACMAT'07
Subtitle of host publicationProceedings of the 12th ACM Symposium on Access Control Models and Technologies
Pages91-100
Number of pages10
DOIs
StatePublished - 2007
EventSACMAT'07: 12th ACM Symposium on Access Control Models and Technologies - Sophia Antipolis, France
Duration: Jun 20 2007Jun 22 2007

Publication series

NameProceedings of ACM Symposium on Access Control Models and Technologies, SACMAT

Other

OtherSACMAT'07: 12th ACM Symposium on Access Control Models and Technologies
CountryFrance
CitySophia Antipolis
Period6/20/076/22/07

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Fingerprint Dive into the research topics of 'A logical specification and analysis for SELinux MLS policy'. Together they form a unique fingerprint.

  • Cite this

    Hicks, B., Rueda, S., St. Clair, L., Jaeger, T., & McDaniel, P. (2007). A logical specification and analysis for SELinux MLS policy. In SACMAT'07: Proceedings of the 12th ACM Symposium on Access Control Models and Technologies (pp. 91-100). (Proceedings of ACM Symposium on Access Control Models and Technologies, SACMAT). https://doi.org/10.1145/1266840.1266854