K-SELinux: formal analysis and verification of SELinux policies via semantic execution

Abstract

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, certain environments with stringent security requirements demand the formal verification of policies. While existing policy tools primarily focus on specific aspects of policy analysis, such as integrity and consistency, they lack a unified approach to satisfy diverse requirements. Essentially, their capabilities are limited, and formal guarantees are often absent.

To address these issues, we have comprehensively formalized the semantics of the SELinux policy language in the \mathbb{K} framework. This approach provides a universal foundation for specifying various requirements, benefiting policy managers and policy tool developers. Furthermore, employing this approach, we have introduced a powerful tool named K-SELinux. This tool enables comprehensive analysis of SELinux policies, encompassing integrity, consistency, completeness, policy queries, policy optimization, and more. Notably, it provides excellent extensibility, enabling the seamless development of additional functions to address evolving needs.

To demonstrate the practicality and effectiveness of our tool, we conducted testing on real-world policies. The tests revealed several crucial issues, including contradictions arising from indirect information flow and incomplete entity restrictions.

Graphical abstract

Keywords

SELinux / access control / semantics / verification

References

[1] Loscocco P, Smalley S. Integrating flexible support for security policies into the Linux operating system. In: Proceedings of FREENIX Track: 2001 USENIX Annual Technical Conference. 2001, 29–42

[2] PeBenito C, Mayer F, MacMillan K. Reference policy for security enhanced Linux. In: Proceedings of 2006 Security Enhanced Linux Symposium. 2006

[3] Hicks B, Rueda S, St . Clair L, Jaeger T, McDaniel P. A logical specification and analysis for SELinux MLS policy. ACM Transactions on Information and System Security (TISSEC), 2010, 13( 3): 26

[4] Sarna-Starosta B, Stoller S D. Policy analysis for security-enhanced Linux. In: Proceedings of 2004 Workshop on Issues in the Theory of Security. 2004, 1–12

[5] Clemente P, Kaba B, Rouzaud-Cornabas J, Alexandre M, Aujay G. SPTrack: Visual analysis of information flows within SELinux policies and attack logs. In: Proceedings of the 8th International Conference on Active Media Technology. 2012, 596–605

[6] Gove R. V3SPA: A visual analysis, exploration, and diffing tool for SELinux and SEAndroid security policies. In: Proceedings of 2016 IEEE Symposium on Visualization for Cyber Security (VizSec). 2016, 1–8

[7] Wang R, Enck W, Reeves D, Zhang X, Ning P, Xu D, Zhou W, Azab A M. EASEAndroid: automatic policy analysis and refinement for security enhanced android via large-scale semi-supervised learning. In: Proceedings of the 24th USENIX Security Symposium. 2015, 351–366

[8] Jaeger T, Sailer R, Zhang X. Analyzing integrity protection in the SELinux example policy. In: Proceedings of the 12th USENIX Security Symposium. 2003

[9] SETools: SELinux policy analysis tools v4. See github.com/OwlCyberDefense/setools?tab=readme-ov-file, accessed 2023-05-03

[10] SELinux wiki. See selinuxproject.org/page/Main_Page, accessed 2023-05-03

[11] Mayer F, MacMillan K, Caplan D. SELinux by Example: Using Security Enhanced Linux (Prentice Hall Open Source Software Development Series). Upper Saddle River: Prentice Hall PTR, 2006

[12] Reshetova E, Bonazzi F, Asokan N. SELint: an SEAndroid policy analysis tool. In Proceedings of the 3rd International Conference on Information Systems Security and Privacy ICISSP. 2016, 47–58

[13] Roșu G, Șerbănută T F . An overview of the K semantic framework. The Journal of Logic and Algebraic Programming, 2010, 79( 6): 397–434

[14] Dasgupta S, Park D, Kasampalis T, Adve V S, Roșu G. A complete formal semantics of x86-64 user-level instruction set architecture. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2019, 1133–1148

