SaTC: CORE: Small: Checking Security Checks in OS Kernels

操作系统（OS）内核在计算机系统中起着至关重要的作用，它实际上完全控制着整个系统。操作系统内核不仅管理硬件和系统资源，还提供服务和保护。考虑到这些任务，操作系统内核必须处理外部不受信任的输入并执行复杂的操作，这两者都容易出错。为了避免进入错误的状态，操作系统内核倾向于强制执行大量的安全检查——“if”和“switch”语句用于验证状态。不幸的是，安全检查本身经常是错误的。特别是，安全检查可能缺失或不完整，可能放置在不适当的位置，可能针对错误的变量，等等。错误的安全检查通常会导致严重的安全影响，因为对潜在错误的预期验证可能无效。本项目旨在系统地研究操作系统内核中的安全检查，自动识别安全检查，并开发一套新技术来检测常见的安全检查错误。该项目有望有效地发现广泛使用的操作系统内核中潜在的大量以前未知的安全检查错误，从而显著提高拥有数十亿用户的计算机系统的安全性。该项目的更广泛的教育活动包括将研究与外展相结合，在明尼苏达州的大学和行业中组织“夺旗”比赛，以及为培训跨学科和代表性不足的学生开发课程。该项目的目标是系统地调查安全检查并有效地检测流行操作系统内核中常见和关键的安全检查错误，包括Linux内核，Android内核，FreeBSD内核，Darwin-XNU （MacOS）和ReactOS（类windows）。该项目由两个主要的研究重点组成：(1)识别安全检查和(2)检测安全检查错误。这两个研究重点都具有挑战性，因为它们需要理解代码语义和上下文，甚至是开发人员的逻辑。因此，该项目开发了一套语义和上下文感知方法。该项目还增强了现有的技术，如模糊测试和符号执行，以有效地、可扩展地检测安全检查错误。在这个项目中开发的多种通用技术，如准确地找到间接调用目标，识别语义相似的对等代码路径，建模操作系统内核边界，也将推进系统分析和保护的未来研究。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.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.