CAREER: Whole-Kernel Analysis Against Developer- and Compiler-Introduced Errors

An operating system (OS) kernel is the heart of a computer system. It controls virtually everything in the system and thus is the most important part of the system. Modern OS kernels have become extremely large and complex, containing tens of millions of lines of code. As such, they tend to have a large number of errors that are introduced by not only developers but also compilers. Kernel errors are particularly security-critical because a single error in the kernel may break the whole system. Therefore, detecting and eliminating errors in OS kernels is imperative. This is however very challenging because OS kernels are full of hard-to-analyze code artifacts, and the errors take diverse forms and are hard to be specified for detection. This project aims to combat both developer- and compiler-introduced errors by proposing a set of new approaches and techniques, and by realizing them in a precise, whole-kernel analysis system. The project is expected to improve the security of widely used computer systems, to protect user data and privacy, and to advance the knowledge in the fields of security, systems, compilers, and software engineering. In addition, the resulting system will be integrated into educational tools to help raise student awareness of errors and also to improve their skills in writing secure and correct code.

The project is structured into three research thrusts. (1) Enabling precise whole-kernel analysis with foundational techniques. This project first aims to tackle multiple important problems, such as the prevalent hand-written assembly and the monolithic nature, that have been impeding precise whole-kernel analysis. (2) Detecting semantic errors and even insecure function designs through multiple new peer-checking techniques. These techniques minimize the needs for the challenging semantic understanding and error specification in detection, and expect to turn peer-checking into a powerful and generic error-detection approach. (3) Discovering and eliminating compiler-introduced security errors. Compilers tend to focus on semantic correctness but overlook security states, leading to security errors. This thrust aims to create a new memory model to capture security states, and a new oracle to determine security errors introduced by compilers. In addition to detecting errors, the generic approaches and techniques of this project would also advance future research on the analysis and protection of computer systems.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.