{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:06:07Z","timestamp":1750309567584,"version":"3.41.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2024,10,7]],"date-time":"2024-10-07T00:00:00Z","timestamp":1728259200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"MUR National Recovery and Resilience Plan funded by the European Union - NextGenerationEU","award":["PE00000014, P2022EPPHM"],"award-info":[{"award-number":["PE00000014, P2022EPPHM"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Priv. Secur."],"published-print":{"date-parts":[[2024,11,30]]},"abstract":"<jats:p>Security Enhanced Linux (SELinux) is a security architecture for Linux implementing Mandatory Access Control. It has been used in numerous security-critical contexts ranging from servers to mobile devices. However, its application is challenging as SELinux security policies are difficult to write, understand, and maintain. Recently, the intermediate language CIL was introduced to foster the development of high-level policy languages and to write structured configurations. Despite CIL\u2019s high level features, CIL configurations are hard to understand as different constructs interact in non-trivial ways. Moreover, there is no mechanism to ensure that a given configuration obeys desired information flow policies. To remedy this, we enrich CIL with a formal semantics, and we propose IFCIL, a backward compatible extension of CIL for specifying fine-grained information flow requirements. Using IFCIL, administrators can express confidentiality, integrity, and non-interference properties. We also provide a tool to statically verify these requirements and we experimentally assess it on ten real-world policies.<\/jats:p>","DOI":"10.1145\/3690636","type":"journal-article","created":{"date-parts":[[2024,8,29]],"date-time":"2024-08-29T09:44:15Z","timestamp":1724924655000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Specifying and Verifying Information Flow Control in SELinux Configurations"],"prefix":"10.1145","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1288-9623","authenticated-orcid":false,"given":"Lorenzo","family":"Ceragioli","sequence":"first","affiliation":[{"name":"IMT School for Advanced Studies Lucca, Lucca, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0351-9169","authenticated-orcid":false,"given":"Letterio","family":"Galletta","sequence":"additional","affiliation":[{"name":"IMT School for Advanced Studies Lucca, Lucca Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8070-4838","authenticated-orcid":false,"given":"Pierpaolo","family":"Degano","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Pisa, Pisa Italy and IMT School for Advanced Studies Lucca, Lucca Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2952-939X","authenticated-orcid":false,"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2024,10,7]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706349"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-15791"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.29"},{"key":"e_1_3_3_5_2","volume-title":"Cascade: A High Level Language for SELinux Policy","author":"Burgener Daniel","year":"2024","unstructured":"Daniel Burgener. 2024. Cascade: A High Level Language for SELinux Policy. https:\/\/github.com\/dburgener\/cascade"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.10"},{"key":"e_1_3_3_7_2","volume-title":"[PATCH 1\/3] libsepol\/cil: Make Name Resolution in Macros Work as Documented","author":"Carter James","year":"2024","unstructured":"James Carter. 2024. [PATCH 1\/3] libsepol\/cil: Make Name Resolution in Macros Work as Documented. https:\/\/lore.kernel.org\/selinux\/20210507173744.198858-1-jwcart2@gmail.com\/"},{"key":"e_1_3_3_8_2","volume-title":"Bug (?) Report for Secilc and CIL Semantics: Some Unexpected Behaviours","author":"Ceragioli Lorenzo","year":"2024","unstructured":"Lorenzo Ceragioli. 2024. Bug (?) Report for Secilc and CIL Semantics: Some Unexpected Behaviours. https:\/\/lore.kernel.org\/selinux\/5ca2e18c-6395-a0af-fdee-b0ac5f1de714@phd.unipi.it\/"},{"key":"e_1_3_3_9_2","volume-title":"[Bug Report?] Other Unexpected Behaviours in Secilc and CIL Semantics","author":"Ceragioli Lorenzo","year":"2024","unstructured":"Lorenzo Ceragioli. 2024. [Bug Report?] Other Unexpected Behaviours in Secilc and CIL Semantics. https:\/\/lore.kernel.org\/selinux\/86d254dd-fd82-e25c-915b-16615b341457@phd.unipi.it\/"},{"key":"e_1_3_3_10_2","volume-title":"SELinux CIL Semantics","author":"Ceragioli Lorenzo","year":"2024","unstructured":"Lorenzo Ceragioli. 2024. SELinux CIL Semantics. https:\/\/github.com\/lceragioli\/SELinuxCILSemantics"},{"key":"e_1_3_3_11_2","volume-title":"SELinux IFCIL Tool","author":"Ceragioli Lorenzo","year":"2024","unstructured":"Lorenzo Ceragioli. 2024. SELinux IFCIL Tool. https:\/\/github.com\/lceragioli\/SELinuxIFCIL"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919690"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1987.10001"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_3_3_16_2","volume-title":"BigMAC: Analysis Tool to Introspect and Query Android Security Policies","author":"Cybersecurity Florida Institute for","year":"2024","unstructured":"Florida Institute for Cybersecurity. 2024. BigMAC: Analysis Tool to Introspect and Query Android Security Policies."},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-914-5"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"volume-title":"Android Open Source Project","key":"e_1_3_3_19_2","unstructured":"Google. 2024. Android Open Source Project. https:\/\/source.android.com\/"},{"volume-title":"sepolicy","year":"2024","key":"e_1_3_3_20_2","unstructured":"Google. 2024. sepolicy. https:\/\/android.googlesource.com\/platform\/system\/sepolicy\/"},{"key":"e_1_3_3_21_2","volume-title":"openWRT SELinux Policy (Commit aa59f95 on 3 Dec 2021)","author":"Grift Dominick","year":"2024","unstructured":"Dominick Grift. 2024. openWRT SELinux Policy (Commit aa59f95 on 3 Dec 2021). https:\/\/git.defensec.nl\/?p=selinux-policy.git;a=summary"},{"key":"e_1_3_3_22_2","volume-title":"SELinux Example Policy Cilpolicy (Commit 562a8a2 on 8 Sep 2015)","author":"Grift Dominick","year":"2024","unstructured":"Dominick Grift. 2024. SELinux Example Policy Cilpolicy (Commit 562a8a2 on 8 Sep 2015). https:\/\/web.archive.org\/web\/20201027211840\/https:\/\/github.com\/doverride\/cilpolicy"},{"key":"e_1_3_3_23_2","volume-title":"SELinux Example Policy dspp5 (Commit cf4dd60 on 16 Dec 2021)","author":"Grift Dominick","year":"2024","unstructured":"Dominick Grift. 2024. SELinux Example Policy dspp5 (Commit cf4dd60 on 16 Dec 2021). https:\/\/git.defensec.nl\/?p=dssp5.git;a=summary"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0052-x"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2005-13105"},{"key":"e_1_3_3_26_2","first-page":"271","volume-title":"29th USENIX Security Symposium (USENIX Security\u201920)","author":"Hernandez Grant","year":"2020","unstructured":"Grant Hernandez, Dave (Jing) Tian, Anurag Swarnim Yadav, Byron J. Williams, and Kevin R. B. Butler. 2020. BigMAC: Fine-grained policy analysis of Android firmware. In 29th USENIX Security Symposium (USENIX Security\u201920). USENIX Association, 271\u2013287. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/hernandez"},{"key":"e_1_3_3_27_2","volume-title":"Lobster: A Domain Specific Language for SELinux Policies","author":"Hurd Joe","year":"2008","unstructured":"Joe Hurd, Magnus Carlsson, Brett Letner, and Peter White. 2008. Lobster: A Domain Specific Language for SELinux Policies. Technical Report. Galois, Inc."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274709"},{"key":"e_1_3_3_29_2","volume-title":"Proceedings of the 12th USENIX Security Symposium, Washington, D.C., USA, 2003","author":"Jaeger Trent","year":"2003","unstructured":"Trent Jaeger, Reiner Sailer, and Xiaolan Zhang. 2003. Analyzing integrity protection in the SELinux example policy. In Proceedings of the 12th USENIX Security Symposium, Washington, D.C., USA, 2003. USENIX Association."},{"key":"e_1_3_3_30_2","first-page":"2579","volume-title":"30th USENIX Security Symposium (USENIX Security\u201921)","author":"Lee Yu-Tsung","year":"2021","unstructured":"Yu-Tsung Lee, William Enck, Haining Chen, Hayawardh Vijayakumar, Ninghui Li, Zhiyun Qian, Daimeng Wang, Giuseppe Petracca, and Trent Jaeger. 2021. PolyScope: Multi-policy access control analysis to compute authorized attack operations in Android systems. In 30th USENIX Security Symposium (USENIX Security\u201921). USENIX Association, 2579\u20132596. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/lee-yu-tsung"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-15805"},{"key":"e_1_3_3_32_2","volume-title":"Specifying and Verifying Information Flow Control in SELinux Configurations \u2013 Full Version with Proofs","author":"Galletta Pierpaolo Degano, David Basin, Lorenzo Ceragioli, and Letterio","year":"2024","unstructured":"Pierpaolo Degano, David Basin, Lorenzo Ceragioli, and Letterio Galletta. 2024. Specifying and Verifying Information Flow Control in SELinux Configurations \u2013 Full Version with Proofs. https:\/\/github.com\/lceragioli\/SELinuxIFCIL\/blob\/main\/paper.pdf"},{"key":"e_1_3_3_33_2","first-page":"330","volume-title":"Proceedings of the 6th Static Analysis Symposium, LNCS,1694","author":"M\u00fcller-Olm Markus","year":"1999","unstructured":"Markus M\u00fcller-Olm, David A. Schmidt, and Bernhard Steffen. 1999. Model-checking: A tutorial introduction. In Proceedings of the 6th Static Analysis Symposium, LNCS,1694, A. Cortesi and G. Fil\u00e9 (Eds.). Springer, 330\u2013354."},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292561"},{"key":"e_1_3_3_35_2","first-page":"201","article-title":"SELinux security policy configuration system with higher level language","volume":"18","author":"Nakamura Yuichi","year":"2010","unstructured":"Yuichi Nakamura, Yoshiki Sameshima, and Toshihiro Yamauchi. 2010. SELinux security policy configuration system with higher level language. J. Inf. Process. 18 (2010), 201\u2013212.","journal-title":"J. Inf. Process."},{"key":"e_1_3_3_36_2","unstructured":"OpenWRT. 2024. https:\/\/openwrt.org"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3408987"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"e_1_3_3_39_2","volume-title":"SELinux Project","author":"Project SELinux","year":"2024","unstructured":"SELinux Project. 2024. SELinux Project. https:\/\/selinuxproject.org"},{"key":"e_1_3_3_40_2","volume-title":"The SELinux Notebook - CIL Reference Guide (Commit 2b3b4ee on 6 Jul 2020)","author":"Project SELinux","year":"2024","unstructured":"SELinux Project. 2024. The SELinux Notebook - CIL Reference Guide (Commit 2b3b4ee on 6 Jul 2020). https:\/\/github.com\/SELinuxProject\/selinux-notebook\/blob\/main\/src\/notebook-examples\/selinux-policy\/cil\/CIL_Reference_Guide.pdf"},{"key":"e_1_3_3_41_2","volume-title":"The SELinux Notebook - Kernel Policy Language","author":"Project SELinux","year":"2024","unstructured":"SELinux Project. 2024. The SELinux Notebook - Kernel Policy Language."},{"key":"e_1_3_3_42_2","volume-title":"The SELinux Notebook - MLS Statements","author":"Project SELinux","year":"2024","unstructured":"SELinux Project. 2024. The SELinux Notebook - MLS Statements. https:\/\/github.com\/SELinuxProject\/selinux-notebook\/blob\/main\/src\/mls_statements.md#mls-statements"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2020.101816"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.5220\/0006126600470058"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_3_46_2","first-page":"1","volume-title":"Proceedings of the 2004 Workshop on Issues in the Theory of Security","author":"Sarna-Starosta Beata","year":"2004","unstructured":"Beata Sarna-Starosta and Scott D. Stoller. 2004. Policy analysis for security-enhanced Linux. In Proceedings of the 2004 Workshop on Issues in the Theory of Security. 1\u201312."},{"key":"e_1_3_3_47_2","volume-title":"Proceedings of the Network and Distributed System Security Symposium, NDSS 2006, San Diego, California, USA","author":"Shankar Umesh","year":"2006","unstructured":"Umesh Shankar, Trent Jaeger, and Reiner Sailer. 2006. Toward automated information-flow integrity verification for security-critical applications. In Proceedings of the Network and Distributed System Security Symposium, NDSS 2006, San Diego, California, USA. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss2006\/toward-automated-information-flow-integrity-verification-security-critical-applications\/"},{"key":"e_1_3_3_48_2","volume-title":"Add Support for a Source Policy HLL","author":"Smalley Stephen","year":"2018","unstructured":"Stephen Smalley. 2018. Add Support for a Source Policy HLL. https:\/\/github.com\/SELinuxProject\/selinux\/issues\/54"},{"key":"e_1_3_3_49_2","volume-title":"20th Annual Network and Distributed System Security Symposium, 2013, San Diego, California, USA, February 24\u201327, 2013","author":"Smalley Stephen","year":"2013","unstructured":"Stephen Smalley and Robert Craig. 2013. Security Enhanced (SE) Android: Bringing Flexible MAC to Android. In 20th Annual Network and Distributed System Security Symposium, 2013, San Diego, California, USA, February 24\u201327, 2013. The Internet Society."},{"key":"e_1_3_3_50_2","volume-title":"Increasing Performance and Granularity in Rolebased Access Control Systems","author":"Spengler Bradley","year":"2004","unstructured":"Bradley Spengler. 2004. Increasing Performance and Granularity in Rolebased Access Control Systems. http:\/\/grsecurity.net\/researchpaper.pdf"},{"key":"e_1_3_3_51_2","volume-title":"Information Flow Analysis in Security Enhanced Linux","author":"Thomsen Dan","year":"2004","unstructured":"Dan Thomsen. 2004. Information Flow Analysis in Security Enhanced Linux. CERIAS Security Seminar at Purdue University."},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1587\/transinf.E92.D.2196"}],"container-title":["ACM Transactions on Privacy and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3690636","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3690636","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:19:10Z","timestamp":1750295950000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3690636"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,7]]},"references-count":51,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,11,30]]}},"alternative-id":["10.1145\/3690636"],"URL":"https:\/\/doi.org\/10.1145\/3690636","relation":{},"ISSN":["2471-2566","2471-2574"],"issn-type":[{"type":"print","value":"2471-2566"},{"type":"electronic","value":"2471-2574"}],"subject":[],"published":{"date-parts":[[2024,10,7]]},"assertion":[{"value":"2023-10-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-07-28","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-07","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}