CAREER: Modal Abstractions of Systems Concepts for OS Kernel Verification

操作系统(OS)是协调其他应用程序之间的硬件共享(例如无冲突地共享内存)、提供硬件的高级抽象以及包括用于常见程序任务(例如从磁盘存储和检索文件)的可重用功能的软件系统。由于它们可以控制其他程序并协调硬件资源的使用，因此操作系统代码中的缺陷可能会危及操作系统上运行的任何软件的可靠性或安全性。大多数计算机只运行少数几个通用操作系统之一，因此这些系统中的任何一个系统中的一个漏洞都可能会影响到非常多的计算机，这使得它们的正确性对于世界各地日常使用的无数基于计算机的系统至关重要。这个项目探索了新的方法来从数学上证明操作系统的正确性属性，从而最终确定操作系统中不可能存在错误。该项目的创新之处在于专注于验证与工业中使用的操作系统设计类似的现实操作系统设计，处理操作系统对硬件控制的重要细微之处，以及指定低级代码中常见设计模式的正确性的新方法。该项目的影响是为低级代码引入了新的验证技术，预计这些技术将比操作系统适用得更广泛，并与教育相结合。该项目开发了本科自动机和可计算性课程教学的新方法，整合了安全和软件验证的现代应用程序，以更好地展示材料的价值，并提高学生的参与度。该项目引入了从模式逻辑到操作系统验证的一系列技术，并试图证明这些技术支持操作系统内核和系统代码中一般发生的三种推理：位置虚拟化(如在虚拟内存管理和写入时复制文件系统中)、缓存(包括硬件存储缓冲区、转换后备缓冲区和操作系统级缓存)，以及单个协议的抽象，以多种不同的方式使用，但以兼容的方式使用(与设备驱动程序框架相关)。该项目构建了多核x86-体系结构的详细模型，包括中断处理、虚拟内存管理和弱内存模型之间交互的详细信息。该项目使用该模型实现了一个遵循标准操作系统设计的小型操作系统(特别是对地址空间、设备驱动程序、虚拟文件系统层和文件系统缓存使用了相同的标准抽象)，并在扩展了新推理原则的Hoare逻辑中验证了操作系统。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Operating systems (OSes) are software systems that coordinate sharing of hardware between other applications (such as sharing memory without conflict), provide a high-level abstraction of hardware, and include reusable functionality for common program tasks (such as storing and retrieving files from disk). Because they have control over other programs and mediate use of hardware resources, defects in operating system code can compromise the reliability or security of any software running on the OS. Most computers run one of just a few general-purpose operating systems, so a bug in any one of those systems will likely affect very many computers, making their correctness critical to countless computer-based systems used daily around the world. This project explores new ways to mathematically prove correctness properties of operating systems, and thereby to establish conclusively the impossibility of bugs in them. The project's novelties are a focus on verifying realistic OS designs similar to those used in industry, treating significant subtleties of OS control over hardware, and new approaches to specifying correctness for common design patterns in low-level code. The project's impacts are the introduction of new verification techniques for low-level code that are expected to apply more broadly than to operating systems, and integration with education. The project develops new ways of teaching undergraduate automata and computability courses, integrating modern applications from security and software verification to better demonstrate the material's value and improve student engagement. The project brings a range of techniques from modal logic to bear on OS verification, and attempts to show that these techniques support three kinds of reasoning that occur in operating system kernels and systems code in general: location virtualization (as in virtual-memory management and copy-on-write filesystems), caching (including hardware store buffers, translation lookaside buffers, and OS-level caches), and abstraction of a single protocol to be used in multiple different ways but in a compatible manner (as relevant to device driver frameworks). The project constructs a detailed model of the multicore x86-64 architecture, including details of interactions between interrupt handling, virtual memory management, and weak memory models. The project uses the model to implement a small OS following standard OS designs (in particular, using the same standard abstractions for address spaces, device drivers, the virtual filesystem layer, and filesystem caching), and verifies the OS in a Hoare logic extended with new reasoning principles.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.