Refactoring the FreeBSD Kernel with Checked C

Most modern operating system kernels are written in C, making them vulnerable to buffer overflow and buffer over-read attacks. Microsoft has developed an extension to the C language named Checked C which provides new source language constructs that allow the compiler to prevent NULL pointer dereferences and spatial memory safety errors through static analysis and run-time check insertion. We evaluate the use of Checked C on operating system kernel code by refactoring parts of the FreeBSD kernel to use Checked C extensions. We describe our experience refactoring the code that implements system calls and UDP and IP networking. We then evaluate the refactoring effort and the performance of the refactored kernel. It took two undergraduate students approximately three months to refactor the system calls, the network packet (mbuf) utility routines, and parts of the IP and UDP processing code. Our experiments show that using Checked C incurred no performance or code size overheads.