Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Last modified: Wed Nov 13 02:47:06 2019 GMT.
AbstractThe 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 the 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 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.
PublishedIn Proc. 47th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'20), New Orleans, LA, January 2020. Published as Proceedings of the ACM on Programming Languages (PACMPL), Volume 4, Number POPL, Article 20 (January 2020), 31 pages.
Copyright © 1996-2019 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science