{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:00:07Z","timestamp":1725570007526},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642171635"},{"type":"electronic","value":"9783642171642"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17164-2_3","type":"book-chapter","created":{"date-parts":[[2010,11,19]],"date-time":"2010-11-19T05:54:39Z","timestamp":1290146079000},"page":"21-33","source":"Crossref","is-referenced-by-count":8,"title":["From a Verified Kernel towards Verified Systems"],"prefix":"10.1007","author":[{"given":"Gerwin","family":"Klein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","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.) Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada. USENIX (October 2010)"},{"issue":"11","key":"3_CR2","doi-asserted-by":"publisher","first-page":"1382","DOI":"10.1109\/32.41331","volume":"15","author":"W.R. Bevier","year":"1989","unstructured":"Bevier, W.R.: Kit: A study in operating system verification. IEEE Transactions on Software Engineering\u00a015(11), 1382\u20131396 (1989)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"3_CR3","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W.R. Bevier","year":"1989","unstructured":"Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: An approach to systems verification. Journal of Automated Reasoning\u00a05(4), 411\u2013428 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"3_CR4","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":"3_CR5","series-title":"Electronic Notes in Computer Science","first-page":"25","volume-title":"Proceedings of the 4th Workshop on Systems Software Verification","author":"A. Boyton","year":"2009","unstructured":"Boyton, A.: A verified shared capability model. In: Klein, G., Huuck, R., Schlich, B. (eds.) Proceedings of the 4th Workshop on Systems Software Verification, Aachen, Germany. Electronic Notes in Computer Science, vol.\u00a0254, pp. 25\u201344. Elsevier, Amsterdam (2009)"},{"key":"3_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":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"3_CR8","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":"3_CR9","doi-asserted-by":"crossref","unstructured":"Feiertag, R.J., Neumann, P.G.: The foundations of a provably secure operating system (PSOS). In: AFIPS Conference Proceedings, 1979 National Computer Conference, New York, NY, USA, pp. 329\u2013334 (June 1979)","DOI":"10.1109\/MARK.1979.8817256"},{"key":"3_CR10","unstructured":"Hart, B.: SDR security threats in an open source world. In: Software Defined Radia Conference, Phoenix, AZ, USA, pp. 3.5\u20133 1\u20134 (November 2004)"},{"issue":"6","key":"3_CR11","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":"3_CR12","doi-asserted-by":"publisher","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. Communications of the ACM\u00a053(6), 107\u2013115 (2010)","journal-title":"Communications of the ACM"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"Proceedings of the 22nd ACM Symposium on Operating Systems Principles","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: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, pp. 207\u2013220. ACM, New York (2009)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Koscher, K., Czeskis, A., Roesner, F., Patel, S., Kohno, T., Checkoway, S., McCoy, D., Kantor, B., Anderson, D., Shacham, H., Savage, S.: Experimental security analysis of a modern automobile. In: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, USA, pp. 447\u2013462 (May 2010)","DOI":"10.1109\/SP.2010.34"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Kuz, I., Klein, G., Lewis, C., Walker, A.: capDL: A language for describing capability-based systems. In: Proceedings of the 1st Asia-Pacific Workshop on Systems, New Delhi, India (to appear, August 2010)","DOI":"10.1145\/1851276.1851284"},{"key":"3_CR16","unstructured":"Meng, J., Paulson, L.C., Klein, G.: A termination checker for Isabelle Hoare logic. In: Beckert, B. (ed.) Proceedings of the 4th International Verification Workshop, Bremen, Germany. CEUR Workshop Proceedings, vol.\u00a0259, pp. 104\u2013118 (July 2007)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"3_CR18","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":"3_CR19","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, pp. 97\u2013108 (January 2007)","DOI":"10.1145\/1190216.1190234"},{"issue":"2","key":"3_CR20","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. Communications of the ACM\u00a023(2), 118\u2013131 (1980)","journal-title":"Communications of the ACM"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-03359-9_34","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Winwood","year":"2009","unstructured":"Winwood, S., Klein, G., Sewell, T., Andronick, J., Cock, D., Norrish, M.: Mind the gap: A verification framework for low-level C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol.\u00a05674, pp. 500\u2013515. Springer, Heidelberg (2009)"},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1145\/1806596.1806610","volume-title":"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"J. Yang","year":"2010","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, Toronto, Ontario, Canada, pp. 99\u2013110. ACM, New York (June 2010)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17164-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,13]],"date-time":"2020-06-13T19:06:49Z","timestamp":1592075209000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17164-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642171635","9783642171642"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17164-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}