{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T01:11:14Z","timestamp":1773277874957,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642228629","type":"print"},{"value":"9783642228636","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_24","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T09:47:55Z","timestamp":1312796875000},"page":"325-340","source":"Crossref","is-referenced-by-count":46,"title":["seL4 Enforces Integrity"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Sewell","sequence":"first","affiliation":[]},{"given":"Simon","family":"Winwood","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Gammie","sequence":"additional","affiliation":[]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Andronick, J., Bourke, T., Derrin, P., Elphinstone, K., Greenaway, D., Klein, G., Kolanski, R., Sewell, T., Winwood, S.: Abstract formal specification of the seL4\/ARMv6 API (January 2011), http:\/\/ertos.nicta.com.au\/software\/seL4\/"},{"key":"24_CR2","volume-title":"5th SSV","author":"J. Andronick","year":"2010","unstructured":"Andronick, J., Greenaway, D., Elphinstone, K.: Towards proving security in the presence of large untrusted components. In: Klein, G., Huuck, R., Schlich, B. (eds.) 5th SSV. USENIX, Vancouver (2010)"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Bell, D., LaPadula, L.: Secure computer system: Unified exposition and Multics interpretation. Technical Report MTR-2997, MITRE Corp (March 1976)","DOI":"10.21236\/ADA023588"},{"key":"24_CR4","series-title":"ENTCS","first-page":"25","volume-title":"4th SSV","author":"A. Boyton","year":"2009","unstructured":"Boyton, A.: A verified shared capability model. In: Klein, G., Huuck, R., Schlich, B. (eds.) 4th SSV. ENTCS, vol.\u00a0254, pp. 25\u201344. Elsevier, Amsterdam (2009)"},{"key":"24_CR5","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":"24_CR6","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/365230.365252","volume":"9","author":"J.B. Dennis","year":"1966","unstructured":"Dennis, J.B., Van Horn, E.C.: Programming semantics for multiprogrammed computations. CACM\u00a09, 143\u2013155 (1966)","journal-title":"CACM"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-87873-5_11","volume-title":"Verified Software: Theories, Tools, Experiments","author":"D. Elkaduwe","year":"2008","unstructured":"Elkaduwe, D., Klein, G., Elphinstone, K.: Verified protection model of the seL4 microkernel. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 99\u2013114. Springer, Heidelberg (2008)"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Feiertag, R.J., Neumann, P.G.: The foundations of a provably secure operating system (PSOS). In: AFIPS Conf. Proc., 1979 National Comp. Conf., New York, NY, USA, pp. 329\u2013334 (June 1979)","DOI":"10.1109\/MARK.1979.8817256"},{"key":"24_CR9","doi-asserted-by":"publisher","first-page":"115","DOI":"10.3233\/JCS-2005-13105","volume":"13","author":"J. Guttman","year":"2005","unstructured":"Guttman, J., Herzog, A., Ramsdell, J., Skorupka, C.: Verifying information flow goals in security-enhanced linux. J. Comp. Security\u00a013, 115\u2013134 (2005)","journal-title":"J. Comp. Security"},{"key":"24_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02333-0","volume-title":"Operating System Security","author":"T. Jaeger","year":"2008","unstructured":"Jaeger, T.: Operating System Security. Morgan & Claypool Publishers, San Francisco (2008)"},{"issue":"1","key":"24_CR11","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/s12046-009-0002-4","volume":"34","author":"G. Klein","year":"2009","unstructured":"Klein, G.: Operating system verification\u2014an overview. S\u0101dhan\u0101\u00a034(1), 27\u201369 (2009)","journal-title":"S\u0101dhan\u0101"},{"key":"24_CR12","first-page":"207","volume-title":"22nd SOSP","author":"G. Klein","year":"2009","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, Big Sky (2009)"},{"key":"24_CR13","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":"24_CR14","first-page":"437","volume-title":"5th Princeton Symposium on Information Sciences and Systems","author":"B.W. Lampson","year":"1971","unstructured":"Lampson, B.W.: Protection. In: 5th Princeton Symposium on Information Sciences and Systems, pp. 437\u2013443. Princeton University, Princeton (1971); Reprinted in Operat. Syst. Rev. 8(1), 18\u201324 (1974)"},{"issue":"3","key":"24_CR15","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/322017.322025","volume":"24","author":"R.J. Lipton","year":"1977","unstructured":"Lipton, R.J., Snyder, L.: A linear time algorithm for deciding subject security. J. ACM\u00a024(3), 455\u2013464 (1977)","journal-title":"J. ACM"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-12459-4_7","volume-title":"Formal Aspects in Security and Trust","author":"T. Murray","year":"2010","unstructured":"Murray, T., Lowe, G.: Analysing the information flow properties of object-capability patterns. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol.\u00a05983, pp. 81\u201395. Springer, Heidelberg (2010)"},{"key":"24_CR17","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-1-4419-1539-9_10","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"R.J. Richards","year":"2010","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, Heidelberg (2010)"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Shapiro, J.S., Weber, S.: Verifying the EROS confinement mechanism. In: IEEE Symp. Security & Privacy, Washington, DC, USA, pp. 166\u2013181 (May 2000)","DOI":"10.1109\/SECPRI.2000.848454"},{"issue":"2","key":"24_CR19","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1145\/358818.358825","volume":"23","author":"B.J. Walker","year":"1980","unstructured":"Walker, B.J., Kemmerer, R.A., Popek, G.J.: Specification and verification of the UCLA Unix security kernel. CACM\u00a023(2), 118\u2013131 (1980)","journal-title":"CACM"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,8]],"date-time":"2023-06-08T16:23:23Z","timestamp":1686241403000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}