A logical specification and analysis for SELinux MLS policy

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...

• Type: Journal
• Year: 2010
• Where: TISSEC
• Authors: Boniface Hicks, Sandra Rueda, Luke St. Clair, Trent Jaeger, Patrick McDaniel
• Keywords: Education, Policy, Security, SELinux MLS Policy, TISSEC 2010