Real-time systems often carry out safety-critical operations that require strong timing guarantees. For example, the flight controller of a quadcopter needs to send control signals to its actuators in a timely manner, otherwise, the stability of the quadcopter will not be ensured, potentially leading to a physical crash. Furthermore, this problem is exacerbated by the increasing trend of accommodating multiple software components, not necessarily from the same vendor, onto a single platform. On the one hand, the inevitable and intricate interferences between components make it hard to examine whether a safety-critical component always meets its timing requirements. On the other hand, the co-residence of multiple components gives rise to security issues, such as whether malicious components could infer information from other trusted ones that hold secrets. In this sense, strong isolation between components is of utmost importance to the reliability and security of such systems.
A real-time system usually relies on an operating system (OS) kernel to manage and schedule all its application-level constituent components, and it is the responsibility of the OS kernel to enforce strong isolation between these components.
Traditionally, OS kernels emphasize mostly spatial isolation [Costanzo et al. 2016;Murray et al. 2013;Sigurbjarnarson et al. 2018]. Thanks to hardware mechanisms such as virtual memory, and by carefully managing resources such as memory quotas and process IDs in software, an OS kernel provides to each component an illusion of exclusive access to memory and various kernel objects, free from interferences of other components.
However, isolation in the context of real-time systems also relies heavily on temporal isolation, which means that a component's capability to meet its temporal constraints is not influenced by the behavior of others. At minimum, an OS kernel should take advantage of hardware mechanisms such as timer interrupts to preempt a component from monopolizing the CPU time. On top of preemption, ideally, an OS kernel should also enforce temporal isolation at both the microarchitectural level and the algorithmic level.
Temporal isolation at the microarchitectural level. Due to the complexity of modern hardware, components may interfere with each other through shared cache lines, memory banks, etc., also known as microarchitectural level timing channels. For example, when two components share a common cache line, the execution of one of them might affect the execution time of the other one, thus jeopardizing the other's capability of meeting timing constraints. Existing work [Ge et al. 2019;Sha et al. 2016] mitigate this problem by partitioning physical resources properly so as to reduce the non-deterministic temporal behavior due to sharing between components.
Another aspect is the analysis of interrupt latency and context switch overhead. The OS kernel relies on timer interrupts to allocate time resource. Even though interrupts occur periodically, their handling may be delayed if the system is in an uninterruptible state, and the context switch overhead also influences the actual execution time allocated to the scheduled task. Existing work [Blackham et al. 2011;Sewell et al. 2017] conduct worst-case execution time analysis on the OS kernel to compute a bound on both the interrupt latency and kernel overhead, so that users of the system may compensate for this loss of execution time by declaring a larger budget for their tasks.
Temporal isolation at the algorithmic level. Temporal isolation also relies heavily on the scheduler to properly allocate time slots (i.e., the duration between successive interrupts) so that every component meets its temporal constraints. Such reasoning requires examining algorithmic properties of the concrete schedule, which describes the exact time slots a task occupies. For example, to reason about the schedulability of a real-time task, one must check whether this task is scheduled for its budgeted number of time slots during each period (see Sec. 2.2). This problem has not been fully addressed by existing work, and it is the main focus of this work.
Temporal isolation at the algorithmic level is essential for establishing isolation between components in an OS kernel. It relies heavily on reasoning about algorithmic properties of the concrete implementation of a preemptive scheduler, which is challenging in the following ways.
Formalizing algorithmic properties of the scheduler implementation remains a challenge. Despite the rich literature in formal verification of real-time OS kernels [Andronick et al. 2016;Xu et al. 2016], most of them stop at the policy level, such as proving that the running task always has the highest priority among ready ones, or proving that there is no priority inversion. These policy-level properties are not strong enough to prove algorithmic properties of the scheduler implementation. For example, the schedulability of a task states that the task never misses its deadline even in the worst-case, which requires more sophisticated algorithmic reasoning than merely showing that the scheduled task indeed has the highest priority.
Algorithmic reasoning requires decomposition despite interferences between components. One important aspect of temporal isolation is schedulability, whose verification requires proving that tasks do not prevent each other from receiving sufficient execution time as long as they have passed a certain schedulability test. However, in most cases, the temporal behavior of a task inevitably depends on the behavior of others. For example, in fixed-priority scheduling (see Sec. 2.2), the schedule of a task is influenced by when and how long higher priority tasks execute. As a result, the OS kernel needs to enforce budget constraints on each task so that no task can monopolize the CPU time. On the other hand, a schedulability proof is needed to justify the sufficiency of those budget constraints. This intertwining makes it difficult to scale the formal reasoning without a proper abstraction of the interferences.
Partitioned scheduling brings more complexity. On top of the above challenges for flattened (i.e., task-level) scheduling, reasoning about more sophisticated policies such as partitioned scheduling [Davis and Burns 2005] brings more complexity. For example, in the QNX real-time OS [QNX 2019] and the framework presented in Kim et al. [2015], tasks are scheduled following a global priority, yet they are also subject to partition budgets. In this way, the schedule of a task is influenced by tasks both within the same partition and from other partitions, making the reasoning hard to scale. Furthermore, the isolation between components also requires that the local schedule of tasks in a partition be independent of other partitions, which adds more proof obligations to the algorithmic reasoning about the scheduler.
This paper studies isolation properties of real-time OS kernels. In particular, we focus on formal reasoning about algorithmic properties of the concrete implementation of a preemptive scheduler, and make the following contributions to address the above challenges. Our work is formalized in Coq and built on top of CertiKOS [Costanzo et al. 2016;Gu et al. 2015].
• A novel application of supply and demand functions [Liu 2000], called virtual timelines, to describe temporal properties of real-time tasks and connect them with the actual code. In this way, all high-level properties proved on this abstraction carry down to the generated assembly code of the system. • A novel approach that uses virtual timelines to address the isolation property of a component's schedule. For flattened fixed-priority scheduling, we prove that a task's schedule is independent of the behavior of lower-priority tasks. For partitioned scheduling, we prove that the local schedule of tasks in a partition is independent of other partitions. • A compositional framework to reason about algorithmic properties (e.g. schedulability)
of each component's schedule in isolation. In particular, we propose a way to statically encapsulate interferences from other components in the system, and we show how to reason about a component as if it were running on its own virtual timeline. • Combining all of these together, we present a fully verified OS kernel with both temporal and spatial isolation using our compositional framework.
How does this work relate to microarchitectural level details? This work focuses on algorithmic properties of the scheduler implementation, which is orthogonal to the microarchitectural level details. For instance, we rely on the user to declare a suitable budget for each task, without worrying about whether the given budget is sufficient or not. However, we believe our work integrates easily with verification on the microarchitectural level issues, such that if both efforts are successful, the user is guaranteed the exact number of time slots per period, and also guaranteed that her task indeed finishes within these time slots.
Are properties proved in this work specified in clock time? Properties proved in this work, such as schedulability of a task, are specified in discrete logical time, i.e. in units of time slots (or equivalently, number of timer interrupts). This makes sense under the assumption that timer interrupts are strictly periodic, and that the interrupt latency and context switch overhead are negligible so that a task is guaranteed the full amount of time for its execution between successive interrupts. We believe our work is flexible enough to integrate with trustworthy worst-case execution time analysis of kernel services so that these assumptions could be relaxed and these overheads could be compensated properly when a user declares the budget of a task.
Reusability of the virtual timeline abstraction. This paper uses CertiKOS as an example to demonstrate the power of virtual timelines in a concrete OS kernel. However, our technique is reusable in other systems. In fact, our approach gives a novel mechanized formal semantics for algorithmic behaviors of preemptive scheduling, which allows us to reason about various isolation properties, such as schedulability, obliviousness to other components, etc. More importantly, we show how to instantiate this semantics with a concrete runtime system, which in this case means the concrete implementation of a real-time scheduler, in a structured way (detailed in Sec. 2.1). Once it is proved that the system indeed implements this scheduling semantics, all high-level properties proved on the virtual timeline abstraction carry down to the generated assembly code.
Roadmap of the Paper. Sec. 2 gives an overview of our reasoning framework for algorithmic properties and introduces the concept of virtual timelines. Sec. 3 discusses how to reason about algorithmic properties of a component's schedule using the virtual timeline. Sec. 4 describes how we connect virtual timelines with the concrete implementation of a preemptive scheduler in an OS kernel, such that all properties proved on the virtual timeline carry down to the actual code of the system. Section 5 and Section 6 discuss proof efforts and limitations of our work. Sections 7 and 8 discuss the related work and then conclude.
This section gives an overview of our reasoning framework for algorithmic properties of the scheduler in real-time systems. We first explain how this framework fits in the overall verification of an OS kernel. We then describe in more detail the idea of virtual timelines, as well as the computation of virtual time maps.
Our work builds on top of the sequential version of CertiKOS, known as mCertiKOS [Costanzo et al. 2016;Gu et al. 2015], a verified single-core OS kernel with a cooperative round-robin scheduler.
In the rest of this paper, when we refer to CertiKOS we generally mean this specific version of mCertiKOS. The CertiKOS approach adopts a layered approach for building specifications for the OS kernel, and obtains a formal contextual refinement proof between the high-level specification and low-level implementation of the kernel: a program linked with the kernel implementation and running on top of the x86 assembly semantics exhibits the same behavior as the same program running on top of the assembly semantics plus high-level specifications of system calls.
As shown in Fig. 1, we make the following extensions on top of the original CertiKOS:
(0) We extend the cooperative CertiKOS with user-level preemption and a real-time scheduler, and prove functional correctness of its implementation following a layered approach. We prove that the C implementation of the scheduler, sched (enclosed in an orange rectangle), faithfully implements its Coq specification, abs_sched.
(1) We introduce a virtual timeline for each task (denoted vt p for task τ p ) to specify and prove algorithmic properties of a task's schedule. See Def. 3.1 and Cor. 3.3 for more details. (2) We introduce a virtual-time-based scheduler, vt_sched, that operates on each task's virtual timeline to decide its schedule. We then prove that the concrete scheduler in the OS, abs_sched, faithfully implements vt_sched.
(3) We connect a task's virtual timeline with its concrete schedule by proving that vt_sched schedules this task in the exact same way as indicated by its virtual timeline. See Lemma 4.2 as an example. Combining everything together, on top of the functional correctness guarantee of the scheduler, we obtain algorithmic properties for each task's schedule, which are formally connected to the concrete schedule produced by the scheduler in the OS kernel, and which carry down to the generated assembly code of the system.
Also, notice that this framework is not limited to CertiKOS. The abstraction of virtual timelines is generic in specifying and reasoning about fixed-priority scheduling, and it can follow the same approach to connect with other systems employing the same scheduling scheme.
In this section, we explain in more detail intuitions behind virtual timelines, and we use budgetenforcing fixed-priority scheduling as an example. Here, timer interrupts are set up to occur periodically, dividing CPU time into regular time slots. Upon each timer interrupt, its handler invokes the scheduler to decide which task to schedule for the next time slot. We assume that the set of real-time tasks is known ahead of time, denoted as {τ 0 , τ 1 , ..., τ N -1 }. Each task τ p occupies a unique priority level p, with 0 being the highest priority level. When several tasks have the same priority, a simple tie-breaker (e.g. task id) could be adopted without affecting the schedulability of the whole system. A task τ p is specified with (C p , T p ), representing this task's budget and period, respectively. The budget and period are integer values, in units of time slots.
Fig. 2 shows the C implementation of a budget-enforcing fixed-priority preemptive scheduler. In particular, it uses an integer array, quanta, to keep track of the execution time of each task, and makes sure that a task cannot be scheduled for more than its budget in any period. Fig. 3 shows a concrete schedule produced by such a scheduler, from time 0 to 10. On the bottom, we show how the schedules for different tasks are interleaved with each other. And from the top, we show the exact schedule for each task in decreasing order of priority. Here, a down arrow represents the start of a new period. We observe that the number of time slots consumed by a task within each period does not exceed its budget, thanks to the budget-enforcement mechanism. We also observe that the time consumption exactly equals its budget, which is the schedulability of a task: it is guaranteed in each period the full number of execution time slots specified by its budget.
Then, the question is how to formalize algorithmic properties of a task's schedule with isolation in mind. In particular, even though the schedule of tasks interleave with each other, as suggested by both the scheduler implementation and the concrete example, they also follow a strict conceptual Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation 20:7
0 1 2 3 4 5 6 7 8 9 10 0 1 2 3 4 5 6 7 8 9 10 0 1 2 3 4 5 6 7 8 9 10 0 1 2 3 4 5 6 7 8 9 10 0 1 2 3 4 5 6 7 8 9 10 0 1 2 3 4 5 6 7 8 hierarchy. For example, in Fig. 3, the schedule of task τ 0 is regular because it has the highest priority.
Then task τ 1 is scheduled when τ 0 is inactive. Lastly, task τ 2 is scheduled when both τ 0 and τ 1 are inactive. This inspires the concept of virtual timelines. A virtual timeline for a task is intuitively the time łavailablež to the task. A task's virtual time includes all time that is not occupied by higher priority tasks since a task cannot preempt higher priority ones. Notice that the available time to a task may be allocated to this task, or to lower priority ones when this task has finished, or kept idle when there is no task to execute. This idea stems from the time supply and time demand functions, from the original time-demand analysis [Lehoczky et al. 1989;Liu 2000]. The original design sums up the total time demand (budget multiplying the number of periods) across all priorities (required execution time), and compares it with the time supply (global time) to determine the schedulability of a system.
We embrace the idea of comparing supply with demand but change their meaning and the way they are computed. Instead of accumulating demand across priorities, we remove the time used by higher priority tasks by creating holes in the virtual timeline with respect to global time. In Fig. 4, we show the schedule of tasks both on the global timeline (t) and their corresponding virtual timelines (vt p for task τ p ). Notice that the virtual timeline for τ 0 is the same as the global timeline (no holes) as it is the highest priority task. And the virtual timeline for τ 1 is the result of removing all slots occupied by τ 0 from vt 0 . Lastly, vt 2 is the result of removing all schedules of τ 1 from vt 1 .
The benefit of using virtual time is that once we abstract away the time taken by higher priority tasks, the current task becomes the highest priority one in the system, and hence cannot be interrupted. This means we can ignore all tasks with higher priorities and focus only on the current task, effectively creating an illusion of isolation. For example, in Fig. 4, task τ 1 is scheduled immediately after its arrival on the virtual timeline of vt 1 , and finishes when its budget is exhausted. The downside is that the real-time assumptions and requirements (deadlines, periods, etc.) are given in the global timeline and not in the virtual one, and we need to be able to convert global time into virtual time.
As demonstrated in Fig. 4, to ease the reasoning about a task's schedule, we encapsulate interferences from higher-priority tasks in its virtual timeline. This requires a suitable formalization of the virtual timeline that makes it easy to connect a task's schedule in global time to its counterpart in virtual time. We use PT and VT to denote global time and virtual time, respectively. Notice that they are integer values in units of time slots. We use σ p to denote the connection between global and virtual time. There are various alternative ways of defining σ p .
Fig. 6. A concrete time map
(1) σ p : VT → PT. This is a close analogy to the virtual memory mechanism, where the behavior of a process is determined by its virtual memory space, and the OS kernel maintains its page table to make sure that the corresponding physical memory space does not overlap with others. However, such a formalization complicates the reasoning about temporal properties, which are usually specified in the global time. For example, schedulability requires that a task be scheduled for its full budget within each period, yet it is non-trivial to compute which virtual time duration corresponds to a global period using this formalization of virtual timelines.
(2) σ p : VT → VT. This approach reflects our observation in Fig. 4: a task's virtual timeline is the result of taking the virtual timeline of the adjacent higher priority and removing slots already consumed by this high priority task. However, this makes the reasoning tedious because we have to compose multiple time maps to describe one virtual timeline. For example, the virtual timeline of τ 2 is described as
(3) σ p : PT → VT. This is the approach we finally settle on. It takes advantage of the recursive computation as in the second approach, while avoiding the tediousness of composing multiple time maps to describe one virtual timeline. We show the computation of such a time map in the following.
As explained above, we define the time map σ p , a function from global time to virtual time, as a formalization of the virtual timeline for τ p . Fig. 5 demonstrates the general principle of computing time maps, in the form of additional code instruments on top of the sched() function. In particular, vt is a two-dimensional array of integers, where vt
) is allocated to a task p, it is available in the virtual timeline of both this task and all higher priority ones. Fig. 6 shows an example of such vertical computation of time maps.
Although intuitive, this way of vertical computation is inconvenient because the dynamic construction of time maps complicates the reasoning about their properties. Instead, we adopt an equivalent approach of horizontal computation for time maps. In particular, if we know beforehand when each task arrives and what its execution time is, the time map can be pre-computed in the decreasing priority order (we discuss the relaxation of these constraints in Sec. 4.4). This is indeed the case when all tasks are periodic and always use up their budgets. Also, notice that there is only one task per priority level.
In this setting, we know exactly when the highest priority task will be executed (at the start of each of its periods) and thus build its timeline. For example, the time map for τ p+1 can be Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation 20:9 incrementally constructed from the one for task τ p as follows. Below, σ p (t)σ p ( t T p T p ) denotes the available virtual time for τ p since the start of the current period. Notice that the execution time of τ p is also bounded by its budget, C p , and thus its actual time consumption is the minimum of the two. That means, if C p is smaller than σ p (t)σ p ( t T p T p ), task τ p must have finished its execution at time t.
Definition 2.1 (Time map for periodic tasks in fixed-priority scheduling).
time spent in the current period
In this section, we discuss how the abstraction of virtual timelines facilitates the reasoning about algorithmic properties of a component's schedule, with both flattened and partitioned scheduling.
For flattened scheduling, we use fixed-priority scheduling as an example and demonstrate the proof on schedulability and obliviousness to lower priority tasks. For partitioned scheduling, we show how virtual timelines can be used in proving obliviousness to other partitions, and further in proving schedulability of tasks.
In this section, we use fixed-priority scheduling as an example to demonstrate how the virtual timelines could facilitate the reasoning about a task's schedule.
As shown in Fig. 4, the virtual timeline of a task encapsulates interferences from higher priority tasks and allows us to reason about the schedule of this task solely based on its own time map. In particular, on its virtual timeline, a task is scheduled as soon as it arrives, and keeps running until its budget is exhausted.
We use schedulability, which is essential for temporal isolation, as an example to demonstrate how to reason about a task's schedule. Schedulability requires that a task be scheduled for its full amount of budget within each period, despite the worst-case interferences from others. We formalize this property in terms of a task's virtual time.
This is a sufficient and necessary condition for schedulability, which states that a task will receive enough virtual time in each of its physical periods. For example, in Fig. 4, the virtual time available to task τ 1 in its first and second period is 3, which is greater than its budget of 2, so this task is schedulable in the first two periods. Notice that the exact amount of available virtual time varies in different periods, depending on the actual interferences from higher priority tasks. However, thanks to the budget-enforcing mechanism of the scheduler, there is an upper bound on the interference that can be decided statically.
For strictly periodic tasks with no dynamic creation, Liu and Layland [1973]'s seminal work solves the scheduling problem by giving an optimal schedule. The essential observation of their analysis is the critical instant theorem, stated as follows using our virtual time concepts: 0 1 2 3 4 5 6 7 8 9 10 Π = (2, 5) 13) 11 12 13 14 15 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 Π = (2, 5) Fig. 7. Partitioned scheduling 0 1 2 3 4 5 6 0 1 2 3 4 5
This means that a task suffers the most interference (i.e., has the least available time) during its first period, since all higher priority tasks also arrive at time 0. Theorem 3.2 is formalized and proved in Coq, based on the time map computation given by Def. 2.1. An immediate corollary is the schedulability of the full system:
Corollary 3.3. The system is schedulable at all times if each task is schedulable for its first period. Said otherwise,
Partitioned scheduling is another common scheduling paradigm, where the CPU resource is divided among multiple partitions, with each partition hosting its own set of tasks. Partitions are useful for the administration of a system, e.g. applications independently developed by different vendors could be kept in different partitions, so that tasks within a partition are allowed to communicate and cooperate, while they are also free from interference by other partitions.
Each partition Π i is reserved a certain proportion of the CPU resource, specified with a partition budget B i and period P i , i.e., Π i = (B i , P i ). The OS kernel guarantees to schedule this partition for B i time slots in every period, though the exact allocation of these slots may vary depending on the behavior of other partitions. Fig. 7 shows an example of partitioned scheduling. Here, we focus on partition Π 0 , which consists of two tasks, where τ 0 has higher priority over τ 1 . The upper side axis shows the schedule when Π 0 is the only partition in the system. This partition is scheduled periodically, and its tasks are only scheduled when the partition is active. As a comparison, the lower side shows the case when Π 0 is interleaved with Π 1 . Though the partition's exact schedule varies, it is still guaranteed 2 time slots in every period.
Notice that Fig. 8 demonstrates an interesting phenomenon: from the partition's local view, its tasks' schedule varies depending on the exact schedule of this partition. This is caused by the varying task arrival time in this partition's local view, which clearly leads to interferences between partitions. On the one hand, if tasks cooperate with each other in the same partition, the reordering of their schedule might jeopardize its correct operation. On the other hand, the influence from other partitions complicates the temporal property reasoning about the current partition. 0 1 2 3 4 5 6 7 8 9 10 Π " = (2, 5)
) " = (1, 5) ) + = (2, 10) 11 12 13 14 15 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Fig. 10. Another example of local time map for a task
Existing work on isolation properties in partitioned scheduling [Murray et al. 2013] assume a fixed schedule for partitions, and their verification framework does not cover the issue presented in Fig. 8. In this work, we address this issue using the notion of virtual timelines.
In particular, we differentiate different types of virtual timelines as follows. We use PT, VT, and ST to represent the timeline for the global time, a task, and a partition, respectively. All of them are of integer type, in units of time slots. Then we use π, ω and σ for time maps of type parmap, localmap and timemap respectively. Under this notation, π i describes the schedule of partition Π i , σ j describes the schedule of task τ j , and ω j describes the schedule of task τ j in its partition's local view. Fig. 9 demonstrates the general principle of computing time maps with partitioned scheduling, in the form of additional code instruments. Here, the time map and local time map for tasks in Π i are computed in the same way as Fig. 5, with the only exception that the local time map is indexed by the local time of Π i . Virtual time for tasks in other partitions does not increment because the next time slot is not available to them. In the end, we increment the local time of Π i only.
The isolation property requires that the schedule of tasks within Π i does not change no matter how π i is defined, as long as the partition schedule is consistent with its period and budget. We use the vertical computation in Fig. 9 to define ω j . In addition, since this isolation property involves comparing two different executions, we define a canonical local time map for the same task, rewritten ω c j .
Definition 3.4 (The canonical local time map for task τ j ∈ Π i ). We define ω c j as the result of the vertical computation of its local time map, under the setting that Π i is the only partition in the system. In other words, it is computed when the following holds.
This means Π i always occupies the first B i time slots in every period.
The isolation property is defined as below.
Definition 3.5 (The obliviousness of the local schedule of partition Π i ).
This states that the local schedule of tasks within a partition is oblivious to other partitions in the system. Since by definition, σ p = ω p • π i , we obtain an equivalent formalization of this isolation property.
Definition 3.6 (The obliviousness of the local schedule of partition Π i : alternative formalization).
This states that the local schedule within a partition is independent of others, thus even if the partition schedule varies, it only affects the exact time slots taken by this partition, but does not change the ordering of this partition's local schedule. This is analogous to the virtual memory system: we can view ω c p , π i and σ p as the virtual memory space, the page table, and the physical memory space, respectively. Here, ω c p (analogous to the virtual memory space) is decided solely on its own, and the actual allocation of π i and σ p (analogous to the page table and physical memory allocation) are always connected by ω c p , no matter how both of them are influenced by other partitions in the system.
We observe that this obliviousness holds if all tasks have a period that is a multiple of their partition's period. The intuition is that, under such a constrained setting, task arrivals have to occur at the boundary of the partition's period (i.e., 'bound' task [Davis and Burns 2005]), thus their arrival time in the partition's local view does not change. Fig. 10 gives an example of this constrained setting. Here, the periods of tasks in Π 0 always synchronize with the period of the partition, so that the local schedule of tasks are not affected by other partitions in the system.
Further, under this constrained setting, there is a straightforward way of computing ω c p . Observe in Fig. 10 that tasks arrive at local time 0, 2, 4, ..., etc., as if they are still periodic tasks, only with a smaller period. In this case, we define a shrunk period for each task:
Then we assume
, and compute local time map for tasks as follows.
Definition 3.7 (Local time map for periodic tasks with fixed-priority scheduling).
Such obliviousness to other partitions also facilitates the reasoning about schedulability properties. Recall that one of the main difficulties with schedulability analysis is the interference between different components. However, under such a constrained setting, we can transform schedulability, which is specified on the global timeline, into a property on the partition's local timeline, since a task's behavior is only affected by its own partition.
Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation 20:13 Lemma 3.8. The schedulability analysis of task τ p is transformed into reasoning about its local schedule ω p . That is, for any p and k ≥ 0,
Proof. By Def. 3.6, σ p = ω c p • π i . Since the OS kernel guarantees the full amount of schedule for the partition, we can transform a period of T p in the global timeline into a smaller period of
in the partition's local timeline. What's more, the constraint that T p must be a multiple of P i allows us to always match the beginning and the end of the two periods, thus we transform schedulability of a task into the reasoning on its local timeline. □
Section 3 demonstrates the high-level reasoning about a component's schedule on its virtual timeline, which corresponds to step 1 ○ in Fig. 1. In this section, we discuss how to connect temporal properties proved on the virtual timelines with the concrete scheduler implementation of an OS kernel.
In particular, the high-level reasoning is based on schedules over individual virtual timelines, while the concrete scheduler (e.g. Fig. 2) exhibits a global view of the whole system and produces a schedule mixing all components together. For any particular task, the relationship between its schedule in the global view and its schedule in the virtual timeline is demonstrated in Fig. 4. It is challenging to prove such a correspondence directly based on the scheduler implementation. Instead, we use a virtual-time-based scheduler as an intermediate step toward this connection. We first prove that the concrete scheduler is equivalent to the virtual-time-based scheduler (step 2 ○ in Fig. 1). We then prove that for any task, its schedule on the virtual timeline is equivalent to the schedule produced by the virtual-time-based scheduler (step 3 ○ in Fig. 1). Combining both steps together, we connect individual virtual timelines with the concrete scheduler implementation of an OS kernel.
In this section, we first provide background on CertiKOS (Sec. 4.1), and our real-time extension on top of it (Sec. 4.2). We then discuss in detail how we connect virtual timelines with this real-time version of CertiKOS. In particular, we illustrate such a connection under three scheduling scenarios: fixed-priority scheduling with constant execution time (Sec. 4.3), fixed-priority scheduling with variable execution time (Sec. 4.4), and partitioned scheduling (Sec. 4.5).
CertiKOS is a verified kernel whose functional correctness has been mechanized in the Coq proof assistant.
Abstraction layers. CertiKOS carries down its functional correctness guarantees to the assembly level. This is achieved by dividing the kernel into many small pieces that are verified separately, called abstraction layers. Implementation details of lower layers are encapsulated into abstract states and associated primitives in higher layers, thus allowing to reason directly with the specifications rather than the implementations.
We follow this approach in our work to achieve the same level of compositionality, and more importantly, to carry end-to-end guarantees from specifications all the way down to the assembly code.
Notice that temporal properties include safety and liveness. While the former is easily preserved by refinement because high-level invariants also bound the set of possible behaviors of lowlevel code, the latter may not necessarily be preserved in general. However, CertiKOS employs termination-sensitive and observation-preserving refinement, and every system call is proven terminating. Thus, both safety and liveness properties are preserved by refinement in this work.
The machine model. The CertiKOS kernel uses the CompCert compiler [Blazy et al. 2006;Leroy 2009] to propagate the verification done at the C source code level down to the generated assembly code for several architectures (PowerPC, ARM, x86, and RISC-V). (Actually, it is a slightly modified version of CompCert that handles new instructions and abstraction layers which is still verified.) This compiler enjoys a proof of correctness, mechanized in Coq, which ensures that any behavior of the generated assembly code is also an allowed behavior of the source code. This model does not include all hardware features but only those that the compiler actually uses. States of the system are represented as a register set (rs) and a memory state (m) [Leroy et al. 2014].
The CertiKOS machine model builds on top of CompCert's one by extending the memory model with an abstract state that can contain arbitrary information.
The small step operational semantics remains the same with two additions: new instructions and primitives, which are internal functions abstracted as primitive operations, and thus whose execution is seen as a single step instead of as a jump to a function body.
Preemption is essential for multiplexing the processor among multiple processes. Particularly, the ability to preempt a running user process and schedule another one immediately enables us to obtain properties that are not achievable in cooperative systems, such as liveness of any user process.
We replace the cooperative scheduler of CertiKOS with a preemptive one (Fig. 2), and prove its functional correctness following the layered approach (step 0 ○ in Fig. 1). The timer interrupt is set up to occur periodically, and the scheduler is invoked by the timer interrupt handler.
Whenever a timer interrupt occurs, the interrupt handler acknowledges the receipt of the interrupt, and invokes the scheduler to decide whether to preempt the current task and schedule a new one for the next time quantum. This is similar to FreeRTOS, which also uses a constant-rate (or auto-reload) timer for scheduling. We leave the optimization of using one-shot timer for future work, since it is orthogonal to the formal reasoning in this work.
Verified interrupt handler. In addition to the preemptive scheduler, we also verify the interrupt handler which invokes it. This requires extending the machine model with an interrupt mechanism.
After each instruction, a processor checks the interrupt line to decide whether it is going to execute the next instruction or to jump to an interrupt handler. The original CertiKOS machine model only covers synchronous exceptions, e.g. page faults, but not external interrupts. We model this behavior by a 2-step process at each instruction: first, we detect interrupts with an abstract function intr_trigger, then we handle them using an abstract interrupt handler intr_handler that dispatches execution to the corresponding interrupt handler if there is a pending interrupt.
We only model the timer interrupt in this way, since polling for other device interrupts is the typical behavior for high-assurance systems [Murray et al. 2013;Sigurbjarnarson et al. 2018]. Nevertheless, our interrupt mechanism is general enough to extend to any kind of device interrupts.
Restriction to the user mode. In order to keep the modifications to the existing verification proofs of CertiKOS to a minimum, we only allow interrupts in user mode. This way, all the proofs about the kernel do not need to be modified since the assembly semantics in kernel mode has not changed.
• There is no new arrival of higher priority tasks. That is, ∀j < p, t mod T p 0. This corresponds to the first loop in Fig. 2. When a new period starts, the quantum value will be reset to this task's budget. • Task τ p still has remaining budget, or a new period is arriving. That is, quanta [p] > 0 ∨t mod T p = 0. Similarly, if vt_sched schedules τ p at time t, the following must hold, and vice versa:
• For each higher priority task τ j , VTA (σ j , t) = 0.
• VTA (σ p , t) = 1. This indicates that the connection between abs_sched and vt_sched relies on the relation between a task's virtual time and its current quantum value. In particular, we observe in Fig. that a task's quantum is decremented along with the increment in its virtual time, and is eventually depleted so that this task won't be scheduled until the next period. To put it formally, we prove the lemma below to facilitate the refinement proof between abs_sched and vt_sched.
Definition 4.1. Equivalence between states of the abstract scheduler and the virtual-time-based scheduler
It means that whenever the concrete scheduler finishes scheduling, the remaining quanta is the budget minus the elapsed virtual time between the beginning of this period and the end of the next time slot. We prove in Coq that this invariant is indeed preserved by the scheduler, and we, in turn, prove that abs_sched and vt_sched always produce the same schedule.
The sufficiency of individual virtual timelines. To address one of the main challenges of temporal reasoning, that all tasks are interleaved together in the schedule, we carry out step 3 ○ in Fig. 1 and prove that it is sufficient to examine the virtual timeline of a specific task to reason about its schedule. This is consistent with Fig. 4, where the schedules of different tasks never overlap with each other. In other words, the intuition is that, at any moment, there can be at most one task τ p that satisfies VTA (σ p , t).
We prove in Coq that if VTA (σ p , t) = 1 for task τ p , then VTA (σ j , t) = 1 does not hold for any higher priority task τ j . In particular, for any task τ j that has a higher priority than τ p , VTA (σ j , t) = 0 must hold. This is true by contradiction. Assume that there is a higher priority task τ j such that VTA (σ j , t) = 1. Since time slot [t, t+1) is consumed, it becomes unavailable to task τ j+1 and all subsequent lower priority tasks. Thus σ p (t + 1) = σ p (t), which contradicts the assumption that VTA (σ p , t) = 1.
In this way, we formally establish the relation between a task's schedule and its virtual timeline.
Lemma 4.2 (The virtual timeline faithfully describes the schedule of a task). For all p, t,
The main theorem. Combining everything together, on top of the functional correctness of the system, we obtain a schedulability proof for each task, as formalized in Corollary 3.3. And the schedulability property carries down to the generated assembly code of the system.
In this section, we discuss how to allow a periodic task to finish early and give up its remaining quanta to others. This model is more realistic and achieves better utilization for the whole system, i.e., more CPU time can be given to batch tasks when periodic ones do not require all their budgets. This requires a system call sys_finish, similar to periodic_wait in the ARINC 653 standard [ARINC 2015]. The core of its C implementation is straightforward, as shown in Fig. 13. Despite the simplicity of its C implementation, sys_finish complicates both the computation of time maps and the connection between virtual timelines with the concrete scheduler.
Computation of the time map. Under this setting, the fixed-priority scheduler is the same as in Sec. 4.3, thus time maps are defined in the same way as demonstrated in Fig. 5, that is, a time slot is available to the scheduled task and all higher priority tasks. However, the computation in Def. 2.1 is no longer valid because it assumes that every task uses up its budget in each period, which overly simplifies the accounting of time slots taken by higher priority tasks in the current situation.
We observe that the only effect of invoking sys_finish is that the actual execution time of a task may become smaller than its budget, which can only be known at runtime, making the static computation of time maps hard. However, it is possible to maintain an auxiliary data structure, O, to represent an oracle for execution times. Specifically, O p (k) is the execution time at the k-th period [kT p , (k + 1)T p ) of task τ p . We then parameterize the computation of a time map over an oracle, written as σ O p . Definition 4.3 (Computation of dynamic time map).
Compared with Def. 2.1, this parameterized version follows the same idea of recursive computation in decreasing priority order, while allowing variations in the actual execution time. In the following, we show two high-level properties we prove using this dynamic time map.
Obliviousness to lower priority tasks. One of the benefits of fixed-priority scheduling is its robustness, which states that the behavior of lower priority tasks can never affect higher priority ones. In the current setting, this means despite the varying actual execution time of lower priority tasks, the virtual timelines for higher priority ones stay the same.
Lemma 4.4 (Obliviousness to lower priority tasks). We consider the same task set with two different oracles, O 1 and O 2 . The behavior of task τ p does not change if all higher priority tasks exhibit the same behavior.
This is straightforward by observing in Def. 4.3 that the computation only relies on the execution time of higher priority tasks.
Schedulability of a task. Intuitively, if a task set is schedulable when every task always uses up its budget, then it is still schedulable when some tasks do not always use up their budget, since calling sys_finish could only result in more free time.
We define an oracle O init for the case when every task must use up its budget, such that ∀p, i, O init p (i) = C p . We also prove that the actual execution time is always bounded by the budget, in particular, after being updated by sys_finish.
∀p, i, O p (i) ≤ O init p (i) Using this invariant, we prove that if the time map corresponding to O init is schedulable, all subsequent mappings corresponding to a bounded O are also schedulable. This reduces schedulability analysis into the simple check in Corollary. 3.3.
Connection with the concrete implementation. Lastly, we discuss how to connect this dynamic version of virtual timelines to the system implementation. Notice that the concrete scheduler is the same as in Sec. 4.3, and the virtual-time-based scheduler is also similar, except with a parameterized version of time maps. We update the equivalence of states (Def. 4.1) accordingly.
Definition 4.5 (Equivalence between states of the abstract scheduler and the virtual-time-based scheduler, under the setting of variable execution time).
We prove that this relation is preserved by the scheduler, and further prove the refinement between the concrete scheduler and the virtual-time-based scheduler.
The remaining proof obligation is to connect the virtual-time-based system call, vt_sys_finish (illustrated in Fig. 14 using C code), with sys_finish. Here, exec_time represents the actual execution time of task p. Its computation exploits the fact that all lower priority tasks are not runnable until task p is finished, i.e., the entire virtual time duration is consumed by task p. We prove the equivalence of the two by showing that they also preserve the relation in Def. 4.5.
In this section, we discuss how the virtual time abstraction can be applied to partitioned scheduling. In particular, we apply virtual timelines in two different settings: TDMA (Time-Division Multiple Access) schedules and dynamic schedules for partitions. Throughout this section, we assume that the period of a task is a multiple of the period of its partition, which is common in choosing parameters for partitions. We adopt the computation of canonical local time map, ω c p as in Def. 3.7, and we discuss how to connect it with the concrete scheduler implementation.
TDMA Scheduling for Partitions. We first focus on the TDMA-based partitioned scheduling as in ARINC 653 standards, and show how to prove its schedulability, as well as non-interference using the virtual time.
Under this setting, the schedule of a partition is fixed. In fact, it employs the same period, P, for all partitions, and repeats the same partition schedule in every period. Assume the scheduling offset of partition Π i is δ i . Then in its k-th period, it is scheduled during the interval [(k -1)P + δ i , (k -1)P +δ i +B i ). We use π i to denote the schedule of Π i . We assume Π i uses the same fixed-priority scheduling for its tasks as discussed in Sec. 4.4. Scheduling within other partitions are irrelevant with respect to Π i .
Notice that under TDMA, the schedule of a partition is known ahead of time.
Definition 4.6 (Partition schedule under TDMA).
Here, we focus on a global scheduler with partition budget enforcement such as the framework presented in [Kim et al. 2015], as shown in Fig. 17. It is very similar to the flattened fixed-priority scheduler, except that it also maintains an array, Q, for each partition's budget. We omit code pieces that are similar to Fig. 2. The virtual-time-based counterpart of this global scheduler is shown in Fig. 18. Here, the time map for the partition is computed dynamically, while the local time maps for tasks are computed statically.
We prove the equivalence of both schedulers relying on the same relation as Def. 4.7. Since the partition is dynamically scheduled in this case, we need to prove that a partition is indeed scheduled for its full budget, B i , in each period. For simplicity, we assume all partitions have the same period, and prove the schedulability of partitions by showing that the sum of all remaining partition budgets always decrement until a new period arrives.
Our isolation guarantee relies on a proof of information flow non-interference. Non-interference is a property that guards the way information is transmitted among different components in a system. In particular, if two components are proved to be non-interfering with each other, then any modification to the state of one of them cannot alter the execution of the other. (Inter-component communications are prohibited, which would otherwise lead to direct interference between components.) This is of significant value in safety-critical systems, where critical components must never be affected by non-critical ones. Existing work mostly emphasizes spatial isolation, e.g. system calls do not leak information, so that non-interference between components is preserved. In our work, the extension with preemption brings more complexity regarding temporal isolation.
Temporal isolation refers to the absence of information flow through scheduling, that is, a component's observation on its own schedule (e.g. schedulability of a task in flattened scheduling and the local schedule of tasks in partitioned scheduling) is not affected by others. In particular, a component's observation does not include how often or how long it is preempted. Indeed, the current implementation of our scheduler does not allow a component to observe the number or duration of preemptions: timer interrupts and context switches are handled by the OS kernel, and a user task cannot access the global time.
For example, in flattened fixed-priority scheduling, higher-priority tasks can choose to either use up all the budget or yield early during a period, causing lower-priority ones to be preempted longer (and more often) or shorter (and less often), respectively. However, since real-time tasks must satisfy the schedulability test on their task parameters (budget and period), the schedulability of lower-priority tasks always holds thanks to the budget-enforcing mechanism of our scheduler. And since a low-priority task cannot observe preemptions directly (a task is scheduled by the OS kernel according to global time and status of higher-priority tasks, but that information is not exposed to this user task), there is no information leakage from higher-priority ones through scheduling. In other words, the low-priority task's observation on its schedule, which only includes its schedulability property, is not affected by others.
As another example, in partitioned scheduling, the exact schedule of a partition may change depending on the behavior of other partitions, e.g. it may be preempted in the middle by another partition whose task has higher priority than what it has run. However, this partition can enjoy temporal isolation if the local schedule of tasks remains the same regardless of how other partitions execute. This was discussed in Sec. 3.2 and Sec. 4.5.
We define the above notion of temporal isolation to allow flexibility in the global schedule of a component, which leads to better responsiveness of tasks and higher utilization of the processor, compared to a straightforward but rigid solution that makes the schedule of all tasks static. As a consequence, access to global time or time-leaking external devices is prohibited. External devices such as network cards could leak information about global time directly (e.g. by attaching a timestamp to a message) or indirectly. For example, if one knows the expected arrival rate of network packets, then that gives a pretty good indication of the passage of global time by counting how many packets have arrived. Also, as discussed in Sec. 1.3, microarchitectural level details, such as nondeterminism in the number of instructions a component executes during a time slot, are out of the scope of this work. We only focus on algorithmic properties instead.
In this section, we explain how we extend the proof of non-interference between tasks to the case studies described in Sec. 4.3 and Sec. 4.4, and we show how our framework accommodates the isolation proof with the presence of implicitly shared resources.
Non-interference of cooperative CertiKOS. The cooperative version of CertiKOS enjoys a mechanized proof of non-interference by Costanzo et al. [2016]. Unlike the usual approach based on security labels [Zeldovich et al. 2006], it instead defines non-interference with respect to an observation function O, which is a function from a state to an abstract observation that intuitively represents everything that can be observed, directly or indirectly. We call two states observably equivalent or observably indistinguishable regarding an observer task if the task's observation function returns identical values on both states. Non-interference is then defined as łpreserving (observational) indistinguishabilityž: Definition 4.8 (Non-Interference). A system is said to be non-interferent if its execution relation step preserves indistinguishability:
2 ) The interest of this definition is that it makes declassification extremely natural: just let the observation function return the declassified form. For instance, we can declassify the map from virtual addresses to memory content without leaking the physical addresses. The non-interference proof is carried down to the assembly code, thanks to security-preserving simulation relations [Costanzo et al. 2016].
The non-interference proof of CertiKOS takes advantage of the fact that the only way to trigger a context switch is through the sys_yield system call, in particular, that context switches always happen at the same places.
Structure of the non-interference proof of cooperative CertiKOS.
• The behavior of a task. As explained above, Costanzo et al. [2016] define a task's wholeexecution behavior on top of its observation function. ś Observation function. A task's observation includes its register state, virtual memory space, memory quota, number of children tasks, and the output buffer. ś Whole-execution behavior. It is specified with the execution status, e.g. Terminate/Fault, etc. and a task's observation of its final state. On top of this, the whole-execution-based isolation property of a task is defined as follows. A task enjoys non-interference if starting from two observably equivalent initial states, it exhibits observably equivalent whole-execution behavior, e.g. the two executions may terminate at observably equivalent final states. • The non-interference lemmas and frame rule. The core isolation theorem in Costanzo et al. [2016] states that whole-execution behaviors from observably equivalent initialized states s 1 and s 2 are identical. It specifies non-interference on a particular level. This is more of a frame rule, such that if a particular layer satisfies a group of predicates, most importantly confidentiality (observably equivalent states step to observably equivalent next states) and integrity (an inactive task's state is not tempered with by others), then the above statement is true. Notice that in this cooperative setting, context switches only happen upon voluntary yield, and this frame rule requires that two executions of a task be matched step-by-step. ś Proof burden involving system services. Various properties, such as confidentiality and integrity, are proved on all system services when the aforementioned frame rule is instantiated at the top level of cooperative CertiKOS. System calls available to a task include querying its memory quota, spawning new tasks, yielding the current execution, and printing to its buffer. • The end-to-end non-interference proof. The main theorem is an end-to-end property, stating that if two high-level initialized states, S 1 and S 2 , are observably equivalent, then starting from the two corresponding low-level states, s 1 and s 2 , the whole-execution behaviors are also observably equivalent. Its proof is mainly about showing that such security property is preserved by refinement, which is one of the main contributions by Costanzo et al. [2016]. This proof relies on the frame rule mentioned above.
Non-interference with preemption. Preemption breaks this existing proof as context switches can be triggered by interrupts that do not need to occur at the same place in all executions. In particular, we now need to prove that an execution in which a context switch is triggered is observably equivalent to an execution in which no context switch happens, which entails the correctness of context switch. These requirements exercise the specification of the context switch routine, and in doing so discovered that the original specification was not tight enough: the behavior of floating-point registers and the control register is undefined, which prevents us from establishing the equivalence of states before and after a context switch. Notice however that the existing specification was non-interferent, so that the overall non-interference proof of the cooperative CertiKOS is still correct, albeit less meaningful.
To that end, we narrow down the original specification to accurately reflect all details in the context switch. We modify the observation function to be insensitive to the task status, thus allowing to preserve indistinguishable states between a running execution and a preempted one, provided the latter gets the values of registers from its saved context. A task enjoys all system calls available in Costanzo et al. [2016] (newly-spawned tasks are always batch tasks), in addition to involuntary context switches triggered by preemption. These system services do not rely on explicitly querying another task's running status, thus they are compatible with the updated definition of observation. Notice that access to global time and communications between tasks are prohibited as a consequence of strict task-level isolation. A user task is still able to perform operations periodically without access to global time since the OS kernel is responsible for triggering new task periods according to global time.
We then extend the isolation frame rule which proves whole-execution non-interference based on single-step lemmas and instantiate it with various proofs on individual system calls and the scheduler. For example, we prove the integrity of all system calls, such that if a task is inactive (preempted), its observation doesn't change. We also prove the confidentiality of the scheduler, such that stepping from two observably equivalent active states, the next states are observably equivalent as well. Unlike in cooperative CertiKOS, confidentiality here does not require the two next states to be both active or both inactive. Instead, we prove them to be equivalent regardless of whether this task is preempted or not.
The get_usage system call. To illustrate the flexibility of our non-interference proof to address implicitly shared resources, we add get_usage system call. An implicitly shared resource is a resource whose usage is inherently tied with program execution and cannot be physically isolated, such as execution time, I/O, and instruction count. Doing so offers more measurement mechanism for the user, but also introduces a whole new category of side-channels related to the usage of this resource. However, we prove that under certain restrictions, queries of such kind of resource usage are also non-interfering.
Resource accounting relies on a cost model that associates with each instruction its cost for the resource under consideration. On the one hand, in order to avoid blatant information leakage when accessing the current total cost, we need to separately keep track of each observer's resource usage and only give each observer access to its own resource usage. On the other hand, resource accounting can be available only as global hardware monitoring, for instance, timing information is available through hardware timers. Thus, we carefully associate each resource usage to its user, through a stopwatch mechanism, depicted in Fig. 19.
The extension of the observation function is straightforward: we add a new field returning the value of the system call. Once the observation function has been updated, the non-interference proof presents no challenge: we only deal with the new case for the get_usage system call and update the proof of sys_yield (which modifies the stopwatch information).
We build on top of CertiKOS, a fully verified preemptive OS kernel with both spatial and temporal isolation. The extracted assembly code is further compiled by gcc into machine code, and runs on an Intel Sandy Bridge based x86 machine.
For the case studies in Sec. 4.3 and Sec. 4.4, we prove schedulability analysis of tasks, and noninterference at the task level. For the case studies in Sec. 4.5, we prove that the schedulability analysis of tasks is correct and that the local schedule within a partition is independent of others.
More detailed changes are summarized below:
• Extension of CertiKOS with user-level preemption, a verified interrupt handler (Sec.4.2), and a verified preemptive scheduler. • Functional correctness proof of the preemptive scheduler and the sys_finish system call (step 0 ○ in Fig. 1). • Formalization of virtual timelines, and algorithmic reasoning on top of it, including schedulability analysis and obliviousness properties (Sec. 3, also step 1 ○ in Fig. 1). • Formalization of the virtual-time-based scheduler, its refinement proof with the concrete scheduler, and its formal connection with individual virtual timelines (Sec.4.3,4.4,and 4.5, also step 2 ○ 3 ○ in Fig. 1). • Non-interference between tasks. We extend the framework of previous work by Costanzo et al. [2016] to a preemptive scheduler (Sec. 4.6) and fix an existing loose specification in the kernel. • The functional correctness proof of the get_usage system call, while preserving the noninterference property.
Fig. 20 provides a more detailed insight into the proof efforts involved. We have mainly used the one-tactic-per-line style of proof script; and we have also relied on automation techniques and Ltac scripts to simplify the proofs. The numbers in Fig. 20 are estimated LoC of changes against the original version of CertiKOS, obtained by analyzing the result of running git diff with -numstat option. Notice that we only count modified lines once in our estimation: one insertion and one deletion are merged to represent modification on one line. We avoid counting duplicated and reused proofs. For example, the proof for partitioned TDMA scheduler makes use of definitions and lemmas developed for the simple fixed-priority scheduler, yet we did not include those LOC in the statistics for TDMA. From this table we can observe that:
• The functional correctness proof of the fixed-priority scheduler takes more than 16k LoC, partly due to the fact that we introduce many intermediate layers to simplify the proof, thus we also have to duplicate many invariant proofs across those layers. • The formalization and reasoning about virtual timelines take around 2k LoC, which indicate that this is indeed a suitable abstraction for reasoning about algorithmic properties of fixedpriority preemptive scheduling.
• The virtual-time-based scheduler serves as a bridge connecting individual virtual timelines with the concrete scheduler in the system. It includes more than 3k LoC proof for data structures and lemmas mainly involving VTA (Sec. 4.3), which we believe is not specific to CertiKOS, and is applicable to other systems so that they could also benefit from this abstraction of virtual timelines.
Lessons learned. The main challenge with formalizing a preemptive scheduling algorithm is to find a suitable abstraction that facilitates the connection between the abstract scheduling behavior (e.g. virtual timeline in this work) and the concrete scheduler. We discuss possible choices of defining the virtual time map in Sec. 2.3, and our final decision leads to a simple form of simulation relation between the two schedulers, as shown in Def. 4.1.
Mechanized proofs allow us to address rigorous requirements on a complex system, such as schedulability in this work. However, the heavy proof burden coming with it makes it challenging to address complex mathematical reasoning, such as probability-based analysis if soft real-time scheduling algorithms are used. In this work, we select fixed-priority scheduling since it is relatively simple but still meaningful and practical for hard real-time system.
During the proof development, we found certain subtleties in the implementation of the kernel, which either warns us of limitations of our semantics models, or helps us prevent bugs that could invalidate the whole system.
The timer counter. The kernel uses a timer counter to keep track of the number of timer interrupts that have occurred, providing a time measure for the scheduler. However, since the system can run indefinitely, a fixed-sized counter (which we call a bounded counter) will eventually overflow.
We observe that the computation of task arrivals is identical after each hyper-period, that is, the least common multiple of periods of all tasks. We then introduce an unbounded counter in the system, which resides only in the abstract state. The unbounded counter keeps increasing, while the bounded one is reset every time it hits the hyper-period. We prove that as long as these two counters are equal modulo the hyper-period, the result of the scheduler is the same, and all proofs on temporal behaviors still hold.
A context switch subtlety. As mentioned in Sec. 4.6, the context switch primitive can satisfy non-interference in a cooperative setting without being tight at all. And this is actually exactly what happened: the existing context switch primitive of CertiKOS exhibits an undefined behavior regarding the CR register (where the test flags are set for instance), although it does satisfy noninterference in a cooperative setting.
The fact that non-interference with preemption requires to prove that the saved and restored contexts are identical forces us to strengthen this specification.
User-level preemption. Similar to [Sigurbjarnarson et al. 2018], our current extension on CertiKOS only allows for preemption at the user level. This assumption simplifies the correctness proof of CertiKOS, which assumes that kernel functions are executed atomically. However, the downside is that the lack of kernel preemption may result in longer interrupt disable time (interrupt latency), lowering the responsiveness of the system. Nevertheless, this is not an inherent limitation and could be mitigated in future work.
One solution is to adopt the bottom-halves mechanism (as used in µC/OS-III [Labrosse 2011]) and offload time-consuming work to user mode, effectively bounding the latency introduced by kernel services. This approach achieves better responsiveness, while still only requiring preemption in user mode so that the current functional correctness proof of CertiKOS would still be applicable.
It should also be noted that our reasoning framework is compatible with the future extension of kernel preemption. Indeed, enabling kernel preemption would require a careful handling of concurrent accesses to kernel objects even on a single-core machine, resulting in more complexity in both the kernel implementation and its proof. However, in a setting in which system calls do not block each other (which is reasonable for a single-core real-time system), kernel preemption is largely irrelevant to the scheduler. The scheduler is still invoked periodically by timer interrupts and selects the highest-priority available task in the system. Likewise, the schedulability and obliviousness properties proved on the scheduler still hold regardless of whether kernel preemption is supported or not. In this sense, our reasoning framework is compatible with verified single-core preemptible kernels.
Kernel overhead. A real-time OS kernel relies on the timer interrupt, which is triggered at a constant rate, to preempt user tasks. However, if the interrupt happens in the middle of a system call, its handling will be delayed until control is given back to user mode. Similarly, the interrupt handler itself also consumes time. In both cases, these small overheads prevent a task from executing for its full budget.
Ignoring kernel overhead is a fairly common assumption for schedulability analysis in a first approximation. However, such overhead can be accounted for without having to update our existing framework. At any timer interrupt, the maximum delay incurred by the kernel is the interrupt latency plus the context switch overhead. Given a trustworthy WCET on both overheads (which can be obtained by a sound analysis if the underlying real-time processor exhibits predictable timing behavior or a conservative estimation in case of a general-purpose processor), we can characterize the amount of recurring interference as another task with higher priority, a period that equals to that of the timer interrupt, and the worst-case execution time that equals to the sum of the maximum interrupt latency plus context switch overhead. In this way, the analysis of the interference of both overheads fit into the existing framework.
Nevertheless, as we do not allow real-time tasks to invoke certain system calls such as sys_spawn, and the C code of the rest of our system calls is simple enough (they are essentially straight-line programs, and we measure their average execution time to be 0.47µs on a 2.8 GHz machine), a statistical analysis should give a reasonable estimate.
Interrupt Driven Tasks. Currently, we only allow timer interrupts to preempt a task. However, users are able to sample a device periodically for interrupts or new data, which is common in time-critical cyber-physical systems [Murray et al. 2013;Sigurbjarnarson et al. 2018]. Thus the current periodic task set is already a reasonable setting for verification work.
One possible extension is to consider sporadic tasks, or interrupt driven tasks, that are not strictly periodic but triggered by interrupts. It is not difficult to support these tasks in our reasoning framework. The critical instant theorem we prove (Thm. 3.2) states that as long as the schedulability test is satisfied, a task enjoys its full budget within any physical time window whose length equals its period, no matter when this time window starts. This already entails schedulability in case of interrupt-driven tasks, whose minimum inter-arrival time, called period in real-time literature, is bounded and known. Hence, if a task is analyzed to be schedulable with the assumption of the minimum inter-arrival time, it is always schedulable as long as actual inter-arrival times are not lower than the bound. We leave this extension for future work.
Verification of schedulability analysis. The first mechanized proof about schedulability proves optimality of EDF [Wilding 1998]. Dutertre [2000] uses a state machine model in the automated theorem prover PVS to describe and verify the behavior of the priority ceiling protocol. Zhang et al. [2012] formally specify the correctness requirement (no priority inversion) of priority inheritance protocol using Isabelle/HOL, and prove the correctness of an implementation, but temporal properties are not modeled.
The PROSA [Cerqueira et al. 2016] project demonstrates readable mechanized proofs of various schedulability analyses written in Coq. It defines an abstract model of real-time tasks and real-time schedulers, and proves that all tasks will complete on time if certain conditions hold. Guo et al. [2019] connect PROSA with the real-time extension of CertiKOS described in Sec. 4.2, and obtains a schedulability proof for it. This connection requires a ghost variable to map kernel states to Prosa schedules and is based on the proof that the scheduler indeed follows a given scheduling policy. Unlike us, they only prove the schedulability of tasks under fixed-priority scheduling and do not address isolation. Our work highlights a suitable abstraction with isolation in mind. In addition to fixed-priority scheduling, our work also addresses partitioned scheduling, which involves more subtle isolation issues.
Verification of OS kernels. For a full overview of the verification efforts about operating systems, we refer the reader to Klein [2009] and Zhao et al. [2017]. Among all the OS verification works, we place our emphasis mainly on those conducted at the C or assembly code level.
SeL4 [Klein et al. 2009] is a formally-verified operating system kernel. It achieves multitasking in the kernel by polling timer interrupts at specified preemption points. Its machine model includes interrupts as abstract events and user transitions as arbitrary non-deterministic updates to the state, and the correctness of assembly routines is assumed [Sewell et al. 2013]. As a comparison, the machine model of this work is an extension of the CompCert assembly semantics, with checking on interrupt lines and also incorporated instruction level resource measurement such as instruction count. Most of the assembly routines are verified against this more realistic machine model.
An early extension of CertiKOS [Chen et al. 2016] tackles the problem of an interruptible kernel. By abstracting away interrupts using an approach based on abstraction layers, it proves a simulation relation between different interrupt models, and eventually achieves a model that is suitable for reasoning about device drivers in an interruptible kernel. Concurrent CertiKOS (known as mC2) [Gu et al. 2016[Gu et al. , 2018] ] is the first verified kernel that can support multicore concurrency with fine-grained locking but its scheduler is still not preemptive. Nemati et al. [2015] prove the design of a hypervisor based on ARMv7 with isolation properties, including caches. Unlike us, however, there is no verified implementation, as the proofs are only done at the specification level. Nelson et al. [2017] report the push-button verification of a kernel using the z3 SMT solver. To achieve that though, they must make compromises on the interfaces to make them amenable to automated verification by removing all quantifiers.
Verification of real-time OS kernels. INTEGRITY-178B is, to the best of our knowledge, the first real-time kernel to enjoy a machine-checked mathematical proof of non-interference [Richards 2010], as well as the avionics certification DO-178B level A. Nevertheless, this proof only applies to a model of the kernel, and has no formal link with its implementation.
The eChronos OS [Andronick et al. 2016] is a real-time operating system designed for uniprocessor embedded systems. It enables interrupts in most parts of the kernel to achieve minimum latency. It uses an interleaving model of the application code and different OS components [Andronick et al. 2015] and proves that the currently running process always has the highest priority among ready tasks. This work only models the behavior of different components and hardware interrupts without an end-to-end proof. Xu et al. [2016] verify µC/OS-II [Labrosse 1998], a real-time operating system featuring a preemptive kernel, using an ownership-transfer semantics. They prove the contextual refinement between the system's implementation and specification; they also demonstrate the ability to prove high-level properties, such as priority inversion freedom. However, it does not address more sophisticated high-level properties such as schedulability or temporal isolation.
Enforcement of isolation properties. Murray et al. [2013] prove a non-interference property for the seL4 kernel, which schedules partitions in a round-robin manner, and each partition adopts preemptive priority-based scheduling for its tasks. The non-interference proof depends on the setting that partitions are scheduled statically, so that there is no information flow from a partition to the scheduler. In contrast, our work focuses on formalizing a different problem in which partitions can be scheduled dynamically (e.g. it can depend on the global priority of its task), such that there can be information flow from a partition to the scheduler, yet the local schedule of tasks within one partition remains uninfluenced by others. Our work also addresses the schedulability analysis of real-time tasks, which is essential for temporal isolation. Sigurbjarnarson et al. [2018] prove intransitive non-interference of a system, so that only information flow explicitly allowed in the flow control graph can occur in the system. They implement NiStar, an OS kernel with decentralized information flow control, and prove that there is no covert channel among processes through the scheduler. This is achieved by statically assigning each time quantum to a thread, and a thread cannot transfer its quantum to others unless allowed by the information flow policy. It also addresses the partition isolation of a formalization of the ARINC 653 specification, which assumes a fixed schedule for partitions, in contrast to the dynamic partition schedule we focus on in this work. Lyons et al. [2018] propose a mixture of capability-based resource management and sporadicserver-based scheduling. They provide to the user an interface for reserving a portion of CPU time for a specific critical task. They report 2k lines of code on top of the original implementation of the OS kernel, and they use testing to show that this mechanism indeed constrains the CPU utilization of a particular task. As a comparison, our work focuses on strict temporal isolation, such as schedulability and obliviousness to other components, and we formally prove these properties in Coq with more than 76k LoC. Our work uses periodic servers for partitions, instead of sporadic servers used in [Lyons et al. 2018]. However, the same reasoning framework applies in both cases.
WCET analysis of verified OS kernels. Blackham et al. [2011] conduct a static WCET analysis on the seL4 compiled binary code's interrupt response time, with the help of invariants from the formal proof to exclude infeasible paths. They show that the WCET is sufficiently low without making the kernel fully preemptible. Sewell et al. [2017] achieve automation in determining and proving loop bounds, though manual annotation is still needed in some places.
This paper presents a novel compositional framework for verifying preemptive schedulers with temporal isolation. We introduce virtual timelines to describe temporal behaviors of components and to connect them with the actual system implementation. Using this abstraction, we prove the schedulability of each component in isolation, and prove various isolation properties regarding the schedule of components. In flattened fixed-priority scheduling, we prove that a task's schedule is not influenced by lower priority ones. In partitioned scheduling, we prove that a partition's local schedule of tasks is independent of other partitions, under a constrained setting.
As a case study, we apply this framework to CertiKOS, a formally verified single-core cooperative OS kernel. We extend it with a verified timer interrupt handler and a verified preemptive scheduler. We connect virtual timelines with the concrete implementation of the system by introducing a virtual-time-based scheduler, and proving that it is consistent with both the concrete scheduler and individual virtual timelines. In this way, all properties we prove on virtual timelines carry down to the generated assembly code of the system. We also prove that all services provided by our kernel preserve the integrity and confidentiality of user tasks, by showing that non-interference holds for this kernel. We also implement a secure get_usage system call for resource accounting and prove it to be non-interfering, by carefully defining what value it returns. Combining everything together, we achieve both temporal and spatial isolation between different components.
To the best of our knowledge, this is the first work that provides a formal abstraction for verifying the actual implementation of preemptive schedulers with temporal isolation.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 20. Publication date: January 2020.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 20. Publication date: January 2020. Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation 20:17
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 20. Publication date: January 2020. Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation 20:29