{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:55:28Z","timestamp":1725562528149},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642150562"},{"type":"electronic","value":"9783642150579"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15057-9_6","type":"book-chapter","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T07:01:15Z","timestamp":1281510075000},"page":"86-96","source":"Crossref","is-referenced-by-count":4,"title":["The L4.verified Project \u2014 Next Steps"],"prefix":"10.1007","author":[{"given":"Gerwin","family":"Klein","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Boettcher, C., DeLong, R., Rushby, J., Sifre, W.: The MILS component integration approach to secure information sharing. In: 27th IEEE\/AIAA Digital Avionics Systems Conference (DASC), St. Paul, MN (October 2008)","DOI":"10.1109\/DASC.2008.4702758"},{"key":"6_CR2","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, Aachen, Germany, October 2009. ENTCS, vol.\u00a0254, pp. 25\u201344. Elsevier, Amsterdam (2009)"},{"key":"6_CR3","unstructured":"Elkaduwe, D., Klein, G., Elphinstone, K.: Verified protection model of the seL4 microkernel. Technical Report NRL-1474, NICTA (October 2007), http:\/\/ertos.nicta.com.au\/publications\/papers\/Elkaduwe_GE_07.pdf"},{"key":"6_CR4","first-page":"11","volume-title":"IEEE Symp. Security & Privacy","author":"J. Goguen","year":"1982","unstructured":"Goguen, J., Meseguer, J.: Security policies and security models. In: IEEE Symp. Security & Privacy, Oakland, California, USA, April 1982, pp. 11\u201320. IEEE Computer Society, Los Alamitos (1982)"},{"issue":"6","key":"6_CR5","first-page":"28","volume":"34","author":"G. Klein","year":"2009","unstructured":"Klein, G.: Correct OS kernel? proof? done! USENIX ;login:\u00a034(6), 28\u201334 (2009)","journal-title":"USENIX ;login:"},{"issue":"6","key":"6_CR6","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G. Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., 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. CACM\u00a053(6), 107\u2013115 (2010)","journal-title":"CACM"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/1629575.1629596","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, Big Sky, MT, USA, October 2009, pp. 207\u2013220. ACM, New York (2009)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Kuz, I., Klein, G., Lewis, C., Walker, A.: capDL: A language for describing capability-based systems. In: 1st APSys, New Delhi, India (August 2010) (to appear)","DOI":"10.1145\/1851276.1851284"},{"key":"6_CR9","first-page":"42","volume-title":"33rd POPL","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) 33rd POPL, pp. 42\u201354. ACM, New York (2006)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL\u2014 A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle\/HOL\u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"1278","DOI":"10.1109\/PROC.1975.9939","volume":"63","author":"J.H. Saltzer","year":"1975","unstructured":"Saltzer, J.H., Schroeder, M.D.: The protection of information in computer systems. Proc. IEEE\u00a063, 1278\u20131308 (1975)","journal-title":"Proc. IEEE"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15057-9_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:01:01Z","timestamp":1606186861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15057-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642150562","9783642150579"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15057-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}