{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T13:10:08Z","timestamp":1746364208972,"version":"3.40.4"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105055"},{"type":"electronic","value":"9783319105062"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10506-2_17","type":"book-chapter","created":{"date-parts":[[2014,9,3]],"date-time":"2014-09-03T02:41:50Z","timestamp":1409712110000},"page":"246-261","source":"Crossref","is-referenced-by-count":5,"title":["On Two Models of Noninterference: Rushby and Greve, Wilding, and Vanfleet"],"prefix":"10.1007","author":[{"given":"Adrian Garcia","family":"Ramirez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Schmaltz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Freek","family":"Verbeek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Langenstein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Blasum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Hardin, D.S. (ed.): Design and Verification of Microprocessor Systems for High-Assurance Applications (2010)","DOI":"10.1007\/978-1-4419-1539-9"},{"key":"17_CR2","unstructured":"Alves-Foss, J., Taylor, C.: An analysis of the GWV security policy. In: Fifth International Workshop on ACL2 Prover and its Applications (2004)"},{"key":"17_CR3","unstructured":"Brygier, J., Fuchsen, R., Blasum, H.: PikeOS: Safe and secure virtualization in a separation microkernel. Technical report, SYSGO (2009)"},{"key":"17_CR4","unstructured":"Eggert, S., van der Meyden, R., Schnoor, H., Wilke, T.: Complexity and unwinding for intransitive noninterference. CoRR abs\/1308.1204 (2013)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"17_CR6","unstructured":"Greve, D., Wilding, M., Richards, R., Vanfleet, W.M.: Formalizing security policies for dynamic and distributed systems (September 2004) (unpublished), http:\/\/hokiepokie.org\/docs\/sstc05.pdf"},{"key":"17_CR7","unstructured":"Greve, D., Wilding, M., Vanfleet, W.M.: A separation kernel formal security policy. In: Fourth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2003 (July 2003)"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-1-4419-1539-9_9","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"D. Greve","year":"2010","unstructured":"Greve, D.: Information security modeling and analysis. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 249\u2013299. Springer, US (2010), http:\/\/dx.doi.org\/10.1007\/978-1-4419-1539-9_9"},{"issue":"2","key":"17_CR9","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1109\/TSE.1987.226478","volume":"13","author":"J.T. Haigh","year":"1987","unstructured":"Haigh, J.T., Young, W.D.: Extending the noninterference version of mls for sat. IEEE Trans. Software Eng.\u00a013(2), 141\u2013150 (1987)","journal-title":"IEEE Trans. Software Eng."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Hardin, D.S. (ed.): Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer (2010)","DOI":"10.1007\/978-1-4419-1539-9"},{"key":"17_CR11","unstructured":"Kaiser, R., Wagner, S.: Evolution of the PikeOS microkernel. In: First International Workshop on Microkernels for Embedded Systems, p. 50 (2007)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Krohn, M., Tromer, E.: Noninterference for a practical DIFC-based operating system. In: IEEE Symp. Security & Privacy, pp. 61\u201376 (2009)","DOI":"10.1109\/SP.2009.23"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-540-74835-9_16","volume-title":"Computer Security \u2013 ESORICS 2007","author":"R. Meyden van der","year":"2007","unstructured":"van der Meyden, R.: What, indeed, is intransitive noninterference? In: Biskup, J., L\u00f3pez, J. (eds.) ESORICS 2007. LNCS, vol.\u00a04734, pp. 235\u2013250. Springer, Heidelberg (2007)"},{"issue":"47","key":"17_CR14","doi-asserted-by":"publisher","first-page":"4123","DOI":"10.1016\/j.tcs.2010.08.013","volume":"411","author":"R. Meyden van der","year":"2010","unstructured":"van der Meyden, R., Zhang, C.: A comparison of semantic models for noninterference. Theor. Comput. Sci.\u00a0411(47), 4123\u20134147 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-540-30108-0_14","volume-title":"Computer Security \u2013 ESORICS 2004","author":"D. Oheimb von","year":"2004","unstructured":"von Oheimb, D.: Information flow control revisited: Noninfluence = Noninterference + Nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol.\u00a03193, pp. 225\u2013243. Springer, Heidelberg (2004)"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Richards, R.J.: Modeling and security analysis of a commercial real-time operating system kernel. In: Hardin (ed.) [10], pp. 301\u2013322","DOI":"10.1007\/978-1-4419-1539-9_10"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1067627.806586","volume":"15","author":"J. Rushby","year":"1981","unstructured":"Rushby, J.: Design and verification of secure systems. ACM SIGOPS Operating Systems Review\u00a015, 12\u201321 (1981)","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"17_CR19","unstructured":"Rushby, J.: Noninterference, transitivity and channel-control security policies. Tech. rep., Computer Science Laboratory, SRI International (1992)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Ryan, P.Y.A., Schneider, S.A.: Process algebra and non-interference. Journal of Computer Security, 214\u2013227 (1999)","DOI":"10.1109\/CSFW.1999.779775"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/10722599_2","volume-title":"Computer Security - ESORICS 2000","author":"G. Schellhorn","year":"2000","unstructured":"Schellhorn, G., Reif, W., Schairer, A., Karger, P., Austel, V., Toll, D.: Verification of a formal security model for multiapplicative smart cards. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol.\u00a01895, pp. 17\u201336. Springer, Heidelberg (2000)"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Wilding, M., Greve, D., Richards, R., Hardin, D.: Formal verification of partition management for the AAMP7G microprocessor. In: Hardin (ed.) [10], pp. 175\u2013191","DOI":"10.1007\/978-1-4419-1539-9_6"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10506-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T12:51:39Z","timestamp":1746363099000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10506-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319105055","9783319105062"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10506-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}