一句话：提出虚拟时间线抽象，并在 Coq 中验证抢占式调度器实现，使实时内核获得时间与空间隔离。
安全攸关实时系统要求组件间具备空间与时间隔离，其中时间隔离依赖于具体抢占式调度器实现的性质（如及时提供时间片、对抢占不敏感等）。已有工作或只验证调度器抽象模型，或证明的性质不足以建立组件隔离。本文提出一种组合式推理框架，以 virtual timeline（实时调度分析中 supply bound function 的变体）作为抽象，隔离地规定并推理每个组件的调度行为，并证明抽象上的性质可下推到 OS 内核生成的汇编代码。作者在 Coq 中验证了一个扩展自 mCertiKOS 的实时内核，加入用户级抢占、经验证的定时器中断处理程序和实时调度器。结果证明，在排除微架构级时间信道的前提下，该内核在功能正确性之外还满足时间与空间隔离。
The reliability and security of safety-critical real-time systems are of utmost importance because the failure of these systems could incur severe consequences (e.g., loss of lives or failure of a mission). Such properties require strong isolation between components and they rely on enforcement mechanisms provided by the underlying operating system (OS) kernel. In addition to spatial isolation which is commonly provided by OS kernels to various extents, it also requires temporal isolation, that is, properties on the schedule of one component (e.g., schedulability) are independent of behaviors of other components. The strict isolation between components relies critically on algorithmic properties of the concrete implementation of the scheduler, such as timely provision of time slots, obliviousness to preemption, etc. However, existing work either only reasons about an abstract model of the scheduler, or proves properties of the scheduler implementation that are not rich enough to establish the isolation between different components. In this paper, we present a novel compositional framework for reasoning about algorithmic properties of the concrete implementation of preemptive schedulers. In particular, we use virtual timeline , a variant of the supply bound function used in real-time scheduling analysis, to specify and reason about the scheduling of each component in isolation. We show that the properties proved on this abstraction carry down to the generated assembly code of the OS kernel. Using this framework, we successfully verify a real-time OS kernel, which extends mCertiKOS, a single-processor non-preemptive kernel, with user-level preemption, a verified timer interrupt handler, and a verified real-time scheduler. We prove that in the absence of microarchitectural-level timing channels, this new kernel enjoys temporal and spatial isolation on top of the functional correctness guarantee. All the proofs are implemented in the Coq proof assistant.
@article{paperbot527,
title = {Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation},
author = {Mengqi Liu and Lionel Rieg and Zhong Shao and Ronghui Gu and David Costanzo and Jung-Eun Kim and Man-Ki Yoon},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371088}
}