A logical specification and analysis for SELinux MLS policy

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

Research output: Contribution to journalArticlepeer-review

47 Scopus citations


The SELinux mandatory access control (MAC) policy has recently added a multilevel 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 the SELinux MLS model makes it impractical to manually evaluate that a given policy meets certain specific properties. To address this issue, we have modeled the SELinux MLS model, using a logical specification and implemented that specification in the Prolog language. Furthermore, we have developed some analyses for testing information flow properties of a given policy as well as 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. We also evaluated whether the policy associated to a given application is compliant with the policy of the SELinux system in which it would be deployed.

Original languageEnglish (US)
Article number26
JournalACM Transactions on Information and System Security
Issue number3
StatePublished - Jul 1 2010

All Science Journal Classification (ASJC) codes

  • General Computer Science
  • Safety, Risk, Reliability and Quality


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

Cite this