In: Lecture Notes in Computer Science : Advances in Information and Computer Security, Volume 4266, 2006, pages 389-404. 2006. URL: http://dx.doi.org/10.1007/1190873928.
Abstract: This paper presents a Colored Petri Nets (CPN) approach to analyze the information flow in the policy file of Security-Enhanced Linux (SELinux). The SELinux access control decisions are based on a security policy file that contains several thousands of security rules. It becomes a challenge for policy administrator to determine whether the modification of the security policy file conforms to the pre-specified security goals. To address this issue, this paper proposes a formal information flow model for SELinux security policy file, and presents a simple query language to help administrators to express the expected/unexpected information flow. We developed a method to transform the SELinux policy and security goal into Policy CPN Diagram and Query CPN Diagram. A tool named SEAnalyzer that can automatically verify the SELinux policy has been developed and two application examples of this tool will be presented in the context.
Keywords: Colored Petri Nets; information flow; SELinux; security policy.