{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T10:08:37Z","timestamp":1781258917710,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":68,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,10,11]],"date-time":"2009-10-11T00:00:00Z","timestamp":1255219200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2009,10,11]]},"DOI":"10.1145\/1629575.1629596","type":"proceedings-article","created":{"date-parts":[[2009,10,13]],"date-time":"2009-10-13T15:11:11Z","timestamp":1255446671000},"page":"207-220","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1142,"title":["seL4"],"prefix":"10.1145","author":[{"given":"Gerwin","family":"Klein","sequence":"first","affiliation":[{"name":"NICTA & UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kevin","family":"Elphinstone","sequence":"additional","affiliation":[{"name":"NICTA & UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"NICTA, UNSW & Open Kernel Labs, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[{"name":"NICTA & UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Cock","sequence":"additional","affiliation":[{"name":"NICTA & UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philip","family":"Derrin","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dhammika","family":"Elkaduwe","sequence":"additional","affiliation":[{"name":"NICTA & UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kai","family":"Engelhardt","sequence":"additional","affiliation":[{"name":"UNSW & NICTA, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rafal","family":"Kolanski","sequence":"additional","affiliation":[{"name":"NICTA & UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[{"name":"NICTA & ANU, Canberra, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Harvey","family":"Tuch","sequence":"additional","affiliation":[{"name":"NICTA & UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simon","family":"Winwood","sequence":"additional","affiliation":[{"name":"NICTA & UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,10,11]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"93","volume-title":"1986 Summer USENIX","author":"Accetta M.","year":"1986","unstructured":"M. Accetta , R. Baron , W. Bolosky , D. Golub , R. Rashid , A. Tevanian , and M. Young . Mach: A new kernel foundation for UNIX development . In 1986 Summer USENIX , pages 93 -- 112 , 1986 . M. Accetta, R. Baron, W. Bolosky, D. Golub, R. Rashid, A. Tevanian, and M. Young. Mach: A new kernel foundation for UNIX development. In 1986 Summer USENIX, pages 93--112, 1986."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9123-z"},{"key":"e_1_3_2_1_3_1","series-title":"LNCS","first-page":"109","volume-title":"Tools and Alg. for the Construction and Analysis of Systems (TACAS)","author":"Alkassar E.","year":"2008","unstructured":"E. Alkassar , N. Schirmer , and A. Starostin . Formal pervasive verification of a paging mechanism . In C.R. Ramakrishnan and J. Rehof, editors, Tools and Alg. for the Construction and Analysis of Systems (TACAS) , volume 4963 of LNCS , pages 109 -- 123 . Springer , 2008 . E. Alkassar, N. Schirmer, and A. Starostin. Formal pervasive verification of a paging mechanism. In C.R. Ramakrishnan and J. Rehof, editors, Tools and Alg. for the Construction and Analysis of Systems (TACAS), volume 4963 of LNCS, pages 109--123. Springer, 2008."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1504\/IJES.2006.014859"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/826036.826866"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224077"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.41331"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302691"},{"key":"e_1_3_2_1_11_1","first-page":"99","volume-title":"A verified shared capability model","author":"Boyton A.","year":"2009","unstructured":"A. Boyton . A verified shared capability model . In G. Klein, R. Huuck, and B. Schlich, editors, 4th WS Syst. Softw. Verification SSV'09, ENTCS, pages 99 -- 116 . Elsevier , Jun 2009 . A. Boyton. A verified shared capability model. In G. Klein, R. Huuck, and B. Schlich, editors, 4th WS Syst. Softw. Verification SSV'09, ENTCS, pages 99--116. Elsevier, Jun 2009."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/362258.362278"},{"key":"e_1_3_2_1_13_1","unstructured":"D.\n      Cock\n    .\n  Bitfields and tagged unions in C: Verification through automatic generation\n  . In B. Beckert and G. Klein editors VERIFY\n  '08 volume \n  372\n   of \n  CEUR Workshop Proceedings pages \n  44\n  --\n  55 Aug \n  2008\n  .  D. Cock. Bitfields and tagged unions in C: Verification through automatic generation. In B. Beckert and G. Klein editors VERIFY'08 volume 372 of CEUR Workshop Proceedings pages 44--55 Aug 2008."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294295"},{"key":"e_1_3_2_1_17_1","unstructured":"U. Dannowski. Personal communication.  U. Dannowski. Personal communication."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1525579"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159842.1159850"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1435458.1435465"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_11"},{"key":"e_1_3_2_1_22_1","first-page":"117","volume-title":"11th HotOS","author":"Elphinstone K.","year":"2007","unstructured":"K. Elphinstone , G. Klein , P. Derrin , T. Roscoe , and G. Heiser . Towards a practical, verified kernel . In 11th HotOS , pages 117 -- 122 , May 2007 . K. Elphinstone, G. Klein, P. Derrin, T. Roscoe, and G. Heiser. Towards a practical, verified kernel. In 11th HotOS, pages 117--122, May 2007."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217953"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/MARK.1979.8817256"},{"key":"e_1_3_2_1_25_1","volume-title":"3rd OSDI. USENIX","author":"Ford B.","year":"1999","unstructured":"B. Ford , M. Hibler , J. Lepreau , R. McGrath , and P. Tullmann . Interface and execution models in the Fluke kernel . In 3rd OSDI. USENIX , Feb 1999 . B. Ford, M. Hibler, J. Lepreau, R. McGrath, and P. Tullmann. Interface and execution models in the Fluke kernel. In 3rd OSDI. USENIX, Feb 1999."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945464"},{"key":"e_1_3_2_1_27_1","unstructured":"Green Hills Software Inc. INTEGRITY-178B separation kernel security target version 1.0. http:\/\/www.niap-ccevs.org\/cc-scheme\/st\/st_vid10119-st.pdf 2008.  Green Hills Software Inc. INTEGRITY-178B separation kernel security target version 1.0. http:\/\/www.niap-ccevs.org\/cc-scheme\/st\/st_vid10119-st.pdf 2008."},{"key":"e_1_3_2_1_28_1","unstructured":"Greenhills Software Inc. Integrity real-time operating system. http:\/\/www.ghs.com\/products\/rtos\/integrity.html 2008.  Greenhills Software Inc. Integrity real-time operating system. http:\/\/www.ghs.com\/products\/rtos\/integrity.html 2008."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1066473.1066478"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1987.226478"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217975.1217978"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1700527.1700692"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180448"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1767111.1767128"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133572.1133615"},{"key":"e_1_3_2_1_36_1","volume-title":"2nd PLOS","author":"Hohmuth M.","year":"2005","unstructured":"M. Hohmuth and H. Tews . The VFiasco approach for a verified operating system . In 2nd PLOS , Jul 2005 . M. Hohmuth and H. Tews. The VFiasco approach for a verified operating system. In 2nd PLOS, Jul 2005."},{"key":"e_1_3_2_1_37_1","unstructured":"Iguana. http:\/\/www.ertos.nicta.com.au\/software\/kenge\/iguana-project\/latest\/.  Iguana. http:\/\/www.ertos.nicta.com.au\/software\/kenge\/iguana-project\/latest\/."},{"key":"e_1_3_2_1_38_1","first-page":"1","article-title":"Government Protection Profile for Separation Kernels","author":"Directorate Information Assurance","year":"2007","unstructured":"Information Assurance Directorate . U.S . Government Protection Profile for Separation Kernels in Environments Requiring High Robustness , Jun 2007 . Version 1 .03. http:\/\/www.niap--ccevs.org\/cc--scheme\/pp\/pp.cfm\/id\/pp_skpp_hr_v1.03\/. Information Assurance Directorate. U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, Jun 2007. Version 1.03. http:\/\/www.niap--ccevs.org\/cc--scheme\/pp\/pp.cfm\/id\/pp_skpp_hr_v1.03\/.","journal-title":"Environments Requiring High Robustness"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9126-9"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596566"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_20"},{"key":"e_1_3_2_1_43_1","unstructured":"L4HQ. http:\/\/l4hq.org\/arch\/arm\/.  L4HQ. http:\/\/l4hq.org\/arch\/arm\/."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168633"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/234215.234473"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/822075.822414"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/786768.786973"},{"key":"e_1_3_2_1_49_1","series-title":"LNCS","first-page":"189","volume-title":"Proc. TPHOLs'07","author":"Ni Z.","year":"2007","unstructured":"Z. Ni , D. Yu , and Z. Shao . Using XCAP to certify realistic system code: Machine context management . In Proc. TPHOLs'07 , volume 4732 of LNCS , pages 189 -- 206 . Springer , Sep 2007 . Z. Ni, D. Yu, and Z. Shao. Using XCAP to certify realistic system code: Machine context management. In Proc. TPHOLs'07, volume 4732 of LNCS, pages 189--206. Springer, Sep 2007."},{"key":"e_1_3_2_1_50_1","series-title":"LNCS","volume-title":"Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. Paulson , and M. Wenzel . Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS . Springer , 2002 . T. Nipkow, L. Paulson, and M. Wenzel. Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002."},{"key":"e_1_3_2_1_51_1","unstructured":"OKL4 web site. http:\/\/okl4.org.  OKL4 web site. http:\/\/okl4.org."},{"key":"e_1_3_2_1_52_1","first-page":"146","volume-title":"Proceedings of the Seventh DoD\/NBS Computer Security Initiative Conference","author":"Perrine T.","year":"1984","unstructured":"T. Perrine , J. Codd , and B. Hardy . An overview of the kernelized secure operating system (KSOS) . In Proceedings of the Seventh DoD\/NBS Computer Security Initiative Conference , pages 146 -- 160 , Sep 1984 . T. Perrine, J. Codd, and B. Hardy. An overview of the kernelized secure operating system (KSOS). In Proceedings of the Seventh DoD\/NBS Computer Security Initiative Conference, pages 146--160, Sep 1984."},{"key":"e_1_3_2_1_53_1","unstructured":"Rockwell Collins Inc. AAMP7r1 Reference Manual 2003.  Rockwell Collins Inc. AAMP7r1 Reference Manual 2003."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/800216.806586"},{"key":"e_1_3_2_1_55_1","first-page":"129","volume-title":"10th National Computer Security Conference","author":"Saydjari O.","year":"1987","unstructured":"O. Saydjari , J. Beckman , and J. Leaman . Locking computers securely . In 10th National Computer Security Conference , pages 129 -- 141 , Sep 1987 . O. Saydjari, J. Beckman, and J. Leaman. Locking computers securely. In 10th National Computer Security Conference, pages 129--141, Sep 1987."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294294"},{"key":"e_1_3_2_1_57_1","first-page":"89","volume-title":"5th IWOOOS","author":"Shapiro J.S.","year":"1996","unstructured":"J.S. Shapiro , D.F. Faber , and J.M. Smith . State caching in the EROS kernel--implementing efficient orthogonal peristence in a pure capability system . In 5th IWOOOS , pages 89 -- 100 , Nov 1996 . J.S. Shapiro, D.F. Faber, and J.M. Smith. State caching in the EROS kernel--implementing efficient orthogonal peristence in a pure capability system. In 5th IWOOOS, pages 89--100, Nov 1996."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/319151.319163"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217951"},{"key":"e_1_3_2_1_60_1","volume-title":"8th USENIX Security Symp.","author":"Spencer R.","year":"1999","unstructured":"R. Spencer , S. Smalley , P. Loscocco , M. Hibler , D. Andersen , and J. Lepreau . The Flask security architecture: System support for diverse security policies . In 8th USENIX Security Symp. , Aug 1999 . R. Spencer, S. Smalley, P. Loscocco, M. Hibler, D. Andersen, and J. Lepreau. The Flask security architecture: System support for diverse security policies. In 8th USENIX Security Symp., Aug 1999."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.043"},{"key":"e_1_3_2_1_62_1","volume-title":"UNSW","author":"Tuch H.","year":"2008","unstructured":"H. Tuch . Formal Memory Models for Verifying C Systems Code. PhD thesis , UNSW , Aug 2008 . H. Tuch. Formal Memory Models for Verifying C Systems Code. PhD thesis, UNSW, Aug 2008."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9120-2"},{"key":"e_1_3_2_1_64_1","volume-title":"USENIX","author":"Tuch H.","year":"2005","unstructured":"H. Tuch , G. Klein , and G. Heiser . OS verification -- now! In 10th HotOS, pages 7--12 . USENIX , Jun 2005 . H. Tuch, G. Klein, and G. Heiser. OS verification -- now! In 10th HotOS, pages 7--12. USENIX, Jun 2005."},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_3_2_1_66_1","volume-title":"Common Criteria for IT Security Evaluation","author":"US National Institute of Standards.","year":"1999","unstructured":"US National Institute of Standards. Common Criteria for IT Security Evaluation , 1999 . ISO Standard 15408. http:\/\/csrc.nist.gov\/cc\/. US National Institute of Standards. Common Criteria for IT Security Evaluation, 1999. ISO Standard 15408. http:\/\/csrc.nist.gov\/cc\/."},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/358818.358825"},{"key":"e_1_3_2_1_68_1","volume-title":"http:\/\/www.dwheeler.com\/sloccount\/","author":"Wheeler D.A.","year":"2001","unstructured":"D.A. Wheeler . SLOCCount. http:\/\/www.dwheeler.com\/sloccount\/ , 2001 . D.A. Wheeler. SLOCCount. http:\/\/www.dwheeler.com\/sloccount\/, 2001."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.5555\/1060289.1060308"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_34"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/355616.364017"}],"event":{"name":"SOSP09: ACM SIGOPS 22nd Symposium on Operating Systems Principles","location":"Big Sky Montana USA","acronym":"SOSP09","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1629575.1629596","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1629575.1629596","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:23:27Z","timestamp":1750249407000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1629575.1629596"}},"subtitle":["formal verification of an OS kernel"],"short-title":[],"issued":{"date-parts":[[2009,10,11]]},"references-count":68,"alternative-id":["10.1145\/1629575.1629596","10.1145\/1629575"],"URL":"https:\/\/doi.org\/10.1145\/1629575.1629596","relation":{},"subject":[],"published":{"date-parts":[[2009,10,11]]},"assertion":[{"value":"2009-10-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}