An approach for SELinux policy analysis via semantic execution
image:
image
view moreCredit: HIGHER EDUCATION PRESS
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.
Journal
Frontiers of Computer Science
Method of Research
Experimental study
Subject of Research
Not applicable
Article Title
K-SELinux: formal analysis and verification of SELinux policies via semantic execution
Fault-tolerant paths and disjoint paths: boosting data center network reliability with augmented cubes
Higher Education Press
image:
image
view moreCredit: HIGHER EDUCATION PRESS
Researchers have developed new algorithms to enhance the reliability of data center networks (DCNs) by constructing fault-tolerant paths and maximum disjoint paths in augmented cube-based architectures. These breakthroughs address critical challenges in handling node failures and improving data transmission efficiency, which are vital as cloud computing and big data continue to drive DCN expansion. The findings were published on 15 June 2026 in Frontiers of Computer Science, a journal co-published by Higher Education Press and Springer Nature.
As DCNs grow in scale and complexity, even minor node or link failures can disrupt services, leading to data loss or downtime. Traditional routing strategies often struggle with slow fault recovery and suboptimal path lengths. To tackle this, a team led by Weibei Fan from Nanjing University of Posts and Telecommunications focused on the augmented cube-based DCN (AQDNₙ), a structure known for its scalability and high connectivity.
The team’s first innovation is a fault-tolerant path construction algorithm. It ensures communication between any two fault-free nodes even when up to 2n−2 nodes fail (where n is the dimension of AQDNₙ). By leveraging the recursive structure of augmented cubes and optimizing cross-edge connections, the algorithm efficiently bypasses faults.
Their second key contribution is the AQDN-DP algorithm, which constructs 2n−1 disjoint paths between any two nodes— the maximum possible number determined by AQDNₙ’s (2n−1)-connectivity. These paths avoid shared nodes or links, eliminating common-mode failure risks and enabling load balancing.
Comparative experiments against traditional BFS (Breadth-First Search) showed striking improvements: the fault-tolerant algorithm reduced average execution time by 16.37% and path length by 54.23%. AQDN-DP also demonstrated strong fault tolerance, with more parallel links supporting reliable transmission as n increases.
"We designed these algorithms to ensure data centers can handle failures gracefully while maintaining efficiency," said Weibei Fan. "This means more stable cloud services, faster data processing, and better resilience against unexpected disruptions."
Moving forward, the team plans to explore applications in larger-scale networks and integrate adaptive learning to optimize paths in real time.
Journal
Frontiers of Computer Science
Method of Research
Experimental study
Subject of Research
Not applicable
Article Title
Fault-tolerant path and disjoint path construction in data center network based on augmented cube
No comments:
Post a Comment