Checked C for UEFI Firmware
Compiler-Based Vulnerability Prevention for Firmware
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.
Key Contributions
- Redesigned bounds models and annotations for UEFI's freestanding compilation environment
- Enabled automated memory-safety guarantees for early-boot software
- Demonstrated that strong, automated spatial memory safety is achievable even in firmware
- Published as an Experience Paper at ISSTA 2025
Technologies
C, Checked C, 3C, LLVM/Clang, EDK-II/UEFI