¡¡Chinese Journal of Computers   Full Text
  TitleA Information-Flow-Based Verification Solution with Security Sensitivity to Check Security Policy of SELinux
  AuthorsZHANG Yang
  Address(State Key Laboratory of Information Security, Institute of Software£¬ Chinese Academy of Sciences, Beijing 100190)
  Year2009
  IssueNo.4(709¡ª720)
  Abstract &
  Background 		Abstract According to the implementation of multi-policy in SELinux, the authors introduce the multi-level sensitivity label into the traditional information flow analysis. On the basis of automata and linear temporal logic, an improved information flow analysis is proposed. It can verify both the integrity and confidentiality of the SELinux policies.
Keywords secure operating system; SELinux; secure policy; information flow; finite state machine
Background The work attributes to the project ¡°Research on the Key Technology of High-level Secure OS Design and Verification¡±, which is supported by the National High Technology Research and Development Program (863 Program) of China under grant Nos.2007AA01Z465, 2006AA01Z433, 2007AA01Z414.
SELinux has been adopted in the mainstream Linux Distributions for the reason that it extends Linux with a flexible mandatory access control mechanism that enforce security policies expressed in SELinux¡¯s policy language. However, determining whether a given policy meets security goals is difficult, due to the size and the complexity of SELinux policies. To analyze the validity and conformance with the security goal of SELinux policy configurations, many approaches has been developed. These methods can be divided into two categories: access control space based and information flow based. While the access control space-based analysis can not deal with the illegal information flow caused by indirect access requirement and its analysis procedure is complex and not intuitive, the information flow-based method draws more and more researcher¡¯s attention.
In this paper, to the question that current information flow-based SELinux policy analysis can not manipulate all its semantic properties (mls configuration for example), the authors introduce the multi-level sensitivity label into the traditional information flow analysis. On the basis of automata and linear temporal logic, an improved information flow analysis is proposed. It can verify both the integrity and confidentiality of the SELinux policies.