{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T15:10:47Z","timestamp":1777129847869,"version":"3.51.4"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"10","license":[{"start":{"date-parts":[[2019,9,24]],"date-time":"2019-09-24T00:00:00Z","timestamp":1569283200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-2-0293, FA8750-16-2- 0274, FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-12-2-0293, FA8750-16-2- 0274, FA8750-15-C-0082"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1065451, 1521523, 1715154"],"award-info":[{"award-number":["1065451, 1521523, 1715154"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2019,9,24]]},"abstract":"<jats:p>Operating system (OS) kernels form the backbone of system software. They can have a significant impact on the resilience and security of today's computers. Recent efforts have demonstrated the feasibility of formally verifying simple general-purpose kernels, but they have ignored the important issues of concurrency, which include not just user and I\/O concurrency on a single core, but also multi-core parallelism with fine-grained locking. In this work, we present CertiKOS, a novel compositional framework for building verified concurrent OS kernels. Concurrency allows interleaved execution of programs belonging to different abstraction layers and running on different CPUs\/threads. Each such layer can have a different set of observable events. In CertiKOS, these layers and their observable events can be formally specified, and each module can then be verified at the abstraction level it belongs to. To link all the verified pieces together, CertiKOS enforces a so-called contextual refinement property for every such piece, which states that the implementation will behave like its specification under any concurrent context with any valid interleaving. Using CertiKOS, we have successfully developed a practical concurrent OS kernel, called mC2, and built the formal proofs of its correctness in Coq. The mC2 kernel is written in 6500 lines of C and x86 assembly and runs on stock x86 multicore machines. To our knowledge, this is the first correctness proof of a general-purpose concurrent OS kernel with fine-grained locking.<\/jats:p>","DOI":"10.1145\/3356903","type":"journal-article","created":{"date-parts":[[2019,9,24]],"date-time":"2019-09-24T12:58:26Z","timestamp":1569329906000},"page":"89-99","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Building certified concurrent OS kernels"],"prefix":"10.1145","volume":"62","author":[{"given":"Ronghui","family":"Gu","sequence":"first","affiliation":[{"name":"Columbia University, New York, NY"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hao","family":"Chen","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jieung","family":"Kim","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00e9r\u00e9mie","family":"Koenig","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiongnan (Newman)","family":"Wu","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vilhelm","family":"Sj\u00f6berg","sequence":"additional","affiliation":[{"name":"CertiK, Cambridge, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Costanzo","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,9,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_3"},{"key":"e_1_2_1_2_1","volume-title":"Operating Systems Principles and Practice","author":"Anderson T.","year":"2011","unstructured":"Anderson , T. , Dahlin , M. Operating Systems Principles and Practice . Recursive Books , 2011 (Figure 5.14). Anderson, T., Dahlin, M. Operating Systems Principles and Practice. Recursive Books, 2011 (Figure 5.14)."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI'12)","author":"Belay A.","year":"2012","unstructured":"Belay , A. , Bittau , A. , Mashtizadeh , A. , Mazi\u00e8res , D. , Kozyrakis , C. Dune : Safe user-level access to privileged CPU features . In Proceedings of 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI'12) ( 2012 ), 335--348. Belay, A., Bittau, A., Mashtizadeh, A., Mazi\u00e8res, D., Kozyrakis, C. Dune: Safe user-level access to privileged CPU features. In Proceedings of 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI'12) (2012), 335--348."},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of 2014 ACM Conference on Programming Language Design and Implementation (PLDI'14)","author":"Carbonneaux Q.","year":"2014","unstructured":"Carbonneaux , Q. , Hoffmann , J. , Ramananandro , T. , Shao , Z. End-to-end verification of stackspace bounds for C programs . In Proceedings of 2014 ACM Conference on Programming Language Design and Implementation (PLDI'14) ( 2014 ), 270--281. Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z. End-to-end verification of stackspace bounds for C programs. In Proceedings of 2014 ACM Conference on Programming Language Design and Implementation (PLDI'14) (2014), 270--281."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_2_1_9_1","volume-title":"Commun. ACM","author":"Dijkstra E.W.","year":"1968","unstructured":"Dijkstra , E.W. The structure of the \"THE\"-multiprograrnrning system . Commun. ACM , ( 1968 ), 341--346. Dijkstra, E.W. The structure of the \"THE\"-multiprograrnrning system. Commun. ACM, (1968), 341--346."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI'16)","author":"Gu R.","year":"2016","unstructured":"Gu , R. , Shao , Z. , Chen , H. , Wu , X.N. , Kim , J. , Sj\u00f6berg , V. , Costanzo , D. Certikos : An extensible architecture for building certified concurrent OS kernels . In Proceedings of 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI'16) ( 2016 ), 653--669. Gu, R., Shao, Z., Chen, H., Wu, X.N., Kim, J., Sj\u00f6berg, V., Costanzo, D. Certikos: An extensible architecture for building certified concurrent OS kernels. In Proceedings of 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI'16) (2016), 653--669."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI'14)","author":"Hawblitzel C.","year":"2014","unstructured":"Hawblitzel , C. , Howell , J. , Lorch , J.R. , Narayan , A. , Parno , B. , Zhang , D. , Zill , B. Ironclad apps : End-to-end security via automated full-system verification . In Proceedings of 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI'14) ( 2014 ), 165--181 Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B. Ironclad apps: End-to-end security via automated full-system verification. In Proceedings of 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI'14) (2014), 165--181"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_2_1_15_1","volume-title":"Morgan Kaufmann","author":"Herlihy M.","year":"2008","unstructured":"Herlihy , M. , Shavit , N. The Art of Multiprocessor Programming . Morgan Kaufmann , 2008 . Herlihy, M., Shavit, N. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_14"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/358818.358824"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2797022.2797042"},{"key":"e_1_2_1_24_1","first-page":"59","article-title":"A practical verification framework for preemptive OS kernels. In Proceedings of 28th International Conference on Computer-Aided Verification (CAV)","author":"Xu F.","year":"2016","unstructured":"Xu , F. , Fu , M. , Feng , X. , Zhang , X. , Zhang , H. , Li , Z . A practical verification framework for preemptive OS kernels. In Proceedings of 28th International Conference on Computer-Aided Verification (CAV) , Part II ( 2016 ), 59 -- 79 . Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z. A practical verification framework for preemptive OS kernels. In Proceedings of 28th International Conference on Computer-Aided Verification (CAV), Part II (2016), 59--79.","journal-title":"Part"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3356903","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3356903","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3356903","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:37Z","timestamp":1750203877000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3356903"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,24]]},"references-count":23,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2019,9,24]]}},"alternative-id":["10.1145\/3356903"],"URL":"https:\/\/doi.org\/10.1145\/3356903","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9,24]]},"assertion":[{"value":"2019-09-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}