Analysis Of SELinux Security Policies Based On Colored Petri-net

As the base of the entire information systems, operating systems are the direct managers of computer resources and their security issues are the most important information security issues. SELinux is a typical security enhanced module in Linux and it implements mandatory access control mechanism which can better ensure system security. Furthermore, security policies configuration is the key for SELinux to implement security and protection, but complicated policy models and thousands of policy rules make it hard to do correct and safe policy configuration, which limits the application of SELinux. Thus it is very significant to establish an automated tool for analyzing SELinux security policies. Specifically, there are three parts of work in this paper as following.(1) Research on SELinux and analysis methods of SELinux policies. Evolution of SELinux and its role in the whole access control architecture of Linux are discussed in the first place. And security models and policy configuration of SELinux are studied in detail. Then existing methods for analyzing SELinux policies are compared and analyzed. Among these methods, existing colored petri-net method has many advantages but its available implement completely depends on other mathematical software tool, which is impossible to be embedded into SELinux security policy configuration. The conclusion of automated analysis is drawn.(2) Research on automated analysis method of SELinux policies based on colored petri-net systematically. Some key problems including analysis goals, extraction of security policy elements, construction and query execution of colored petri-net are further studied, related simulation examples are presented. Overall, the security elements and access control relationships in policies are formalized to corresponding sets and mappings. Then BNF statements and mapping of access control relationships are transferred to corresponding places and transitions in colored petri-net. At last, security goals are verified with execution of transitions in petri-net. During the analysis, considering that security goal can not be described by positive or negative representation alone, a kind of BNF query statement combining positive and negative representation is used to describe the security goal.(3) Design and implementation of an automated analysis tool of SELinux policies. Overall architecture, data structures and key modules of the prototype are designed. An independent prototype for analyzing SELinux policies based on colored petri-net is designed and implemented with using83functions in C language in this paper. In addition, a set of SELinux policy configuration files as for some student-teacher application is input into the prototype for analysis and test, and test results are satisfactory.