[15] Hildenbrandt E, Saxena M, Rodrigues N, Zhu X, Daian P, Guth D, Moore B, Park D, Zhang Y, Stefanescu A, Roșu G. KEVM: a complete formal semantics of the Ethereum virtual machine. In: Proceedings of the 31st IEEE Computer Security Foundations Symposium. 2018, 204–217

[16] Saxena M, Rodrigues N, Chen X, Roșu G. Formal semantics of hybrid automata. See ideals.illinois.edu/items/114383 website, 2020

[17] Smalley S, Craig R. Security enhanced (SE) android: bringing flexible mac to android. In: Proceedings of the 20th Annual Network and Distributed System Security Symposium. 2013, 20–38

[18] Eaman A, Sistany B, Felty A. Review of existing analysis tools for SELinux security policies: challenges and a proposed solution. In: Proceedings of the 7th International Conference on E-Technologies: Embracing the Internet of Things. 2017, 116–135

[19] Blanchette J, Summerfield M. C++ GUI Programming with Qt 4. Upper Saddle River: Prentice Hall PTR, 2006

[20] Marouf S, Shehab M. SEGrapher: visualization-based SELinux policy analysis. In: Proceedings of the 4th Symposium on Configuration Analytics and Automation (SAFECONFIG). 2011, 1–8

[21] Nakamura Y, Sameshima Y, Tabata T. SEEdit: SELinux security policy configuration system with higher level language. In: Proceedings of the 23rd Large Installation System Administration Conference. 2009, 107–117

[22] Chen Y M, Kao Y W. Information flow query and verification for security policy of security-enhanced Linux. In: Proceedings of the 1st International Workshop on Security on Advances in Information and Computer Security. 2006, 389–404

[23] Radhika B S, Kumar N V N, Shyamasundar R K, Vyas P . Consistency analysis and flow secure enforcement of SELinux policies. Computers & Security, 2020, 94: 101816

[24] Zhai G, Guo T, Huang J. SCIATool: a tool for analyzing SELinux policies based on access control spaces, information flows and CPNs. In: Proceedings of the 6th International Conference on Trusted Systems. 2015, 294–309

[25] Zanin G, Mancini L V. Towards a formal model for security policies specification and validation in the SELinux system. In: Proceedings of the 9th ACM Symposium on Access Control Models and Technologies. 2004, 136–145

[26] Bogdanas D, Roșu G . K-java: a complete semantics of java. ACM SIGPLAN Notices, 2015, 50( 1): 445–456

[27] Roșu G. Matching logic. Logical Methods in Computer Science, 2017, 13(4): 1–61

[28] Feynman R, Objectives C. EBNF: a notation to describe syntax. See ics.uci.edu/~pattis/ICS-33/lectures/ebnf.pdf website, 2016

[29] Biba K J. Integrity considerations for secure computer systems. See ojp.gov/ncjrs/virtual-library/abstracts/integrity-considerations-secure-computer-systems website, 1977

[30] Kumar N V N, Shyamasundar R K. Realizing purpose-based privacy policies succinctly via information-flow labels. In: Proceedings of the 4th IEEE International Conference on Big Data and Cloud Computing. 2014, 753–760

[31] Kumar N V N, Shyamasundar R K. A complete generative label model for lattice-based access control models. In: Proceedings of the 15th International Conference on Software Engineering and Formal Methods. 2017, 35–53

[32] Selinuxproject. Refpolicy release 2.20221101. See github.com/SELinuxProject/refpolicy/releases/tag/RELEASE_2_20221101, accessed 2023-05-03

[33] Google. Aosp policy android-8.0.0 r1. See android.googlesource.com/platform/system/sepolicy/+/refs/tags/android-8.0.0_r1, accessed 2023-05-03

[34] Google. Aosp policy android-9.0.0 r1. See android.googlesource.com/platform/system/sepolicy/+/refs/tags/android-9.0.0_r1, accessed 2023-05-03

RIGHTS & PERMISSIONS

Higher Education Press