{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T14:33:43Z","timestamp":1754145223938,"version":"3.41.2"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"ISSTA","license":[{"start":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T00:00:00Z","timestamp":1750550400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-2340548"],"award-info":[{"award-number":["CNS-2340548"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N660012224037"],"award-info":[{"award-number":["N660012224037"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2025,6,22]]},"abstract":"<jats:p>Embedded software, predominantly written in C, is prone to memory corruption vulnerabilities due to spatial memory issues. Although various memory safety techniques exist, they are often unsuitable for embedded systems due to resource constraints and a lack of standardized OS support. Checked C, a backward-compatible, memory-safe C dialect, offers a potential solution by using pointer annotations for runtime checks to enhance spatial memory safety with minimal overhead. This paper provides the first experience report of porting EDK2 (an open-source UEFI implementation), an exemplary embedded codebase to Checked C, highlighting challenges and providing insights into applying Checked C to similar embedded systems. We also provide an enhanced automated annotation tool e3c, which improves the conversion rate by 25%, enabling easier conversion to Checked C.<\/jats:p>","DOI":"10.1145\/3728929","type":"journal-article","created":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T10:52:56Z","timestamp":1750589576000},"page":"1212-1233","source":"Crossref","is-referenced-by-count":0,"title":["Adding Spatial Memory Safety to EDK II through Checked C (Experience Paper)"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-7199-1879","authenticated-orcid":false,"given":"Sourag","family":"Cherupattamoolayil","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-8720-7138","authenticated-orcid":false,"given":"Arunkumar","family":"Bhattar","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-6314-331X","authenticated-orcid":false,"given":"Connor Everett","family":"Glosner","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5124-6818","authenticated-orcid":false,"given":"Aravind","family":"Machiry","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,22]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Hussein Aitlahcen. 2022. TianoCore EDK2 bindings for Rust UEFI Applications. https:\/\/github.com\/hussein-aitlahcen\/edk2-rs"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.3390\/s21072329"},{"key":"e_1_2_1_3_1","unstructured":"Anthropic. 2025. AI research and products. https:\/\/www.anthropic.com\/"},{"key":"e_1_2_1_4_1","unstructured":"ARM. 2020. EDK-2. https:\/\/gitlab.arm.com\/arm-reference-solutions\/edk2-platforms"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/318774.318944"},{"key":"e_1_2_1_6_1","unstructured":"BlueHat. 2019. Memory corruption is still the most prevalent security vulnerability. https:\/\/www.zdnet.com\/article\/microsoft-70-percent-of-all-security-bugs-are-memory-safety-issues\/"},{"key":"e_1_2_1_7_1","unstructured":"Checked C. 2024. 3C: Semi-automated conversion of C code to Checked C. https:\/\/github.com\/checkedc\/checkedc-clang\/blob\/main\/clang\/docs\/checkedc\/3C\/README.md"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908). USENIX Association, USA. 209\u2013224."},{"key":"e_1_2_1_9_1","unstructured":"Checked C. 2024. The Checked C. https:\/\/github.com\/checkedc\/checkedc"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Sourag Cherupattamoolayil. 2025. Adding Spatial Memory Safety to EDK II through Checked C (Artifact). https:\/\/doi.org\/10.5281\/zenodo.15450480 10.5281\/zenodo.15450480","DOI":"10.5281\/zenodo.15450480"},{"key":"e_1_2_1_11_1","unstructured":"DARPA. 2024. Translating All C to Rust. https:\/\/www.darpa.mil\/program\/translating-all-c-to-rust"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SecDev45635.2020.00018"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Archibald Samuel Elliott Andrew Ruef Michael Hicks and David Tarditi. 2018. Checked C: Making C Safe by Extension. In 2018 IEEE Cybersecurity Development (SecDev). 53\u201360. https:\/\/doi.org\/10.1109\/SecDev.2018.00015 10.1109\/SecDev.2018.00015","DOI":"10.1109\/SecDev.2018.00015"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.039"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586046"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485498"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2016.7783743"},{"key":"e_1_2_1_18_1","unstructured":"Forescout. 2020. AMNESIA:33 \u2013 Foresout Research Labs Finds 33 New Vulnerabilities in Open Source TCP\/IP Stacks. https:\/\/www.forescout.com\/blog\/amnesia33-forescout-research-labs-finds-33-new-vulnerabilities-in-open-source-tcp-ip-stacks\/"},{"key":"e_1_2_1_19_1","unstructured":"Unified EFI Forum. 2025. Unified Extensible Firmware Interface (UEFI) Board. https:\/\/uefi.org\/board"},{"key":"e_1_2_1_20_1","unstructured":"Unified EFI Forum. 2025. Unified Extensible Firmware Interface (UEFI) Specification. https:\/\/uefi.org\/specifications"},{"key":"e_1_2_1_21_1","unstructured":"Iv\u00e1n Arce Francisco Falcon. 2024. PixieFail: Nine vulnerabilities in Tianocore\u2019s EDK II IPv6 network stack.. https:\/\/blog.quarkslab.com\/pixiefail-nine-vulnerabilities-in-tianocores-edk-ii-ipv6-network-stack.html"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2023.3329667"},{"key":"e_1_2_1_23_1","unstructured":"Dominik Harmim Vladim\u0131r Marcin and Ondrej Pavela. 2019. Scalable static analysis using facebook infer. I VI-B."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00069"},{"key":"e_1_2_1_25_1","unstructured":"Jiewen Yao Vincent J. Zimmer and Jian Wang. 2020. A Tour Beyond BIOS - Security Enhancement to Mitigate Buffer Overflow in Unified Extensible Interface (UEFI). https:\/\/tianocore-docs.github.io\/ATBB-Mitigate_Buffer_Overflow_in_UEFI\/draft\/"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the General Track of the Annual Conference on USENIX Annual Technical Conference (ATEC \u201902)","author":"Jim Trevor","year":"2002","unstructured":"Trevor Jim, J. Greg Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A Safe Dialect of C. In Proceedings of the General Track of the Annual Conference on USENIX Annual Technical Conference (ATEC \u201902). USENIX Association, USA. 275\u2013288. isbn:1880446006"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 13th Conference on USENIX Security Symposium -","volume":"13","author":"Johnson Rob","year":"2004","unstructured":"Rob Johnson and David Wagner. 2004. Finding user\/kernel pointer bugs with type inference. In Proceedings of the 13th Conference on USENIX Security Symposium - Volume 13 (SSYM\u201904). USENIX Association, USA. 9."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510454.3528640"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICBDSS51270.2020.00033"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527322"},{"key":"e_1_2_1_32_1","unstructured":"Lloyd Markle. [n. d.]. Experiences in a Real World Application of Cyclone: A Type-safe Dialect of C."},{"key":"e_1_2_1_33_1","unstructured":"Alex Matrosov. 2023. The Untold Story of the BlackLotus UEFI Bootkit. https:\/\/www.binarly.io\/posts\/The_Untold_Story_of_the_BlackLotus_UEFI_Bootkit\/index.html"},{"key":"e_1_2_1_34_1","unstructured":"Medium. 2023. Ownership and Borrowing in Rust: A Comprehensive Guide. https:\/\/medium.com\/@TechSavvyScribe\/ownership-and-borrowing-in-rust-a-comprehensive-guide-1400d2bae02a"},{"key":"e_1_2_1_35_1","unstructured":"Microsoft. 2025. EDK-2. https:\/\/github.com\/microsoft\/mu"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00023"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542504"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1837855.1806657"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065887.1065892"},{"key":"e_1_2_1_40_1","unstructured":"NVIDIA. 2022. EDK-2. https:\/\/github.com\/NVIDIA\/edk2"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3443420"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186041"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1809028.1806598"},{"key":"e_1_2_1_44_1","unstructured":"Rust. 2025. Rust Programming Language. https:\/\/www.rust-lang.org\/"},{"key":"e_1_2_1_45_1","unstructured":"Rust. 2025. Understanding Ownership. https:\/\/doc.rust-lang.org\/book\/ch04-00-understanding-ownership.html"},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the 2012 USENIX Conference on Annual Technical Conference (USENIX ATC\u201912)","author":"Serebryany Konstantin","year":"2012","unstructured":"Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitry Vyukov. 2012. AddressSanitizer: A Fast Address Sanity Checker. In Proceedings of the 2012 USENIX Conference on Annual Technical Conference (USENIX ATC\u201912). USENIX Association, USA. 28."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1030083.1030124"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","unstructured":"Md Shafiuzzaman Achintya Desai Laboni Sarker and Tevfik Bultan. 2024. UEFI Vulnerability Signature Generation using Static and Symbolic Analysis. https:\/\/doi.org\/10.48550\/arXiv.2407.07166 arxiv:arXiv:2407.07166. 10.48550\/arXiv.2407.07166","DOI":"10.48550\/arXiv.2407.07166"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3690275"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3589610.3596271"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00010"},{"key":"e_1_2_1_52_1","unstructured":"Binarly Research Team. 2023. Finding LogoFAIL: The Dangers of Image Parsing During System Boot. https:\/\/binarly.io\/posts\/finding_logofail_the_dangers_of_image_parsing_during_system_boot\/"},{"key":"e_1_2_1_53_1","unstructured":"Tianocore. 2019. EDK II new feature staging. https:\/\/github.com\/tianocore\/edk2-staging\/tree\/edkii-rust"},{"key":"e_1_2_1_54_1","unstructured":"Tianocore. 2022. Function Definition Layout. https:\/\/tianocore-docs.github.io\/edk2-CCodingStandardsSpecification\/draft\/5_source_files\/57_c_programming.html##57-c-programming"},{"key":"e_1_2_1_55_1","unstructured":"Tianocore. 2022. Tasks Add Rust Support to EDK II. https:\/\/github.com\/tianocore\/tianocore.github.io\/wiki\/Tasks-Add-Rust-Support-to-EDK-II"},{"key":"e_1_2_1_56_1","unstructured":"Tianocore. 2025. EDK-2. https:\/\/github.com\/tianocore\/edk2"},{"key":"e_1_2_1_57_1","unstructured":"Tianocore. 2025. EDK-2 Platforms. https:\/\/github.com\/tianocore\/edk2-platforms"},{"key":"e_1_2_1_58_1","unstructured":"Tianocore. 2025. EDK-2 pytool Library. https:\/\/github.com\/tianocore\/edk2-pytool-library"},{"key":"e_1_2_1_59_1","unstructured":"Nicole Tietz-Sokolskaya. 2023. Why Rust\u2019s learning curve seems harsh and ideas to reduce it. https:\/\/ntietz.com\/blog\/rust-resources-learning-curve\/"},{"key":"e_1_2_1_60_1","unstructured":"CVE Trends. 2021. CVE trends. https:\/\/www.cvedetails.com\/vulnerabilities-by-types.php"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3055386.3055397"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2023.3236542"},{"volume-title":"https:\/\/en.wikipedia.org\/wiki\/Ripple20","key":"e_1_2_1_63_1","unstructured":"Wikipedia. 2024. Ripple20. https:\/\/en.wikipedia.org\/wiki\/Ripple20"},{"key":"e_1_2_1_64_1","unstructured":"Jiewen Yao. 2022. SecurityEx. https:\/\/github.com\/jyao1\/SecurityEx"},{"key":"e_1_2_1_65_1","unstructured":"Jiewen Yao Vincent J. Zimmer and Matt Fleming. 2016. A Tour Beyond BIOS Memory Map and Practices in UEFI BIOS. https:\/\/raw.githubusercontent.com\/tianocore-docs\/Docs\/master\/White_Papers\/A_Tour_Beyond_BIOS_Memory_Map_And_Practices_in_UEFI_BIOS_V2.pdf"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179421"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833723"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.3199"},{"key":"e_1_2_1_69_1","volume-title":"Proceedings of the 22nd USENIX Conference on Security (SEC\u201913)","author":"Zeng Bin","year":"2013","unstructured":"Bin Zeng, Gang Tan, and \u00dalfar Erlingsson. 2013. Strato: a retargetable framework for low-level inlined-reference monitors. In Proceedings of the 22nd USENIX Conference on Security (SEC\u201913). USENIX Association, USA. 369\u2013382. isbn:9781931971034"},{"key":"e_1_2_1_70_1","doi-asserted-by":"crossref","unstructured":"Hanliang Zhang Cristina David Yijun Yu and Meng Wang. 2023. Ownership Guided C to\u00a0Rust Translation. In Computer Aided Verification Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland Cham. 459\u2013482. isbn:978-3-031-37709-9","DOI":"10.1007\/978-3-031-37709-9_22"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586038"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3728929","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3728929","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T16:53:05Z","timestamp":1752684785000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3728929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,22]]},"references-count":71,"journal-issue":{"issue":"ISSTA","published-print":{"date-parts":[[2025,6,22]]}},"alternative-id":["10.1145\/3728929"],"URL":"https:\/\/doi.org\/10.1145\/3728929","relation":{},"ISSN":["2994-970X"],"issn-type":[{"type":"electronic","value":"2994-970X"}],"subject":[],"published":{"date-parts":[[2025,6,22]]}}}