{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:54:15Z","timestamp":1743040455409,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031712609"},{"type":"electronic","value":"9783031712616"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-71261-6_2","type":"book-chapter","created":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:02:03Z","timestamp":1725735723000},"page":"21-38","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verified Fault Handling for\u00a0Modern Board Management Controllers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7215-9147","authenticated-orcid":false,"given":"Ben","family":"Fiedler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5411-9785","authenticated-orcid":false,"given":"Zikai","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2997-6560","authenticated-orcid":false,"given":"David","family":"Cock","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8298-1126","authenticated-orcid":false,"given":"Timothy","family":"Roscoe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,8]]},"reference":[{"key":"2_CR1","unstructured":"OpenBMC. https:\/\/www.openbmc.org\/"},{"key":"2_CR2","unstructured":"AMD: Zynq UltraScale+ Device Technical Reference Manual. Tech. Rep.\u00a02.4 (2023). https:\/\/docs.amd.com\/r\/en-US\/ug1085-zynq-ultrascale-trm"},{"issue":"10","key":"2_CR3","doi-asserted-by":"publisher","first-page":"1693","DOI":"10.1016\/j.jss.2011.04.054","volume":"84","author":"D Bucur","year":"2011","unstructured":"Bucur, D., Kwiatkowska, M.: On software verification for sensor nodes. J. Syst. Softw. 84(10), 1693\u20131707 (2011)","journal-title":"J. Syst. Softw."},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Burns, A., Davis, R.I.: A survey of research into mixed criticality systems. ACM Comput. Surv. 50(6) (2017). https:\/\/doi.org\/10.1145\/3131347","DOI":"10.1145\/3131347"},{"key":"2_CR5","unstructured":"Christian Svensson et al: Open-source firmware for your baseboard management controller (BMC) (2018). https:\/\/github.com\/u-root\/u-bmc, computer Software"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Cock, D., et al.: Enzian: an open, general, CPU\/FPGA platform for systems software research. In: Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 434\u2013451. ASPLOS \u201922, Association for Computing Machinery, New York, NY, USA (Feb 2022). https:\/\/doi.org\/10.1145\/3503222.3507742","DOI":"10.1145\/3503222.3507742"},{"key":"2_CR7","unstructured":"Cofer, D., et al.: Secure mathematically-assured composition of control models. Tech. Rep. AFRL-RI-RS-TR-2017-176, Rockwell Collins, Cedar Rapids, United States (Sep 2017). https:\/\/apps.dtic.mil\/sti\/citations\/AD1039782"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Curbo, J., Falco, G.: A research agenda for space flight software security. In: 2023 IEEE 9th International Conference on Space Mission Challenges for Information Technology (SMC-IT), pp. 68\u201377 (2023). https:\/\/doi.org\/10.1109\/SMC-IT56444.2023.00016","DOI":"10.1109\/SMC-IT56444.2023.00016"},{"key":"2_CR9","unstructured":"Database, M.C.: CVE-2022-40242 (Dec 2022). https:\/\/www.cve.org\/CVERecord?id=CVE-2022-40242"},{"key":"2_CR10","unstructured":"Database, M.C.: CVE-2022-40259 (Dec 2022). https:\/\/www.cve.org\/CVERecord?id=CVE-2022-40259"},{"key":"2_CR11","unstructured":"Database, M.C.: CVE-2021-39295 (Apr 2023). https:\/\/www.cve.org\/CVERecord?id=CVE-2021-39295"},{"key":"2_CR12","unstructured":"Database, M.C.: CVE-2022-26872 (Jan 2023). https:\/\/www.cve.org\/CVERecord?id=CVE-2022-26872"},{"key":"2_CR13","unstructured":"Database, M.C.: CVE-2023-31008 (Jan 2024). https:\/\/www.cve.org\/CVERecord?id=CVE-2023-31008"},{"key":"2_CR14","unstructured":"Database, M.C.: CVE-2023-31037 (Jan 2024). https:\/\/www.cve.org\/CVERecord?id=CVE-2023-31037"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Farrukh, A., West, R.: Flyos: integrated modular avionics for autonomous multicopters. In: 2022 IEEE 28th Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 68\u201381 (2022). https:\/\/doi.org\/10.1109\/RTAS54340.2022.00014","DOI":"10.1109\/RTAS54340.2022.00014"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Fiedler, B., Liu, Z.: An sel4-based board management controller with verified fault handling for the Enzian research computer. https:\/\/doi.org\/10.5281\/zenodo.12775411","DOI":"10.5281\/zenodo.12775411"},{"issue":"2","key":"2_CR17","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/3369758","volume":"63","author":"J Frazelle","year":"2020","unstructured":"Frazelle, J.: Opening up the baseboard management controller. Commun. ACM 63(2), 38\u201340 (2020)","journal-title":"Commun. ACM"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Greenaway, D., Lim, J., Andronick, J., Klein, G.: Don\u2019t sweat the small stuff: formal verification of C code without the pain. SIGPLAN Not. 49(6), 429\u2013439 (2014). https:\/\/doi.org\/10.1145\/2666356.2594296","DOI":"10.1145\/2666356.2594296"},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-030-61467-6_18","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20\u201330, 2020, Proceedings, Part III","author":"M Huisman","year":"2020","unstructured":"Huisman, M., Monti, R.E.: On the industrial application of critical software verification with VerCors. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Applications: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20\u201330, 2020, Proceedings, Part III, pp. 273\u2013292. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_18"},{"key":"2_CR20","unstructured":"International Rectifier: Dual Output Digital Multi-Phase Controller IR3581. Tech. rep. (Apr 2014)"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Jung, R., et al.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 637\u2013650. POPL \u201915, Association for Computing Machinery, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"2_CR22","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales a sectioning concept for isabelle. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) Theorem Proving in Higher Order Logics, pp. 149\u2013165. Springer Berlin Heidelberg, Berlin, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_11"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems 32(1), 2:1\u20132:70 (2014). https:\/\/doi.org\/10.1145\/2560537","DOI":"10.1145\/2560537"},{"key":"2_CR24","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/3230627","volume":"61","author":"G Klein","year":"2018","unstructured":"Klein, G., Andronick, J., Kuz, I., Murray, T., Heiser, G., Fernandez, M.: Formally verified software in the real world. Commun. ACM 61, 68\u201377 (2018). https:\/\/doi.org\/10.1145\/3230627","journal-title":"Commun. ACM"},{"issue":"5","key":"2_CR25","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1016\/j.jss.2006.08.039","volume":"80","author":"I Kuz","year":"2007","unstructured":"Kuz, I., Liu, Y., Gorton, I., Heiser, G.: CAmkES: a component model for secure microkernel-based embedded systems. J. Syst. Softw. 80(5), 687\u2013699 (2007). https:\/\/doi.org\/10.1016\/j.jss.2006.08.039","journal-title":"J. Syst. Softw."},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Specifying concurrent program modules. ACM Trans. Programm. Lang. Syst. 5(2), 190\u2013222 (1983). https:\/\/www.microsoft.com\/en-us\/research\/publication\/specifying-concurrent-program-modules\/","DOI":"10.1145\/69624.357207"},{"key":"2_CR27","unstructured":"Lyons, A.: Mixed-Criticality Scheduling and Resource Sharing for High-Assurance Operating Systems. Phd thesis, University of New South Wales (Sep 2018). https:\/\/trustworthy.systems\/publications\/papers\/Lyons%3Aphd.pdf"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Martins, J., Pinto, S.: Shedding light on static partitioning hypervisors for arm-based mixed-criticality systems. In: 2023 IEEE 29th Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 40\u201353 (2023). https:\/\/doi.org\/10.1109\/RTAS58335.2023.00011","DOI":"10.1109\/RTAS58335.2023.00011"},{"key":"2_CR29","unstructured":"Maxim Integrated Products, Inc.: MAX15301 InTune Automatically Compensated Digital PoL Controller with Driver and PMBus Telemetry. Tech. rep. (Nov 2013)"},{"key":"2_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: a proof assistant for higher-order logic. Springer-Verlag, Berlin, Heidelberg (2002)"},{"key":"2_CR31","doi-asserted-by":"publisher","unstructured":"Paturel, M., Subasinghe, I., Heiser, G.: First steps in verifying the seL4 Core Platform. In: Asia-Pacific Workshop on Systems (APSys). ACM, Seoul, KR (Aug 2023). https:\/\/doi.org\/10.1145\/3609510.3609821","DOI":"10.1145\/3609510.3609821"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science 1977 pp. 46\u201357 (1977). https:\/\/api.semanticscholar.org\/CorpusID:117103037","DOI":"10.1109\/SFCS.1977.32"},{"key":"2_CR33","unstructured":"SBS Implementers Forum: System Management Bus (SMBus) Specification (Version 2.0). Tech. rep. (Aug 2000)"},{"key":"2_CR34","unstructured":"Schirmer, N.: A sequential imperative programming language syntax, semantics, hoare logics and verification environment. Arch. Formal Proofs 2008 (2008). https:\/\/www.isa-afp.org\/entries\/Simpl.shtml"},{"key":"2_CR35","unstructured":"Semiconductors, N.: I2c-bus specification and user manual. Tech. rep. (Oct 2021). https:\/\/www.nxp.com\/docs\/en\/user-guide\/UM10204.pdf"},{"key":"2_CR36","unstructured":"Steven Vaughan-Nichols: MINIX: Intel\u2019s hidden in-chip operating system. https:\/\/www.zdnet.com\/article\/minix-intels-hidden-in-chip-operating-system\/"},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"Sudvarg, M., Gill, C.: A concurrency framework for priority-aware intercomponent requests in camkes on sel4. In: 2022 IEEE 28th International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), pp. 1\u201310 (2022). https:\/\/doi.org\/10.1109\/RTCSA55878.2022.00007","DOI":"10.1109\/RTCSA55878.2022.00007"},{"key":"2_CR38","unstructured":"System Management Interface Forum, Inc.: PMBus Power System Management Protocol Specification Part I \u2013 General Requirements, Transport And Electrical Interface (Revision 1.3.1). Tech. rep. (Mar 2015)"},{"key":"2_CR39","unstructured":"The seL4 community: Notifications and shared memory (Nov 2020). https:\/\/docs.sel4.systems\/Tutorials\/notifications.html. Accessed 28 May 2024"},{"key":"2_CR40","unstructured":"Xilinx: Zynq UltraScale+ MPSoC Software Developer Guide. Tech. Rep. UG1137 (v2022.2) (Nov 2022)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71261-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:02:28Z","timestamp":1725735748000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71261-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031712609","9783031712616"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71261-6_2","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":"8 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Aspects of Component Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"facs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/facs-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}