权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

CAREER: Modal Abstractions of Systems Concepts for OS Kernel Verification

职业：操作系统内核验证的系统概念的模态抽象

基本信息

批准号：
1844964
负责人：
Colin Gordon
金额：
$ 57.99万
依托单位：
Drexel University
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2019
资助国家：
美国
起止时间：
2019-09-01 至 2025-08-31
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1844964&HistoricalAwards=false
关键词：
CAREER Modal Abstractions Systems Concepts

项目摘要

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.

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