Information flow query and verification for security policy of security-enhanced linux

Yi Ming Chen, Yung Wei Kao

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Scopus citations


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.

Original languageEnglish
Title of host publicationAdvances in Information and Computer Security - First International Workshop on Security, IWSEC 2006, Proceedings
PublisherSpringer Verlag
Number of pages16
ISBN (Print)3540476997, 9783540476993
StatePublished - 2006
Event1st International Workshop on Security, IWSEC 2006 - Kyoto, Japan
Duration: 23 Oct 200624 Oct 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4266 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference1st International Workshop on Security, IWSEC 2006


  • Colored petri nets
  • Information flow
  • Security policy
  • SELinux


Dive into the research topics of 'Information flow query and verification for security policy of security-enhanced linux'. Together they form a unique fingerprint.

Cite this