{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:25:54Z","timestamp":1766136354892},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642353079"},{"type":"electronic","value":"9783642353086"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35308-6_12","type":"book-chapter","created":{"date-parts":[[2012,11,8]],"date-time":"2012-11-08T03:20:18Z","timestamp":1352344818000},"page":"126-142","source":"Crossref","is-referenced-by-count":45,"title":["Noninterference for Operating System Kernels"],"prefix":"10.1007","author":[{"given":"Toby","family":"Murray","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Matichuk","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"Brassil","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Gammie","sequence":"additional","affiliation":[]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-540-27864-1_10","volume-title":"Static Analysis","author":"T. Amtoft","year":"2004","unstructured":"Amtoft, T., Banerjee, A.: Information Flow Analysis in Logical Form. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 100\u2013115. Springer, Heidelberg (2004)"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Banerjee, A.: Verification condition generation for conditional information flow. In: FMSE 2007, pp. 2\u201311. ACM (2007)","DOI":"10.1145\/1314436.1314438"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-21437-0_19","volume-title":"FM 2011: Formal Methods","author":"G. Barthe","year":"2011","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Luna, C.: Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 231\u2013245. Springer, Heidelberg (2011)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL 2004, pp. 14\u201325. ACM (2004)","DOI":"10.1145\/982962.964003"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-22863-6_6","volume-title":"Interactive Theorem Proving","author":"L. Beringer","year":"2011","unstructured":"Beringer, L.: Relational Decomposition. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 39\u201354. Springer, Heidelberg (2011)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure Microkernels, State Monads and Scalable Refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511663079"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Goguen, J., Meseguer, J.: Security policies and security models. In: IEEE Symp. Security & Privacy, Oakland, California, USA, pp. 11\u201320. IEEE (April 1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Greve, D.A.: Information security modeling and analysis. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 249\u2013300. Springer (2010)","DOI":"10.1007\/978-1-4419-1539-9_9"},{"key":"12_CR10","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. Trans. Softw. Engin.\u00a013, 141\u2013150 (1987)","journal-title":"Trans. Softw. Engin."},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: 22nd SOSP, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"12_CR12","unstructured":"Klein, G., Murray, T., Gammie, P., Sewell, T., Winwood, S.: Provable security: How feasible is it? In: 13th HotOS, Napa, CA, USA, pp. 28\u201332. USENIX (May 2011)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-33826-7_23","volume-title":"Software Engineering and Formal Methods","author":"D. Matichuk","year":"2012","unstructured":"Matichuk, D., Murray, T.: Extensible Specifications for Automatic Re-use of Specifications and Proofs. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 333\u2013341. Springer, Heidelberg (2012)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Richards, R.J.: Modeling and security analysis of a commercial real-time operating system kernel. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 301\u2013322. Springer (2010)","DOI":"10.1007\/978-1-4419-1539-9_10"},{"key":"12_CR16","unstructured":"Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical Report CSL-92-02, SRI International (December 1992)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-642-22863-6_24","volume-title":"Interactive Theorem Proving","author":"T. Sewell","year":"2011","unstructured":"Sewell, T., Winwood, S., Gammie, P., Murray, T., Andronick, J., Klein, G.: seL4 Enforces Integrity. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 325\u2013340. Springer, Heidelberg (2011)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T. Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure Information Flow as a Safety Problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 352\u2013367. Springer, Heidelberg (2005)"},{"key":"12_CR19","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)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"van der Meyden, R., Zhang, C.: Information flow in systems with schedulers. In: 21st CSF, pp. 301\u2013312. IEEE (June 2008)","DOI":"10.1109\/CSF.2008.13"},{"key":"12_CR21","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)"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35308-6_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T13:13:44Z","timestamp":1620134024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35308-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642353079","9783642353086"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35308-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}