{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T12:54:09Z","timestamp":1769000049698,"version":"3.49.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2010,7,1]],"date-time":"2010-07-01T00:00:00Z","timestamp":1277942400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CCF-0524132 CNS-0627551"],"award-info":[{"award-number":["CCF-0524132 CNS-0627551"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-0524132 CNS-0627551"],"award-info":[{"award-number":["CCF-0524132 CNS-0627551"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Inf. Syst. Secur."],"published-print":{"date-parts":[[2010,7]]},"abstract":"<jats:p>The SELinux mandatory access control (MAC) policy has recently added a multilevel security (MLS) model which is able to express a fine granularity of control over a subject's access rights. The problem is that the richness of the SELinux MLS model makes it impractical to manually evaluate that a given policy meets certain specific properties. To address this issue, we have modeled the SELinux MLS model, using a logical specification and implemented that specification in the Prolog language. Furthermore, we have developed some analyses for testing information flow properties of a given policy as well as an algorithm to determine whether one policy is compliant with another. We have implemented these analyses in Prolog and compiled our implementation into a tool for SELinux MLS policy analysis, called PALMS. Using PALMS, we verified some important properties of the SELinux MLS reference policy, namely that it satisfies the simple security condition and \u22c6-property defined by Bell and LaPadula. We also evaluated whether the policy associated to a given application is compliant with the policy of the SELinux system in which it would be deployed.<\/jats:p>","DOI":"10.1145\/1805974.1805982","type":"journal-article","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T09:15:22Z","timestamp":1280740522000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["A logical specification and analysis for SELinux MLS policy"],"prefix":"10.1145","volume":"13","author":[{"given":"Boniface","family":"Hicks","sequence":"first","affiliation":[{"name":"St. Vincent College, LaTrobe, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandra","family":"Rueda","sequence":"additional","affiliation":[{"name":"The Pennsylvania State University, University Park, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luke","family":"St.Clair","sequence":"additional","affiliation":[{"name":"The Pennsylvania State University, University Park, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Trent","family":"Jaeger","sequence":"additional","affiliation":[{"name":"The Pennsylvania State University, University Park, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"McDaniel","sequence":"additional","affiliation":[{"name":"The Pennsylvania State University, University Park, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,7,30]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Bell D. and Lapadula L. 1973. Secure computer systems: Mathematical foundations and model. Tech. rep. MITRE."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/373256.373261"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/863632.883503"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/882493.884372"},{"key":"e_1_2_1_5_1","volume-title":"XSB: Logic programming and deductive database system for Unix and Windows","author":"Computer Science Department of the Stony Brook University.","year":"2009","unstructured":"Computer Science Department of the Stony Brook University. 2009. XSB: Logic programming and deductive database system for Unix and Windows. http:\/\/xsb.sourceforge.net."},{"key":"e_1_2_1_6_1","volume-title":"Managing security on DG\/UX system. Manual 093-701139-04","author":"Data General Corporation","unstructured":"Data General Corporation. 1996. Managing security on DG\/UX system. Manual 093-701139-04. Data General Corporation, Westboro, MA."},{"key":"e_1_2_1_7_1","volume-title":"SEBSD: Port of SELinux FLASK and type enforcement to TrustedBSD","author":"Free BSD","year":"2010","unstructured":"FreeBSD. 2010. SEBSD: Port of SELinux FLASK and type enforcement to TrustedBSD. http:\/\/www.trustedbsd.org\/sebsd.html."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1066473.1066478"},{"key":"e_1_2_1_9_1","volume-title":"Trusted Computer Solutions","author":"Hanson C.","unstructured":"Hanson, C. 2006. SELinux and MLS: putting the pieces together. Tech. rep. NAI-02-007, Trusted Computer Solutions, Inc."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSAC.2006.30"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1364385.1364401"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/507711.507713"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/937527.937528"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1268476.1268480"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/373256.373280"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 21st National Information Systems Security Conference.","author":"Loscocco P.","unstructured":"Loscocco, P., Smalley, S., Muckelbauer, P., Tayler, R., Turner, J., and Farrel, J. 1998. The inevitability of failure: The awed assumptions of security modern computing environments. In Proceedings of the 21st National Information Systems Security Conference."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Myers A. C. 1999. Mostly-static decentralized information ow control. Tech. rep. MIT\/LCS\/TR-783.","DOI":"10.5555\/888669"},{"key":"e_1_2_1_18_1","unstructured":"National Security Agency. 2009. Security-enhanced Linux. http:\/\/www.nsa.gov\/selinux."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the Workshop on Issues in the Theory of Security. ACM","author":"Sarna-Starosta B.","unstructured":"Sarna-Starosta, B. and Stoller, S. D. 2004. Policy analysis for security-enhanced Linux. In Proceedings of the Workshop on Issues in the Theory of Security. ACM, New York, 1--12."},{"key":"e_1_2_1_21_1","volume-title":"Configuring the SELinux policy. Tech. rep. NAI-02-007","author":"Smalley S.","unstructured":"Smalley, S. 2002. Configuring the SELinux policy. Tech. rep. NAI-02-007, National Security Agency."},{"key":"e_1_2_1_22_1","volume-title":"Configuring the SELinux policy. Revision Tech. rep. NAI-02-007","author":"Smalley S.","year":"2002","unstructured":"Smalley, S. 2005. Configuring the SELinux policy. Revision Tech. rep. NAI-02-007 (2002), National Security Agency."},{"key":"e_1_2_1_23_1","unstructured":"Smalley S. Vance C. and Salamon W. 2001. Implementing SELinux as a Linux security module. Tech. rep. 01-043 NAI Labs."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1251421.1251432"},{"key":"e_1_2_1_25_1","unstructured":"Sun. 2010. Solaris trusted extensions. http:\/\/www.sun.com."},{"key":"e_1_2_1_26_1","unstructured":"Sun. 2009. Trusted solaris operating environment\u2014a technical overview. http:\/\/www.sun.com."},{"key":"e_1_2_1_27_1","unstructured":"Tresys. 2010. Setools\u2014policy analysis tools for SELinux. http:\/\/oss.tresys.com\/projects\/setools."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 3rd Annual Security-Enhanced Linux Symposium. ACM","author":"Vance C.","unstructured":"Vance, C., Miller, T., and Dekelbaum, R. 2007. Security-enhanced Darwin: Porting SELinux to Mac os x. In Proceedings of the 3rd Annual Security-Enhanced Linux Symposium. ACM, New York."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/990036.990059"}],"container-title":["ACM Transactions on Information and System Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1805974.1805982","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1805974.1805982","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1805974.1805982","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:23:32Z","timestamp":1763457812000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1805974.1805982"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,7]]}},"alternative-id":["10.1145\/1805974.1805982"],"URL":"https:\/\/doi.org\/10.1145\/1805974.1805982","relation":{},"ISSN":["1094-9224","1557-7406"],"issn-type":[{"value":"1094-9224","type":"print"},{"value":"1557-7406","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,7]]},"assertion":[{"value":"2008-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-02-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-07-30","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}