{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T20:55:41Z","timestamp":1768942541952,"version":"3.49.0"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T00:00:00Z","timestamp":1768867200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T00:00:00Z","timestamp":1768867200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2026,6]]},"DOI":"10.1007\/s11704-024-40495-7","type":"journal-article","created":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T06:58:39Z","timestamp":1768892319000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["K-SELinux: formal analysis and verification of SELinux policies via semantic execution"],"prefix":"10.1007","volume":"20","author":[{"given":"Jinhui","family":"Kang","sequence":"first","affiliation":[]},{"given":"Jianhong","family":"Zhao","sequence":"additional","affiliation":[]},{"given":"Yongwang","family":"Zhao","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,1,20]]},"reference":[{"key":"40495_CR1","first-page":"29","volume-title":"Proceedings of FREENIX Track: 2001 USENIX Annual Technical Conference","author":"P Loscocco","year":"2001","unstructured":"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\u201342"},{"key":"40495_CR2","volume-title":"Proceedings of 2006 Security Enhanced Linux Symposium","author":"C PeBenito","year":"2006","unstructured":"PeBenito C, Mayer F, MacMillan K. Reference policy for security enhanced Linux. In: Proceedings of 2006 Security Enhanced Linux Symposium. 2006"},{"issue":"3","key":"40495_CR3","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1805974.1805982","volume":"13","author":"B Hicks","year":"2010","unstructured":"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","journal-title":"ACM Transactions on Information and System Security (TISSEC)"},{"key":"40495_CR4","first-page":"1","volume-title":"Proceedings of 2004 Workshop on Issues in the Theory of Security","author":"B Sarna-Starosta","year":"2004","unstructured":"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\u201312"},{"key":"40495_CR5","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/978-3-642-35236-2_60","volume-title":"Proceedings of the 8th International Conference on Active Media Technology","author":"P Clemente","year":"2012","unstructured":"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\u2013605"},{"key":"40495_CR6","first-page":"1","volume-title":"Proceedings of 2016 IEEE Symposium on Visualization for Cyber Security (VizSec)","author":"R Gove","year":"2016","unstructured":"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\u20138"},{"key":"40495_CR7","first-page":"351","volume-title":"Proceedings of the 24th USENIX Security Symposium","author":"R Wang","year":"2015","unstructured":"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\u2013366"},{"key":"40495_CR8","volume-title":"Proceedings of the 12th USENIX Security Symposium","author":"T Jaeger","year":"2003","unstructured":"Jaeger T, Sailer R, Zhang X. Analyzing integrity protection in the SELinux example policy. In: Proceedings of the 12th USENIX Security Symposium. 2003"},{"key":"40495_CR9","unstructured":"SETools: SELinux policy analysis tools v4. See github.com\/Owl-CyberDefense\/setools?tab=readme-ov-file, accessed 2023-05-03"},{"key":"40495_CR10","unstructured":"SELinux wiki. See selinuxproject.org\/page\/Main_Page, accessed 2023-05-03"},{"key":"40495_CR11","volume-title":"SELinux by Example: Using Security Enhanced Linux (Prentice Hall Open Source Software Development Series)","author":"F Mayer","year":"2006","unstructured":"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"},{"key":"40495_CR12","first-page":"47","volume-title":"Proceedings of the 3rd International Conference on Information Systems Security and Privacy ICISSP","author":"E Reshetova","year":"2016","unstructured":"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\u201358"},{"issue":"6","key":"40495_CR13","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu G, \u015eerb\u0103nut\u0103 T F. An overview of the K semantic framework. The Journal of Logic and Algebraic Programming, 2010, 79(6): 397\u2013434","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"40495_CR14","doi-asserted-by":"publisher","first-page":"1133","DOI":"10.1145\/3314221.3314601","volume-title":"Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"S Dasgupta","year":"2019","unstructured":"Dasgupta S, Park D, Kasampalis T, Adve V S, Ro\u015fu 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\u20131148"},{"key":"40495_CR15","first-page":"204","volume-title":"Proceedings of the 31st IEEE Computer Security Foundations Symposium","author":"E Hildenbrandt","year":"2018","unstructured":"Hildenbrandt E, Saxena M, Rodrigues N, Zhu X, Daian P, Guth D, Moore B, Park D, Zhang Y, Stefanescu A, Ro\u015fu G. KEVM: a complete formal semantics of the Ethereum virtual machine. In: Proceedings of the 31st IEEE Computer Security Foundations Symposium. 2018, 204\u2013217"},{"key":"40495_CR16","volume-title":"See ideals.illinois.edu\/items\/114383 website","author":"M Saxena","year":"2020","unstructured":"Saxena M, Rodrigues N, Chen X, Ro\u015fu G. Formal semantics of hybrid automata. See ideals.illinois.edu\/items\/114383 website, 2020"},{"key":"40495_CR17","first-page":"20","volume-title":"Proceedings of the 20th Annual Network and Distributed System Security Symposium","author":"S Smalley","year":"2013","unstructured":"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\u201338"},{"key":"40495_CR18","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-319-59041-7_7","volume-title":"Proceedings of the 7th International Conference on E-Technologies: Embracing the Internet of Things","author":"A Eaman","year":"2017","unstructured":"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\u2013135"},{"key":"40495_CR19","volume-title":"C++ GUI Programming with Qt 4","author":"J Blanchette","year":"2006","unstructured":"Blanchette J, Summerfield M. C++ GUI Programming with Qt 4. Upper Saddle River: Prentice Hall PTR, 2006"},{"key":"40495_CR20","first-page":"1","volume-title":"Proceedings of the 4th Symposium on Configuration Analytics and Automation (SAFECONFIG)","author":"S Marouf","year":"2011","unstructured":"Marouf S, Shehab M. SEGrapher: visualization-based SELinux policy analysis. In: Proceedings of the 4th Symposium on Configuration Analytics and Automation (SAFECONFIG). 2011, 1\u20138"},{"key":"40495_CR21","first-page":"107","volume-title":"Proceedings of the 23rd Large Installation System Administration Conference","author":"Y Nakamura","year":"2009","unstructured":"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\u2013117"},{"key":"40495_CR22","first-page":"389","volume-title":"Proceedings of the 1st International Workshop on Security on Advances in Information and Computer Security","author":"Y M Chen","year":"2006","unstructured":"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\u2013404"},{"key":"40495_CR23","doi-asserted-by":"publisher","first-page":"101816","DOI":"10.1016\/j.cose.2020.101816","volume":"94","author":"B S Radhika","year":"2020","unstructured":"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","journal-title":"Computers & Security"},{"key":"40495_CR24","first-page":"294","volume-title":"Proceedings of the 6th International Conference on Trusted Systems","author":"G Zhai","year":"2015","unstructured":"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\u2013309"},{"key":"40495_CR25","first-page":"136","volume-title":"Proceedings of the 9th ACM Symposium on Access Control Models and Technologies","author":"G Zanin","year":"2004","unstructured":"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\u2013145"},{"issue":"1","key":"40495_CR26","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1145\/2775051.2676982","volume":"50","author":"D Bogdanas","year":"2015","unstructured":"Bogdanas D, Ro\u015fu G. K-java: a complete semantics of java. ACM SIGPLAN Notices, 2015, 50(1): 445\u2013456","journal-title":"ACM SIGPLAN Notices"},{"issue":"4","key":"40495_CR27","first-page":"1","volume":"13","author":"G Ro\u015fu","year":"2017","unstructured":"Ro\u015fu G. Matching logic. Logical Methods in Computer Science, 2017, 13(4): 1\u201361","journal-title":"Logical Methods in Computer Science"},{"key":"40495_CR28","volume-title":"EBNF: a notation to describe syntax","author":"R Feynman","year":"2016","unstructured":"Feynman R, Objectives C. EBNF: a notation to describe syntax. See ics.uci.edu\/~pattis\/ICS-33\/lectures\/ebnf.pdf website, 2016"},{"key":"40495_CR29","volume-title":"Integrity considerations for secure computer systems","author":"K J Biba","year":"1977","unstructured":"Biba K J. Integrity considerations for secure computer systems. See ojp.gov\/ncjrs\/virtual-library\/abstracts\/integrity-considerations-secure-computer-systems website, 1977"},{"key":"40495_CR30","first-page":"753","volume-title":"Proceedings of the 4th IEEE International Conference on Big Data and Cloud Computing","author":"N V N Kumar","year":"2014","unstructured":"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\u2013760"},{"key":"40495_CR31","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-66197-1_3","volume-title":"Proceedings of the 15th International Conference on Software Engineering and Formal Methods","author":"N V N Kumar","year":"2017","unstructured":"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\u201353"},{"key":"40495_CR32","unstructured":"Selinuxproject. Refpolicy release 2.20221101. See github.com\/SELinuxProject\/refpolicy\/releases\/tag\/RELEASE_2_20221101, accessed 2023-05-03"},{"key":"40495_CR33","unstructured":"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"},{"key":"40495_CR34","unstructured":"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"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-024-40495-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11704-024-40495-7","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-024-40495-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T06:58:43Z","timestamp":1768892323000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11704-024-40495-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,20]]},"references-count":34,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["40495"],"URL":"https:\/\/doi.org\/10.1007\/s11704-024-40495-7","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,20]]},"assertion":[{"value":"15 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 December 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 January 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare that they have no competing interests or financial conflicts to disclose.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"2006201"}}