{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:29:27Z","timestamp":1742920167293,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572586"},{"type":"electronic","value":"9783031572593"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>An OS microkernel can be extended by implementing services upon it. A service could introduce an object that references a kernel object, and implement a group of functions that invokes the functions for manipulating the kernel object. We consider the scenario where the microkernel has been verified with machine-checkable proofs, while the services remain to be verified. Moreover, the verification of the microkernel is not performed with the verification of subsequent extension in mind. We address the problem of how to build sufficiently on the verification results for the microkernel, in achieving the verification of the services. Our methodology consists of enhancements to the verification framework for the microkernel, and the design of invariants for establishing the connection between the service-level objects and the kernel-level objects. Using the methodology, we have conducted a substantial formal verification of a group of services extending the inter-task communication functionalities of the preemptive microkernel <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mu \\!\\!\\text{ C }\\!\\!\\text{\/ }\\!\\!\\!\\text{ OS-II }$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mrow>\n                  <mml:mi>\u03bc<\/mml:mi>\n                  <mml:mspace\/>\n                  <mml:mspace\/>\n                  <mml:mspace\/>\n                  <mml:mtext>C<\/mml:mtext>\n                  <mml:mspace\/>\n                  <mml:mspace\/>\n                  <mml:mspace\/>\n                  <mml:mtext>\/<\/mml:mtext>\n                  <mml:mspace\/>\n                  <mml:mspace\/>\n                  <mml:mspace\/>\n                  <mml:mspace\/>\n                  <mml:mspace\/>\n                  <mml:mtext>OS-II<\/mml:mtext>\n                  <mml:mspace\/>\n                <\/mml:mrow>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Our verification uncovers dormant bugs and provides a level of correctness assurance for the services that is above what is achievable through extensive testing.<\/jats:p>","DOI":"10.1007\/978-3-031-57259-3_9","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:01:39Z","timestamp":1712322099000},"page":"188-209","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Refinement Verification of OS Services based on a Verified Preemptive Microkernel"],"prefix":"10.1007","author":[{"given":"Ximeng","family":"Li","sequence":"first","affiliation":[]},{"given":"Shanyan","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[]},{"given":"Qianying","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Guohui","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Zhiping","family":"Shi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"9_CR1","unstructured":"The Coq proof assistant. https:\/\/coq.inria.fr\/. Accessed: 2023-10-08."},{"key":"9_CR2","unstructured":"Iris \u2013 a higher-order concurrent separation logic framework, implemented and verified in the Coq proof assistant. https:\/\/iris-project.org\/. Accessed: 2023-10-12."},{"key":"9_CR3","unstructured":"$$\\mu $$C\/OS-II. https:\/\/www.osrtos.com\/rtos\/uc-os-ii\/. Accessed: 2023-10-08."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Eyad Alkassar, Mark\u00a0A. Hillebrand, Dirk Leinenbach, Norbert Schirmer, and Artem Starostin. The Verisoft approach to systems verification. In Proceedings of Second International Conference on Verified Software: Theories, Tools, Experiments (VSTTE), pages 209\u2013224, 2008.","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Eyad Alkassar, Wolfgang\u00a0J. Paul, Artem Starostin, and Alexandra Tsyban. Pervasive verification of an OS microkernel - inline assembly, memory consumption, concurrent devices. In Proceedings of Third International Conference on Verified Software: Theories, Tools, Experiments (VSTTE), pages 71\u201385, 2010.","DOI":"10.1007\/978-3-642-15057-9_5"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"June Andronick, Corey Lewis, and Carroll Morgan. Controlled Owicki-Gries concurrency: Reasoning about the preemptible eChronos embedded operating system. In Proceedings of Workshop on Models for Formal Analysis of Real Systems, (MARS), pages 10\u201324, 2015.","DOI":"10.4204\/EPTCS.196.2"},{"issue":"1","key":"9_CR7","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s13218-010-0005-7","volume":"24","author":"Bernhard Beckert","year":"2010","unstructured":"Bernhard Beckert and Michal Moskal. Deductive verification of system software in the Verisoft XT project. K\u00fcnstliche Intell., 24(1):57\u201361, 2010.","journal-title":"K\u00fcnstliche Intell."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"John Boyland. Checking interference with fractional permissions. In Proceedings of 10th International Symposium on Static Analysis (SAS), pages 55\u201372, 2003.","DOI":"10.1007\/3-540-44898-5_4"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Stephen Brookes and Peter\u00a0W. O\u2019Hearn. Concurrent separation logic. ACM SIGLOG News, 3(3):47\u201365, 2016.","DOI":"10.1145\/2984450.2984457"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew\u00a0W. Appel. VST-Floyd: A separation logic tool to verify correctness of C programs. Journal of Automated Reasoning, 61(1-4):367\u2013422, 2018.","DOI":"10.1007\/s10817-018-9457-5"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter\u00a0W. O\u2019Hearn, and Francesco\u00a0Zappa Nardelli. Applying formal verification to microkernel IPC at Meta. In Proceedings of 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pages 116\u2013129, 2022.","DOI":"10.1145\/3497775.3503681"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Shu Cheng, Jim Woodcock, and Deepak D\u2019Souza. Using formal reasoning on a model of tasks for FreeRTOS. Formal Aspects of Computing, 27(1):167\u2013192, 2015.","DOI":"10.1007\/s00165-014-0308-9"},{"key":"9_CR13","unstructured":"Nathan Chong and Bart Jacobs. Formally verifying FreeRTOS\u2019 interprocess communication mechanism. In Embedded World Exhibition & Conference, 2021."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"David Costanzo, Zhong Shao, and Ronghui Gu. End-to-end verification of information-flow security for C and assembly programs. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 648\u2013664, 2016.","DOI":"10.1145\/2908080.2908100"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Leonardo\u00a0Mendon\u00e7a de\u00a0Moura and Nikolaj\u00a0S. Bj\u00f8rner. Z3: an efficient SMT solver. In Proceedings of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Held as Part of ETAPS, pages 337\u2013340, 2008.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Mike Gordon and H\u00e9l\u00e8ne Collavizza. Forward with Hoare. In A.\u00a0W. Roscoe, Clifford\u00a0B. Jones, and Kenneth\u00a0R. Wood, editors, Reflections on the Work of C. A. R. Hoare, pages 101\u2013121. Springer, 2010.","DOI":"10.1007\/978-1-84882-912-1_5"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, J\u00e9r\u00e9mie Koenig, Xiongnan\u00a0(Newman) Wu, Vilhelm Sj\u00f6berg, and David Costanzo. Building certified concurrent OS kernels. Communications of the ACM, 62(10):89\u201399, 2019.","DOI":"10.1145\/3356903"},{"key":"9_CR18","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan\u00a0(Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 653\u2013669, 2016."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018.","DOI":"10.1017\/S0956796818000151"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Gerwin Klein, June Andronick, Kevin Elphinstone, Toby\u00a0C. Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1):2:1\u20132:70, 2014.","DOI":"10.1145\/2560537"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David\u00a0A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an OS kernel. In Proceedings of 22nd ACM Symposium on Operating Systems Principles (SOSP), pages 207\u2013220, 2009.","DOI":"10.1145\/1629575.1629596"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi\u00a0Wang. Hyperkernel: Push-button verification of an OS kernel. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP), pages 252\u2013269, 2017.","DOI":"10.1145\/3132747.3132748"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow, Lawrence\u00a0C. Paulson, and Markus Wenzel. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Evgeny Novikov and Ilja\u00a0S. Zakharov. Verification of operating system monolithic kernels without extensions. In Proceedings of 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), Part IV, pages 230\u2013248, 2018.","DOI":"10.1007\/978-3-030-03427-6_19"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Leandro\u00a0Batista Ribeiro, Florian Lorber, Ulrik Nyman, Kim\u00a0Guldstrand Larsen, and Marcel Baunach. A modeling concept for formal verification of OS-based compositional software. In Proceedings of 26th International Conference on Fundamental Approaches to Software Engineering (FASE), Held as Part of ETAPS, pages 26\u201346, 2023.","DOI":"10.1007\/978-3-031-30826-0_2"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Aaron\u00a0Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. Logical relations for fine-grained concurrency. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 343\u2013356, 2013.","DOI":"10.1145\/2480359.2429111"},{"key":"9_CR27","unstructured":"Fengwei Xu. Design and Implementation of A Verification Framework for Preemptive OS Kernels. PhD thesis, University of Science and Technology of China, 2016."},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. A practical verification framework for preemptive OS kernels. In Proceedings of 28th International Conference on Computer Aided Verification (CAV), pages 59\u201379, 2016.","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Jean Yang and Chris Hawblitzel. 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 (PLDI), pages 99\u2013110, 2010.","DOI":"10.1145\/1809028.1806610"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Yongwang Zhao, David San\u00e1n, Fuyuan Zhang, and Yang Liu. Refinement-based specification and security analysis of separation kernels. IEEE Transactions on Dependable and Secure Computing, 16(1):127\u2013141, 2019.","DOI":"10.1109\/TDSC.2017.2672983"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57259-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:03:47Z","timestamp":1712322227000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57259-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572586","9783031572593"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57259-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}