SELinux (Security-Enhanced Linux) enforces mandatory access control (MAC) according to policies. However, due to the inherent complexity of systems, real-world SELinux policies often become intricate, comprising thousands of statements, making manual verification of their correctness and security challenging. In addition, specific environments with stringent security requirements demand the formal verification of policies. While existing policy tools primarily focus on particular aspects of policy analysis, such as integrity and consistency, there is a lack of a unified approach to satisfy diverse requirements.
To address the problems, a research team led by Yongwang Zhao published their new research on 15 June 2026 in Frontiers of Computer Science co-published by Higher Education Press.
The team proposed a novel approach for SELinux policy analysis based on the formal semantics of the SELinux policy language. With the semantics of the SELinux policy language formalized in a rewrite-based language framework, K, which provides a semantic simulation environment for access control and a formal symbol system for analysis, users can specify their analysis requirements as assertions and constraints in a unified and easy-to-use method. The built-in theorem prover in the K framework helps policy analysis for not only classical security properties but also various special requirements due to environments and scenarios.
SELinux (Security-Enhanced Linux) enforces mandatory access control (MAC) according to policies. However, due to the inherent complexity of systems, real-world SELinux policies often become intricate, comprising thousands of statements, making manual verification of their correctness and security challenging. In addition, specific environments with stringent security requirements demand the formal verification of policies. While existing policy tools primarily focus on particular aspects of policy analysis, such as integrity and consistency, there is a lack of a unified approach to satisfy diverse requirements.
To address the problems, a research team led by Yongwang Zhao published their new research on 15 June 2026 in Frontiers of Computer Science co-published by Higher Education Press.
The team proposed a novel approach for SELinux policy analysis based on the formal semantics of the SELinux policy language. With the semantics of the SELinux policy language formalized in a rewrite-based language framework, K, which provides a semantic simulation environment for access control and a formal symbol system for analysis, users can specify their analysis requirements as assertions and constraints in a unified and easy-to-use method. The built-in theorem prover in the K framework helps policy analysis for not only classical security properties but also various special requirements due to environments and scenarios.

In the research, they formalize the semantics of the SELinux policy language in the K framework and implement a prototype tool based on the semantics with several security properties specified, including integrity, completeness, consistency, and so on. They apply the tool for real-world policies and find a lot of issues in refpolicy and AOSP policy.
Compared with other existing works, this approach provides a unified method to hold a comprehensive policy analysis for various requirements with formal guarantees.
Future work can focus on improving the performance of semantic execution and encapsulating the procedure of specifying analysis requirements to increase the analysis efficiency and reduce the prior knowledge needed for non-professional users and policy managers.

DOI:10.1007/s11704-024-40495-7