Building Certified Concurrent OS Kernels
Building Certified Concurrent OS Kernels
复制标题
DOI：
10.1145/3356903
复制
发表时间：
2019-10-01
影响因子：
22.7
通讯作者：
Costanzo, David
中科院分区：
文献类型：
--
作者：
Gu, Ronghui;Shao, Zhong;Costanzo, David
操作系统 (OS) 内核构成系统软件的支柱。它们可以对当今计算机的弹性和安全性产生重大影响。最近的努力证明了形式验证简单通用内核的可行性，但他们忽略了并发性的重要问题，其中不仅包括单核上的用户和 I/O 并发性，还包括具有细粒度锁定的多核并行性。在这项工作中，我们提出了 CertiKOS，这是一种用于构建经过验证的并发操作系统内核的新型组合框架。并发允许属于不同抽象层并在不同CPU/线程上运行的程序交错执行。每个这样的层都可以有一组不同的可观察事件。在CertiKOS中，这些层及其可观察事件可以被正式指定，然后每个模块都可以在其所属的抽象级别上进行验证。为了将所有经过验证的部分链接在一起，CertiKOS 对每个这样的部分强制执行所谓的上下文细化属性，该属性规定实现将在具有任何有效交错的任何并发上下文下表现得像其规范。使用 CertiKOS，我们成功开发了一个实用的并发操作系统内核，称为 mC2，并在 Coq 中构建了其正确性的形式证明。 mC2 内核由 6500 行 C 和 x86 汇编语言编写，并在普通 x86 多核机器上运行。据我们所知，这是具有细粒度锁定的通用并发操作系统内核的第一个正确性证明。
Operating system (OS) kernels form the backbone of system software. They can have a significant impact on the resilience and security of today's computers. Recent efforts have demonstrated the feasibility of formally verifying simple general-purpose kernels, but they have ignored the important issues of concurrency, which include not just user and I/O concurrency on a single core, but also multicore parallelism with fine-grained locking. In this work, we present CertiKOS, a novel compositional framework for building verified concurrent OS kernels. Concurrency allows interleaved execution of programs belonging to different abstraction layers and running on different CPUs/ threads. Each such layer can have a different set of observable events. In CertiKOS, these layers and their observable events can be fonnally specified, and each module can then be verified at the abstraction level it belongs to. To link all the verified pieces together, CertiKOS enforces a so-called contextual refinement property for every such piece, which states that the implementation will behave like its specification under any concurrent context with any valid interleaving. Using CertiKOS, we have successfully developed a practical concurrent OS kernel, called mC2, and built the formal proofs of its correctness in Coq. The mC2 kernel is written in 6500 lines of C and x86 assembly and runs on stock x86 multicore machines. To our knowledge, this is the first correctness proof of a general-purpose concurrent OS kernel with fine-grained locking.