{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:46:58Z","timestamp":1750308418661,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T00:00:00Z","timestamp":1598832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2020,8,31]]},"abstract":"<jats:p>This paper presents an analysis of noninterference specifications used in a range of formally verified systems. The main findings are that these systems use distinct specifications and that they often employ small variations, both complicating their security implications. We categorize these specifications and discuss their trade-offs for reasoning about information flows in systems.<\/jats:p>","DOI":"10.1145\/3421473.3421478","type":"journal-article","created":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T13:31:19Z","timestamp":1598880679000},"page":"31-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Noninterference specifications for secure systems"],"prefix":"10.1145","volume":"54","author":[{"given":"Luke","family":"Nelson","sequence":"first","affiliation":[{"name":"University of Washington"}]},{"given":"James","family":"Bornholt","sequence":"additional","affiliation":[{"name":"University of Washington and University of Texas at Austin"}]},{"given":"Arvind","family":"Krishnamurthy","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Xi","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Washington"}]}],"member":"320","published-online":{"date-parts":[[2020,8,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 8th National Computer Security Conference","author":"Boebert W. E.","year":"1985","unstructured":"W. E. Boebert and R.Y. Kain . Apractical alternative to hierarchical integrity policies . In Proceedings of the 8th National Computer Security Conference , Gaithersburg, MD, Sept.-- Oct. 1985 . W. E. Boebert and R.Y. Kain. Apractical alternative to hierarchical integrity policies. In Proceedings of the 8th National Computer Security Conference, Gaithersburg, MD, Sept.--Oct. 1985."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908100"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516702"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.049"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1987.226478"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/2685048.2685062"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/3291168.3291192"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/362375.362389"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040319"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_12"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2018.00010"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/269005.266669"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_2_1_24_1","volume-title":"Is- abelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2016","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Is- abelle\/HOL: A Proof Assistant for Higher-Order Logic . Springer-Verlag , Feb. 2016 . T. Nipkow, L. C. Paulson, and M. Wenzel. Is- abelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, Feb. 2016."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594338"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/794199.795122"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/800216.806586"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/3291168.3291190"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364557"},{"key":"e_1_2_1_34_1","volume-title":"Jan.","author":"Development Team The Coq","year":"2019","unstructured":"The Coq Development Team . The Coq Proof As- sistant, version 8.9.0 , Jan. 2019 . URL https: \/\/doi.org\/10.5281\/zenodo.2554024. 10.5281\/zenodo.2554024 The Coq Development Team. The Coq Proof As- sistant, version 8.9.0, Jan. 2019. URL https: \/\/doi.org\/10.5281\/zenodo.2554024."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.6"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2393847.2393869"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.08.013"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30108-0_14"}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3421473.3421478","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3421473.3421478","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:21Z","timestamp":1750268961000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3421473.3421478"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,31]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,8,31]]}},"alternative-id":["10.1145\/3421473.3421478"],"URL":"https:\/\/doi.org\/10.1145\/3421473.3421478","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2020,8,31]]},"assertion":[{"value":"2020-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}