Operating system (OS) kernels play a critical role in computer systems by virtually having complete control over the systems. OS kernels not only manage hardware and system resources, but also provide services and protection. Given these tasks, OS kernels have to process external untrusted inputs and perform complicated operations, both of which are error-prone. To avoid entering into erroneous states, OS kernels tend to enforce a large number of security checks---"if" and "switch" statements that are used to validate states. Unfortunately, security checks themselves are often buggy. In particular, a security check may be missing or incomplete, be placed in an improper location, target a wrong variable, etc. Buggy security checks often cause critical security impact because the intended validation for potential errors can be void. This project aims to systematically investigate security checks in OS kernels, to automatically identify security checks, and to develop a set of new techniques to detect the common classes of security-check bugs. This project is expected to effectively find a potentially large number of previously unknown security-check bugs in widely used OS kernels, and thus to significantly improve the security of computer systems with billions of users. The broader educational activities of this project include integrating research with outreach, organizing Capture The Flag competitions among universities and industries in Minnesota, and developing courses for training interdisciplinary and underrepresented students. The goal of this project is to systematically investigate security checks and effectively detect the common and critical security-check bugs in popular OS kernels, including the Linux kernel, the Android kernel, the FreeBSD kernel, Darwin-XNU (MacOS), and ReactOS (Windows-like). The project is comprised of two main research thrusts: (1) identifying security checks and (2) detecting security-check bugs. Both research thrusts are challenging because they require the understanding of code semantics and contexts, and even developer logic. Therefore, this project develops a set of semantic-and context-aware approaches. This project also enhances existing techniques such as fuzzing and symbolic execution to effectively and scalably detect security-check bugs. Multiple general techniques developed in this project, such as accurately finding indirect-call targets, identifying semantically-similar peer code paths, modeling OS-kernel boundary, would also advance future research on systems analysis and protection.
SaTC: CORE: Small: Checking Security Checks in OS Kernels