Adding Spatial Memory Safety to EDK II through Checked C (Experience Paper)
Published in ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2025), 2025
Recommended citation: Sourag Cherupattamoolayil, Arunkumar Bhattar, Connor Glosner, Aravind Machiry. "Adding Spatial Memory Safety to EDK II through Checked C (Experience Paper)." ISSTA 2025. https://cglosner.github.io/files/Converting_EDK_II_to_Checked_C_with_3C.pdf
We extended 3C — an automated Checked C conversion tool — to operate within UEFI’s freestanding environment. This required redesigning bounds models, annotations, and runtime assumptions so that type-safe code could compile and execute within firmware constraints. The results show that strong, automated memory-safety guarantees are achievable even in early-boot software.