Sciweavers

Share
TISSEC
2010

A logical specification and analysis for SELinux MLS policy

8 years 5 months ago
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...
Boniface Hicks, Sandra Rueda, Luke St. Clair, Tren
Added 22 May 2011
Updated 22 May 2011
Type Journal
Year 2010
Where TISSEC
Authors Boniface Hicks, Sandra Rueda, Luke St. Clair, Trent Jaeger, Patrick McDaniel
Comments (0)
books