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

操作系统（OS）内核是计算机系统的核心。它几乎控制着系统中的一切，因此是系统中最重要的部分。现代操作系统内核已经变得极其庞大和复杂，包含了数千万行代码。因此，它们往往有大量的错误，这些错误不仅是由开发人员引入的，而且是由编译器引入的。内核错误对安全性尤其重要，因为内核中的单个错误可能会破坏整个系统。因此，检测和消除操作系统内核中的错误是必要的。然而，这是非常具有挑战性的，因为操作系统内核充满了难以分析的代码构件，并且错误的形式多种多样，很难指定用于检测。该项目旨在通过提出一套新的方法和技术，并通过在精确的全内核分析系统中实现它们，来对抗开发人员和编译器引入的错误。该项目预计将提高广泛使用的计算机系统的安全性，保护用户数据和隐私，并推进安全、系统、编译器和软件工程领域的知识。此外，最终的系统将集成到教育工具中，以帮助提高学生对错误的认识，并提高他们编写安全和正确代码的技能。该项目分为三个研究重点。(1)利用基础技术实现精确的全核分析。该项目首先旨在解决多个重要问题，例如普遍存在的手写汇编和整体特性，这些问题一直阻碍着精确的全核分析。(2)通过多种新的对等检查技术检测语义错误甚至不安全的功能设计。这些技术最大限度地减少了对检测中具有挑战性的语义理解和错误规范的需求，并期望将对等检查转变为强大而通用的错误检测方法。(3)发现和消除编译器引入的安全错误。编译器倾向于关注语义正确性，而忽略安全状态，从而导致安全错误。这个任务的目的是创建一个新的内存模型来捕获安全状态，以及一个新的oracle来确定编译器引入的安全错误。除了检测错误外，这个项目的一般方法和技术也将促进未来对计算机系统分析和保护的研究。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.