一句话：设计并实现 CN——面向系统 C 代码的分离逻辑精化类型系统，并验证 pKVM 组件。
系统软件验证项目与常规开发之间仍存在鸿沟，主要挑战在于处理真实系统代码及其语义的复杂性，以及验证工具的可用性。为此，作者设计并实现 CN：一种面向 C 系统软件的分离逻辑精化类型系统，建立在真实的 ISO C 语义上。CN 将精化类型检查归约为可判定的命题逻辑推理，使用一等资源支持指针别名与指针算术，支持迭代分离合取的资源推断，并通过限制规约中 ghost 变量的语法形式保证其可推断。作者形式化了类型系统关键部分并证明类型检查可靠性，还用 CN 验证了 Google pKVM hypervisor 的一个实质组件，展示了可用性。
Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability. We describe an experiment in verification tool design aimed at addressing some aspects of both: we design and implement CN, a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable propositional logic reasoning, uses first-class resources to support pointer aliasing and pointer arithmetic, features resource inference for iterated separating conjunction, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. We implement CN and formalise key aspects of the type system, including a soundness proof of type checking. To demonstrate the usability of CN we use it to verify a substantial component of Google's pKVM hypervisor for Android.
@article{paperbot2075,
title = {CN: Verifying Systems C Code with Separation-Logic Refinement Types},
author = {Christopher Pulte and Dhruv C. Makwana and Thomas Sewell and Kayvan Memarian and Peter Sewell and Neel Krishnaswami},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571194}
}