Real-time systems often power safety-critical applications, such as avionics and automobile control systems, where stringent timing constraints must be satisfied. With the increasing trend of hosting multiple applications on common hardware, the underlying real-time operating system (OS) must guarantee not only the correct operation but also the proper scheduling of each individual component. This requires a systematic way of multiplexing both time and memory resources while preserving strict isolation between independent components.
Consider a self-driving car system comprised of multiple software components at different criticality levels. The GPS navigation module and the visual recognition module sit at the regular criticality level, carrying out normal driving operations. Under this layer, a collision-avoidance controller and a fail-safe controller constantly monitor the overall status of the driving and are ready to take over the vehicle once they detect immediate danger ahead. The latter two modules are at the highest-criticality level since they must function correctly even if the other parts of the system malfunction or are compromised. This requires strict isolation from the other components in the system. For example, these two modules can be placed in a secure execution environment so their memory states cannot be tampered with.
However, spatial isolation alone is not sufficient. The collision-avoidance controller must execute periodically to detect possible crashes in time. In other words, the controller must be reserved a fixed amount of execution time within each period. This is achieved by hierarchical scheduling [Aeronautical Radio, Inc. 2010;Davis and Burns 2005;Deng et al. 1997]. Here, the OS kernel encapsulates each application into a time partition to reserve its CPU share. Then it schedules partitions based on a certain policy (e.g., using priority), and an application can only execute when its enclosing partition is scheduled. Further, to prevent an overrun of one partition from jeopardizing the scheduling of the others, the OS kernel strictly enforces partition budgets at all times, thus ensuring that each application's budget requirement is satisfied regardless of the other partitions in the system. Sec. 2.1 explains more details about real-time hierarchical scheduling.
Traditional real-time systems consist only of in-house components which are always trustworthy. Thus, they only need to focus on the time resource usage and guarantee that one component's ability to satisfy its timing requirement is not affected by behaviors of other components in the same system. However, a recent trend of integrating components from various vendors, some of which may be untrustworthy, which brings unique challenges regarding information flow security. This leads to a stronger notion of temporal isolation, which includes both real-time properties and information flow security. Sec. 2.2 provides more thorough discussion on these two different notions of temporal isolation.
Existing works mostly tackle spatial isolation and prove that memory resources are properly partitioned such that they do not lead to illegal information flow [Costanzo et al. 2016;Murray et al. 2013;Nelson et al. 2017].
On the temporal aspect, existing works only address restricted settings and are not compositional. For example, Murray et al. [2013] requires that partitions be static and scheduled in a round-robin manner. Liu et al. [2020] allows non-static partitions scheduled by a fixed-priority scheduling, but does not allow arbitrary partition periods. All these constraints limit their ability to compose diverse real-time applications into one system.
Let us consider the following example that highlights the non-compositionality of the fixedpriority (FP) scheduling. Under FP, a set of 𝑛 partitions is guaranteed to be schedulable if their total utilization (Σ < l a t e x i t s h a 1 _ b a s e 6 4 = " w 5 d Z m x X Y Z E E 6 u E L B Y p d x 2 U W 1 x 2 g = " > A A A C B H i c d V D L S s N A F J 3 4 r P V V d e l m s A i u Q l J r r b u C G 5 c V 7 A P a U C a T a T t 0 Z h J m J k I I 2 b p 3 q 7 / g T t z 6 H / 6 B n + E 0 j W B F D 1 w 4 n H M v 9 9 7 j R 4 w q 7 T g f 1 s r q 2 v r G Z m m r v L 2 z u 7 d f O T j s q j C W m H R w y E L Z 9 5 E i j A r S 0 V Q z 0 o 8 k Q d x n p O f P r u d + 7 5 5 I R U N x p 5 O I e B x N B B 1 T j L S R e s M 2 H a W 1 b F S p O v a F 4 1 4 1 z q F j O z l y 0 n R r T e g W S h U U a I 8 q n 8 M g x D E n Q m O G l B q 4 T q S 9 F E l N M S N Z e R g r E i E 8 Q x M y M F Q g T p S X 5 u d m 8 N Q o A R y H 0 p T Q M F d / T q S I K 5 V w 3 3 R y p K f q t z c X / / I G s R 4 3 v Z S K K N Z E 4 M W i c c y g D u H 8 d x h Q S b B m i S E I S 2 p u h X i K J M L a J L S 0 R W m O Z C K D r G y i + f 4 f / k + 6 N d t t 2 P X b e r U F i 5 B K 4 B i c g D P g g k v Q A j e g D T o A g x l 4 B E / g 2 X q w X q x X 6 2 3 R u m I V M 0 d g C d b 7 F x p M m O E = < / l a t e x i t > Π 2 ▾ deadline Fig. 1. Compositionality of Scheduling less than the above bound (82.8% for 𝑛 = 2), the partitions are schedulable under FP. Now, adding another partition whose period and budget are 50 ms and 20 ms, respectively, will increase the total utilization to 98.33%, while the Liu-Layland bound changes (77.97% for 𝑛 = 3).foot_0 Fig. 1(a) shows that Π misses its deadline at time 50ms.
The above threshold depend on the number of partitions in the system. Further, it relies on the assumption that partitions with larger periods occupy lower priorities. Otherwise, an exact analysis [Lehoczky et al. 1989] will need to take into account the priority, period and budget of all partitions. This is non-compositional, where a compositional scheme will only need to consider the total utilization of partitions alone, ignoring their numbers and exact parameters.
This non-compositionality is an inherent nature of the FP algorithm, which favors higher-priority partitions over lower-priority ones at any instant. In fact, partitions of different priorities can be viewed as layered on top of each other, where lower-priority ones can only execute when the higher-priorities ones have finished. From the verification perspective, this recursive structure is leverage for the formal reasoning of an FP scheduler, since it maps naturally to an inductive proof. Sec. 2.3 explains in more detail how this recursive structure is characterized by virtual timeline [Liu et al. 2020] and is used in the formal verification of an FP scheduler.
For performance, such non-compositionality may easily lead to underutilization of the processor, i.e., partitions cannot make 100% reservation of the CPU resource, especially with the trend of hosting multiple applications with arbitrary periods on a common hardware. Real-time applications often sample data periodically from devices (e.g., sensor input). In this case, a device's updating rate becomes the base period for its enclosing partition, whose other tasks follow periods that are multiples of this base rate. A complex real-time system may consist of multiple components with diverse base rates and hence may suffer a waste of CPU time due to this non-compositionality.
Earliest-deadline-first (EDF) scheduling is compositional, but significantly more challenging to verify. EDF is a dynamic-priority assignment algorithm, which eliminates fragmentation of CPU time and thus allows the free composition of components (even with diverse periods) as long as their total utilization does not exceed 100% [Liu and Layland 1973]. As illustrated in Fig. 1(b), under EDF, partition Π 2 shifts to the highest priority at time instant 30 and is thus able to schedule for its full budget. Further, we adopt the budget enforcement mechanism to prevent the overrun and malfunctioning within one partition from affecting the scheduling of other partitions.
However, from the verification perspective, the same mechanism brings significant challenges to the formal reasoning of OS kernels that adopt an EDF scheduler, e.g. for partition-level scheduling. Such verification is more challenging than a standalone schedulability analysis, because real-time properties need to connect with the concrete scheduler implementation and serve as pre-conditions for other OS functionalities. Because priority between components varies at different time instants and partitions can no longer be viewed as layering on top of each other, the recursive structure found in FP no longer holds under EDF. Thus, it is beyond the capability of static virtual timelines [Liu et al. 2020].
This paper makes the following contributions:
• We present a novel language-based abstraction to reason about the concrete implementation of preemptive schedulers with a dynamic priority assignment. In particular, it adopts a dynamic computation to address braided timelines which are free to intersect or shift priorities and are not limited to a fixed hierarchy. It achieves compositionality in the sense that real-time components with diverse periods are free to reside in the same system as long as their total utilization does not exceed 100%. • Using this abstraction, we implement and verify a real-time OS kernel with budget-enforcing EDF partitions. We prove that partitions can make a full reservation of the CPU resource.
We prove temporal isolation of partitions (conditioned on the task arrival model) by showing that the task schedule inside a partition is oblivious of others. All our proofs are mechanized in Coq and carried down to the generated assembly code.
In this section, we provide background on real-time hierarchical scheduling, temporal interference between partitions, and the static virtual timeline for verifying FP schedulers.
In real-time systems, a task is the basic unit of execution, corresponding to a user-level process hosted by an OS kernel. It is associated with a pre-specified period and budget (a.k.a. worst-case execution time), making its schedule different from a non-real-time process. For example, a task with a period of 500 ms and a budget of 60 ms will run for 60 ms within every period of 500 ms, say, from time 0 to 500 ms, from 500 ms to 1000 ms, etc. Multiple tasks constitute a real-time application so that they cooperate to achieve specific functionality. However, to accommodate the diverse periods and budgets of tasks and isolate one application's time resource usage from another, an application is usually associated with a time partition. A partition is also associated with a pre-specified period and budget so that the accumulative execution time of its tasks is bounded by the partition budget within every consecutive time window of the partition period. Fig. 3 summarizes the notations used in this paper.
Fig. 2(a) illustrates how a partition, Π 0 , and its two tasks, 𝜏 0 and 𝜏 1 , are scheduled. Task 𝜏 0 has a period of 7 and a budget of 1, such that it will execute for 1 time slot within the time window [0,7]. Similarly, 𝜏 1 executes for 2 time slots within [0,14]. Their enclosing partition, Π 0 , guarantees that the collective execution time of 𝜏 0 and 𝜏 1 does not exceed 2 time slots within [0, 5], [5,10], etc. Notice that, in the second partition period, since both 𝜏 0 and 𝜏 1 have used up their budgets and thus cannot execute, an idle task is scheduled to occupy the time slot allocated for Π 0 , represented by the white box.
In real-time hierarchical scheduling, an application partition is first selected by the global scheduler, and then a task inside the partition is selected by its local scheduler. There are two approaches to real-time hierarchical scheduling. Static partitionings, which can be found in avionics systems [LynxOS-178 2022;VxWorks 653 2022], follow a fixed partition schedule repetitively. They are simple to implement and guarantee strong isolation between components. However, it is a fundamental limitation that this scheme is inflexible in CPU usage [Heiser 2020;Kim et al. Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation 127:5 0 1 2 3 4 5 6 7 8 9 10
(2, 5) means the component's budget is 2 and period is 5. Downarrow represents the arrival of a task.
The number of partitions Π 𝑖
The 𝑖-th partition, where 0 ≤ 𝑖 < 𝑁 𝑇 𝑖
The period of Π 𝑖 𝐶 𝑖
The time budget of Π 𝑖 within each period 𝜋 𝑖
The virtual time map for
The number of tasks inside a particular partition 𝜏 𝑗
The 𝑗-th task inside a particular partition, where 0 ≤ 𝑗 < 𝑀 𝑝 𝑗
The period of 𝜏 𝑗 𝑒 𝑗
The budget of 𝜏 𝑗 within each period
. Further, supporting applications with different base rates can be challenging because staticpartitioning relies on finding a major cycle that accommodates the cyclic behavior of all components.
On the contrary, non-static partitioning allows enhanced resource flexibility and results in better responsiveness. This category employs real-time server algorithms (such as periodic server [Shin and Lee 2003], sporadic server [Sprunt et al. 1989], constant bandwidth server [Abeni and Buttazzo 1998], which is adopted by the SCHED_DEADLINE mechanism in Linux) to contain a set of tasks. A server (used interchangeably with a partition) is characterized by the budget, 𝐶 𝑖 , and the replenishment period, 𝑇 𝑖 . The server's budget is consumed as much as its tasks are executed. Partitions can be scheduled based on fixed-priority (e.g., periodic server, sporadic server) or dynamic-priority (e.g., constant bandwidth server).
As explained above, time partitioning reserves a time budget for a group of tasks, so that they can meet their own timing requirements (e.g., guaranteed amount of time budget within each period) no matter how tasks in other partitions behave. This notion of temporal isolation is widely adopted in the real-time community. Indeed, real-time systems usually host multiple components with diverse timing requirements. Since all components are trusted, traditional spatial isolation techniques (e.g., virtual memory) may not be as important for the system. Instead, such a system usually focuses on temporal isolation and adopt static or dynamic time partitioning schemes to distribute time resource properly among components. As mentioned above, non-static partitioning achieves better CPU utilization and is extensively studied in the literature.
However, in recent years, there is a growing trend of integrating various components, not necessarily from the same vendor, onto a single system [Aeronautical Radio, Inc. 2010;Yoon et al. 2021]. This achieves better cost-effectiveness but also exposes benign components to potential confidentiality violations: malicious components can collude to infer secret information from them since they share common CPU resources. Although various spatial isolation techniques exist, they cannot handle challenges caused by real-time scheduling schemes (e.g., temporal interference caused by the non-static time partitioning). This is a unique challenge for real-time systems which also require isolation in the sense of security.
l a t e x i t > Π0 = (10, 30) < l a t e x i t s h a 1 _ b a s e 6 4 = " a G G D A N N j z 4 N M / O 9 A 2 a w p q q 5 Z s K Let us consider Fig. 2 again. Here, partitions are scheduled by EDF. We examine partition Π 0 , which consists of two tasks, 𝜏 0 and 𝜏 1 , where 𝜏 0 has a higher priority. Case (a) depicts the case when Π 0 runs alone. In this case, it always occupies the first 2 slots within each period (= 5). As a comparison, case (b) schedules Π 0 together with Π 1 . Though Π 0 is still guaranteed 2 time slots in every period, its exact schedule differs from (a). Specifically, the relative ordering between 𝜏 0 and 𝜏 1 is flipped depending on the exact schedule of their enclosing partition Π 0 . This is caused by the varying task arrival time in this partition's local view, which is affected in turn by the behavior of the other partition, i.e., Π 1 . Such non-determinism may allow a partition (e.g., Π 0 ) to infer the execution pattern of another (colluding) partition (e.g., Π 1 ) by observing differences in its own task schedule, which effectively creates a covert channel, breaking the information-flow policy. Liu et al. [2020] formalized this problem, and Yoon et al. [2021] demonstrated the feasibility of establishing such covert channels (e.g., leaking out sensitive data item) in a Linux-based real-time operating system that operates on a 1/10th-scale self-driving car platform.
This paper focuses on the above notion of temporal isolation in the sense of information flow security. Notice that this is a unique challenge for real-time systems that need to integrate potentially untrusted components and execute them alongside trusted ones. For all other real-time systems, the traditional notion of real-time temporal isolation suffices to guarantee their correct operations ś they do not suffer the same security vulnerability if all components are trusted.
CertiKOS [Costanzo et al. 2016;Gu et al. 2015Gu et al. , 2019Gu et al. , 2016] is a verified OS kernel featuring a formal functional correctness guarantee down to the assembly code level. It centers around the idea of abstraction layers, which formally connects a piece of C/assembly code with its Coq specification through a simulation proof. Using this layered approach, CertiKOS builds a verified OS kernel and proves that the behavior of its concrete implementation is equivalent to its Coq specification.
The real-time extension of CertiKOS [Liu et al. 2020] proposes the static virtual timeline to describe and reason about the temporal behavior of a fixed-priority (FP) scheduler. Their main observation is that there is a fixed precedence relation among components, such that the preemption of a component can be viewed as hiding certain time slots away from it. For example, Fig. 4(a) illustrates the FP scheduling of three partitions, Π 0 , Π 1 , and Π 2 , in decreasing order of priority. The bottom plot depicts each partition's virtual timeline, i.e., which time slots are available to it (white boxes) and which ones are not (grey boxes). The top plot depicts the execution of the partition, which must correspond to white boxes on its virtual timeline. The virtual timeline for Π 0 contains only white boxes because it has the highest priority and can never be preempted. Partition is only preempted by Π 0 , thus grey boxes on its virtual timeline correspond to the execution of Π 0 . The remaining time slots are available to Π 1 and are depicted as white boxes. Finally, Π 2 is preempted by both Π 0 and Π 1 , so that grey boxes on its virtual timeline correspond to both tasks' execution. In this way, the virtual timeline hides interferences from higher-priority partitions.
To facilitate mechanized formal reasoning of virtual timelines, Liu et al. [2020] use a virtual time map to describe a virtual timeline. Such a concept is similar to the supply-bound functions in the real-time literature [Lehoczky et al. 1989;Liu 2000], but with adapted definitions to facilitate verification of the scheduler's source code. Here, virtual time is the number of available time slots for a partition, i.e., the total length of white boxes, up to a particular global time instant. Virtual time map is a mapping from the global time to the virtual time of a partition, denoted as 𝜋 𝑖 . For example, all time slots are available to the highest-priority partition, Π 0 . Thus, 𝜋 0 (𝑡) = 𝑡 Time slots not occupied by Π 0 are available to the second-highest one, Π 1 , and so on. Assume that a partition Π 𝑖 becomes ready to run at regular time instants 0,𝑇 𝑖 , 2𝑇 𝑖 , 3𝑇 𝑖 , ..., and that it executes for 𝐶 𝑖 time slots within each period. The virtual time map for Π 𝑖+1 can be constructed as follows (adapted from Def. 2.1 in [Liu et al. 2020]).
Definition 2.1. The static construction of time maps for fixed-priority scheduling:
This means 𝜋 𝑖+1 (𝑡) comes from 𝜋 𝑖 (𝑡), excludes the execution of Π 𝑖 in previous whole periods (⌊ 𝑡 𝑇 𝑖 ⌋𝐶 𝑖 ) joints with the execution of Π 𝑖 in the last partial period. This way of static construction of time maps is specialized in the fixed-priority setting. Liu et al. [2020] prove that such an abstraction faithfully captures the temporal behavior of components. Thus the reasoning of a concrete fixedpriority scheduler implementation is lifted to an abstract domain, where they formally prove temporal properties such as schedulability and obliviousness to lower-priority components.
Formally verifying an EDF scheduler on the source code level is challenging. Though virtual timeline lifts the verification of a concrete scheduler into the abstract domain, getting it to reason about the EDF scheduling is highly non-trivial. The bottom plots in Fig. 5 give an empirical illustration of individual partition's temporal behavior under different scheduling algorithms. Here, the horizontal axis represents the global time, and the vertical axis represents the time available to a particular partition. The overall map is denoted as a virtual timeline. In Round-Robin scheduling, a time slot is only available to one partition at any instant, and thus time resources for different partitions do not overlap. In FP scheduling, time resources are allocated to partitions in decreasing order of fixed-priority, resulting in properly layered timelines in the figure (refer to Def. 2.1 for the exact computation). This recursive nature enables the inductive proof of the FP scheduler in [Liu et al. 2020].
On the other hand, in EDF scheduling, the priority between partitions varies at different time instants, as shown in the top plot (Fig. 5(c)). In this way, the resulting timelines become braided, i.e., they overlap and intersect with each other instead of being properly layered. Such lacking of a recursive structure makes its formal reasoning significantly more challenging, which is beyond the capability of static virtual timelines [Liu et al. 2020].
We tackle this problem by adopting the dynamic computation of time maps. This allows us to separate the source code of an EDF scheduler from the high-level reasoning of its temporal behavior. The intuition is that, even though there is no fixed hierarchy among partitions, at any particular moment, a transient priority relation still exists and is deterministic. We make it explicit by calculating a priority queue at each invocation of the scheduler. This allows us to dictate the availability of a time slot. For example, if partition Π 𝑖 is scheduled on time slot [𝑡, 𝑡 + 1), obviously this slot is available to Π 𝑖 . Further, it is also available to partitions with higher priorities. In fact, the reason this slot is allocated to Π 𝑖 is that all higher-transient-priority partitions have used up their budgets, and thus this slot is available to but not used by them. We then embed the dynamic computation of timelines in a virtual-time-based scheduler. At any moment 𝑡, the scheduler iterates over all partitions in the transient priority queue and schedules the first one available to execute on its virtual timeline. Finally, the scheduler updates time maps for all partitions up to the next time tick, 𝑡 + 1. This is illustrated in Fig. 9. We explain in more detail in Sec. 4.
Previous sections explain two major problems with existing verified real-time OS kernels when being used to integrate real-time components from multiple vendors: (1) the application of hierarchical scheduling may lead to inter-partition interferences (Sec. 2.2); (2) existing formal technique, i.e., static virtual timeline, is not compositional and only works with straightforward scheduling algorithms, such as FP (Sec. 2.4). In this section, we explain our overall design of a secure OS kernel with budget-enforcing EDF partitions, and address the challenges in its formal verification.
In this work, we address an algorithmic covert channel in the context of hierarchical scheduling in a real-time OS kernel. The attacker controls one or more partitions in the system and tasks inside these partitions. The attacker's tasks can access its own memory, invoke system calls (e.g., to communicate with each other inside the same partition), and thus observe the order in which its tasks are scheduled. Indeed, this allows an attacker to measure the progress of its own tasks and to indirectly infer the passage of global time. However, the attacker's code cannot read the global time or access time-leaking devices directly. Thus, the attacker's measurement of time is still logical. Communication between two partitions is also prohibited.
Notice that a real-time task's proper functioning does not necessarily rely on having direct access to a real clock. The OS is able to schedule the task according to its timing parameters. Further, there are various mechanisms for preventing access to a real clock. On the instruction level, modern processors provide mechanisms to prevent user-level instructions to access timing registers, e.g. through RDTSC. On the system level, the OS can properly restrict access to time-leaking devices.
The attacker observes variations in its own task schedule to infer the behavior of tasks in other partitions [Yoon et al. 2021]. Such a covert channel is algorithmic because it leverages the scheduling algorithm instead of micro-architectural-level details. To close such a channel, this work aims to prove the confidentiality property of the scheduler implementation, i.e., the attacker cannot infer information about other partitions by observing its own scheduling behavior.
We make the following design decisions to achieve temporal isolation and full reservation of CPU resources.
• Firstly, budget enforcement prevents the overrun of one partition from affecting other partitions' CPU usage, which is necessary for ensuring isolation. • Secondly, since applications may rely on devices with arbitrary base rates, our system must accommodate arbitrary partition periods. In this case, FP suffers fragmentation issues and thus cannot make full reservation of the CPU resource in a general scenario, as explained earlier. On the contrary, EDF achieves 100% reservation of the CPU resource while allowing arbitrary partition periods. Thus, we adopt EDF for the partition-level scheduling. • Lastly, we require tasks to be bound by their enclosing partitions to avoid covert channel between partitions as illustrated in Fig. 2. More specifically, we require that tasks' periods are multiples of the partitions' period and that tasks' arrivals are always synchronized with the boundaries of the partition's periods [Davis and Burns 2005]. This is in fact a common practice in real-time systems. Sec. 6.2 provides more lengthy discussions.
Even though the above implementation approaches avoid the covert channel illustrated in Fig. 2, its formal verification remains challenging. Fig. 6 gives an overview of our approach. Here, each rectangle represents one "layer," which is a collection of functions and internal states of the OS kernel. Yellow boxes represent concrete C functions. Blue boxes represent abstract functions in Coq.
The green arrow, ⊑, denotes contextual refinement proofs between two layers, which abstracts C functions into Coq representations, or abstracts Coq representations into forms that are more suitable for reasoning.
As shown in Fig. 6, the partition-level scheduler psched and local scheduler lsched are both available in the first layer, "Concrete Scheduler". However, proving schedulability and temporal isolation directly in this layer will be too challenging. Instead, we introduce new intermediate layers to bridge the gap between "Concrete Scheduler" and "Abstract Scheduler with Oblivious lsched", so that proofs for each step can be done more easily. In the following, we explain the intuition behind each layer.
Layer "Concrete Scheduler". This layer includes two pieces of C code, the partition-level scheduler, psched (Fig. 7), and the local scheduler, lsched (Fig. 17). They operate on the global time t, the partition-level quanta array 𝑄 𝑝𝑎𝑟𝑡𝑖𝑡𝑖𝑜𝑛 , and the task-level quanta array 𝑄 𝑡𝑎𝑠𝑘 .
In particular, psched first refills budgets for partitions that are about to start a new period (Line 4 -8). It then iterates over all partitions in the order of their index (Line 13), and maintains 𝑝𝑖𝑑 and 𝑑𝑑𝑙 to find the partition with positive remaining budget and the nearest deadline (Line 14 -21). Here, partition Π 𝑖 's deadline is the ending time of its current period, as computed on Line 15. Finally, psched deducts 𝑄 𝑝𝑎𝑟𝑡𝑖𝑡𝑖𝑜𝑛 [𝑝𝑖𝑑] if Π 𝑝𝑖𝑑 is not an idle partition (Line 23 -25). Even though the implementation of the above EDF scheduler is straightforward, its formal reasoning is extremely challenging, as explained in Sec. 2.4. We introduce two more layers as shown below to facilitate its formal proof.
Layer "Abstract Scheduler with PriQ". It introduces a ghost state, 𝑃𝑟𝑖𝑄 (see Fig. 10), to represent the transient priority queue at any time instant (the closest deadline corresponds to the highest priority). As shown on Line 12 in Fig. 8, 𝑝 represents the transient priority level, where 0 means the highest priority. On Line 13, 𝑃𝑟𝑖𝑄 𝑡 (p) returns the partition index i at priority level p. Unlike psched, int_psched (Fig. 8) iterates over all partitions in decreasing order of priority and checks whether the remaining budget is positive or not. If Π 𝑖 is found at Line 15, it must have the closest deadline among partitions that are ready to run. Thus, int_psched indeed satisfies the EDF policy. We prove that int_psched is contextually equivalent [Gu et al. 2015] to psched in Sec. 4.
Layer "Abstract Scheduler with Braided Virtual Timeline". Here, we define compositional virtual timelines (𝜋, explained in more detail in Sec. 4) to characterize the temporal behavior of EDF scheduling. 𝐼 𝑖 (⌊𝑡/𝑇 𝑖 ⌋) is another ghost state that tracks the amount of interference in the ⌊𝑡/𝑇 𝑖 ⌋-th period to facilitate the formal reasoning on 𝜋, which is explained in more detail in Sec. 5. We then prove that the intermediate EDF scheduler, int_psched (relying on array 𝑄 𝑝𝑎𝑟𝑡𝑖𝑡𝑖𝑜𝑛 ), is contextually equivalent to abs_psched (Fig. 9), such that 𝜋 is indeed a faithful abstraction (Sec. 4.2).
This allows us to address the formal reasoning of the concrete EDF scheduler by formalizing its behavior on top of 𝜋. Sec. 5.1 explains in more detail how such a notion facilitates the proof that each partition gets its full budget within every period. In this way, through equivalence proofs across three consecutive layers (psched ⊑ int_psched ⊑ abs_psched), the property specified using an abstract 𝜋 carries down to the concrete source code of the EDF scheduler.
Layer "Abstract Scheduler with Oblivious lsched". Finally, this layer addresses the task-level scheduler inside partitions, lsched (Fig. 17). We prove its contextual equivalence to a Coq abstraction, obliv_lsched (Fig. 18), which maintains the partition's local time and is oblivious to the global time (Sec. 6.3). In this way, we prove that the local behavior of partitions is independent of other partitions residing on the same processor, and formally close the algorithmic covert channel illustrated in Sec. 2.2.
In this section, we explain how we use braided virtual timelines to reason about EDF scheduling on the partition level.
Fig. 9 illustrates the dynamic construction of braided virtual timelines. N denotes the number of partitions in the system. Here, 𝜋 𝑖 (t) denotes the amount of time available to partition Π 𝑖 in the global time range [0, 𝑡). However, unlike the static construction in Def. 2.1, we cannot compute in advance the value of 𝜋 𝑖 at every time instant. Rather, at time t, all time maps ( {𝜋 0 , 𝜋 1 , ..., 𝜋 𝑁 -1 } ) are valid up to t. Then the scheduler increments the time counter to t + 1 and iterates over all partitions in decreasing order of transient priority (p from 0 to N-1). Variable pid denotes the partition to be scheduled. Initially, it equals N (Line 4), meaning the idle partition will be selected by default. As the scheduler iterates over partition Π 𝑖 (Line 6 -12), it increments 𝜋 𝑖 by 1 at time t+1 (Line 8) because the time slot [t, t+1) is available to Π 𝑖 . If Π 𝑖 is not finished, i.e., the amount of time available to it at the current period is less than its budget (Line 9), it will be selected by the scheduler because it has the highest transient priority among ready partitions. Then, for lower-priority partitions, their virtual time stagnates because they are preempted (Line 13). Here, on Line 14, 𝐼 𝑖 [𝑡/𝑇 𝑖 ] is a ghost state that records the amount of interference Π 𝑖 experiences in each of its period. We will explain in more detail in Lemma 5.5. In this way, if Π 𝑝𝑖𝑑 is scheduled, the virtual time for itself and higher-priority partitions is incremented, while the virtual time for lower-priority ones stagnates.
The intuition behind the loop in Fig. 9 is that at each moment t, there is still transient priority among partitions, allowing us to define the preemption relation between them. In particular, at any moment t, we compute a priority queue 𝑃𝑟𝑖𝑄 𝑡 , which orders all partitions by their current deadlines. Fig. 10 shows its Coq formalization. Here, a partition is represented as ParValid T C, where T is its period and C is its budget. At moment t, get_priqueue_aux computes a list of PriEntry d id, where id is partition ID and d denotes the current deadline of Π 𝑖𝑑 (Line 25). The remaining work is to sort this list by each partition's priority, i.e., deadline. This is achieved by invoking sort with a custom comparator (Line 30), priEntry_le, which first compares the two deadlines, and then compares the partition IDs as a tie-breaker. In the end, get_priqueue returns the priority queue for the set of partitions conf at time instant t. We observe that the transient priority relation is indeed pre-defined and does not depend on the runtime behavior, e.g. whether a task has used up its budget or not at any particular moment.
< l a t e x i t s h a 1 _ b a s e 6 4 = " 3 2 6 w 7 s 0 O r 7 e 9 G 0
o G q N n 9 I r e r M x 6 s d 6 t j 0 V r w c p n j t E f W J 8 / i p i R q Q = = < / l a t e x i t > s 2 =(t 2 , π)
< l a t e x i t s h a 1 _ b a s e 6 4 = " e i 0 S y p
< l a t e x i t s h a 1 _ b a s e 6 4 = " O 9 7 5 q t c v U s h q A b 0 y 7 U r f T 8 5 I
< l a t e x i t s h a 1 _ b a s e 6 4 = " 1 z n 5 p N q T T C p + X L j l S l L t 3 s p 6 5 b 4 s 0 0 = s 0 1 ?
< l a t e x i t s h a 1 _ b a s e 6 4 = " h R i o y N u P R +
< l a t e x i t s h a 1 _ b a s e 6 4 = " / h x U o U 3 R D l o K K x 8 P 4 5 Z 6 g 7 y 2 n l I
This leads to the same motivation when the virtual timeline is first introduced for fixed-priority scheduling: encapsulate interferences from higher-priority partitions such that the schedule of one partition can be decided by looking at its virtual timeline alone. In particular, Line 9 in Fig. 9 compares 𝐶 𝑖 with 𝜋 𝑖 (𝑡) -𝜋 𝑖 (⌊𝑡/𝑇 𝑖 ⌋𝑇 𝑖 ). If the former is smaller, partition Π 𝑖 has been given enough available time slots during the current period and must have used up its budget. Otherwise, Π 𝑖 is ready to run at the next time slot.
This formalization helps us decouple the scheduler's source code from its high-level reasoning. Fig. 7 demonstrates the source code for an EDF scheduler. It uses an array, 𝑄 𝑝𝑎𝑟𝑡𝑖𝑡𝑖𝑜𝑛 , to track the remaining budget of each partition. At any moment, it iterates over all partitions to find the one with a positive budget and the nearest deadline. The formal connection between virtual timelines and this scheduler implementation relies on a refinement proof that the two are equivalent in deciding a task's schedule. The proof structure is similar to that in [Liu et al. 2020], and we explain more details in Sec. 4.2.
In this section, we explain how the braided virtual timeline is formally connected to the source code of an EDF scheduler. This step corresponds to the refinement proof between the partition-level EDF scheduler (psched in Fig. 7) and the braided virtual timeline abstraction (abs_psched in Fig. 9) shown in Fig. 6.
In this paper, we follow the certified abstraction layer approach [Gu et al. 2015] to verify the source code of a real-time OS kernel. Here, a refinement proof between a lower-layer function and a higher-layer function requires matching the relevant state and return value of both functions. In particular, starting from equivalent states, the two functions must execute and result in equivalent final states and yield identical return values.
Fig. 11 illustrates the refinement proof between psched and abs_psched. Here, psched operates on the global time t and the quanta array 𝑄, while abs_psched operates on t and the virtual time maps 𝜋. After executing both functions, they will update relevant states and return the pid for the next partition to schedule. Since the two functions rely on different definitions of states, we use 𝑅 12 to denote their equivalence relation, which is more sophisticated than being identical. Thus, the goal of the refinement proof is to show that if the two starting states satisfy 𝑅 12 (𝑠 0 , 𝑠 2 ), then the two final states must also satisfy such equivalence property, 𝑅 12 (𝑠 ′ 0 , 𝑠 ′ 2 ). Notice that an OS kernel maintains many more states than the global time and quanta array for its scheduler. In the actual proof, all other states are identical across 𝑠 0 and 𝑠 2 and remain unchanged in 𝑠 However, the refinement proof between psched and abs_psched is not straightforward. As illustrated in Fig. 12, the two differ in both the iteration order and in how they check the schedule status of a partition. To bridge the gap between them, we introduce an intermediate abstraction, int_psched (Fig. 8). Here, similar to what abs_psched does, it relies on a priority queue to iterate over all partitions from the one with the nearest deadline. On the other hand, int_psched still relies on 𝑄 𝑝𝑎𝑟𝑡𝑖𝑡𝑖𝑜𝑛 to maintain the schedule status for each partition, similar to psched.
Contextual refinement between psched and int_psched. This involves algorithmic equivalence between the two schedulers. In particular,
• If int_psched returns 𝑁 (the idle partition) at time 𝑡, all partitions must have finished and psched will also return 𝑁 . • If Π 𝑖 is scheduled by int_psched at time 𝑡, all higher-priority ones (having a closer deadline) must have finished. In this case, after iterating over all partitions, psched would also find that Π 𝑖 is the highest-priority ready partition.
Contextual refinement between int_psched and abs_psched. We observe that the two schedulers exhibit a common structure. More specifically, they rely on the same priority queue and iterate over all partitions in the same order. The only difference is that int_psched uses the quantum value while abs_psched looks up the virtual time map to decide whether a partition has used up its budget or not.
Closing this gap between the quantum value and the virtual time map calls for the same equivalence relation as in Def. 4.1 in [Liu et al. 2020]. In particular, we prove that the following relation is preserved as the two schedulers execute so that they match each other step-by-step.
Sufficiency of an individual virtual timeline. We prove that the abstract scheduler, abs_psched, is always consistent with individual virtual timelines, such that it suffices to examine 𝜋 𝑖 to derive Π 𝑖 's temporal properties without considering other tasks. At any moment, at most one partition satisfies both of the following requirements: (i) the next time slot is available to it on its virtual timeline; (ii) it has not used up its budget in the current period.
This concludes the connection with the scheduler's source code. As shown in Fig. 6, this guarantees the faithfulness of the temporal abstraction such that all properties proved on top of it also hold on the system's source code.
This section explains in more detail how we verify the partition-level EDF scheduler. Recall that a partition is strictly periodic and will be cut off until the next period once it has used up its budget. We formalize the proof goal as below.
Definition 5.1 (Schedulability). If the total utilization of all EDF partitions does not exceed 100%, for any partition Π 𝑖 , it always gets its full budget 𝐶 𝑖 in each period 𝑇 𝑖 , i.e., ∀𝑘 ≥ 0, 𝜋 𝑖 ((𝑘 + 1)𝑇 𝑖 ) -𝜋 𝑖 (𝑘 * 𝑇 𝑖 ) ≥ 𝐶 𝑖
The above schedulability property is specified on the braided virtual timeline abstraction, 𝜋 𝑖 , which describes the schedule of partition Π 𝑖 . This is a faithful abstraction since Sec. 4.2 proves the contextual refinement between psched and abs_psched, such that any property proved on 𝜋 𝑖 carries down to the assembly code of psched.
This section outlines our schedulability proof for an EDF scheduler. The proof goal is formalized in Def. 5.1. Given the complicated construction of 𝜋 𝑖 , it is extremely challenging, if possible at all, to obtain a straightforward proof.
Rather, we reflect on the intuition behind the EDF scheduling. Its schedulability test is compositional: only the utilization, instead of the exact period or budget of a partition, matters. An immediate implication is that we can pretend that all partitions have a common period if we are only concerned about the system's schedulability. In other words, we can tweak partitions' parameters so that they share a common period,
. . in which case the scheduling is equivalent to a weighted round-robin manner and proving the schedulability is trivial.
This insight was first discussed by Wilding [Wilding 1998], who formalized it as the optimality of the EDF and proved it in a theorem prover. However, unlike the work being presented in this paper, its proof relies on reordering an existing schedule in a sophisticated manner, making the connection with the scheduler source code challenging, if possible at all.
In this work, we follow a different path with the same insight. Instead of permitting arbitrary adjustment of partition parameters, we view it as a way of breaking down the proof obligation into smaller steps. As mentioned earlier, since the proof regarding the original partition set is challenging, we first consider a trivial case where all partitions share the same period, then adjust partition parameters one by one until we revert it to be identical to the original partition set.
Assume that the partition set Γ contains three partitions: Π 0 = (10, 40), Π 1 = (10, 30), and Π 2 = (20, 50). We define Ω 𝐸𝐷𝐹 (Γ) to specify that Γ is schedulable under the EDF policy. The aforementioned proof structure is illustrated below.
Example 5.2. The schedulability proof for Γ = {Π 0 , Π 1 , Π 2 } Ω 𝐸𝐷𝐹 ({(150, 600), (200, 600), (240, 600)}) =⇒ Ω 𝐸𝐷𝐹 ({(150, 600), (600, 1800), (240, 600)}) =⇒ Ω 𝐸𝐷𝐹 ({(600, 2400), (600, 1800), (240, 600)}) =⇒ Ω 𝐸𝐷𝐹 ({(600, 2400), (600, 1800), (1200, 3000)}) =⇒ Ω 𝐸𝐷𝐹 ({Π 0 , Π 1 , Π 2 }) In the above example, we start from a partition set where all partitions have a common period, 600, while their utilizations remain the same as the original partition set. Subsequently, we enlarge the 2nd, 1st, and 3rd partition by a factor of 3, 4, and 5, respectively. Here, enlarging a partition by a factor of k means updating its period and budget to be k times the original value, such that the partition's utilization stays the same. Also, notice that the order in which we enlarge partitions is not arbitrary. In fact, we follow the increasing order of the original partition's period, such that at any step, the enlarged partition will have the longest period in the system. This helps us eliminate certain unnecessary cases and simplifies the proof. In the end, we shrink all partitions by a factor of 60 to transform them back to the original partition set.
To put it formally, for any arbitrary set Γ containing N periodic partitions, we first compute H as the least common multiple of {𝑇 0 ,𝑇 1 , ...,𝑇 𝑁 -1 }. Then we start from a set whose partitions share a common period H while preserving their original utilization, i.e., Π 𝑖 's budget is 𝐻 𝑇 𝑖 𝐶 𝑖 . Then we enlarge partitions one by one, in increasing order of their original period. For Π 𝑖 , it is enlarged by a factor of 𝑇 𝑖 , with a new period 𝐻𝑇 𝑖 and new budget 𝐻𝐶 𝑖 . In the end, all partitions are shrunk by a factor of H, resulting in the original set.
It is trivial to prove the schedulability of the first case, where all partitions have a common period. In the following sections, we discuss formal proofs that enlarging a partition (Lemma 5.3) and shrinking all partitions (Lemma 5.4) preserves the schedulability of the system. Lemma 5.3 (Enlarging a partition preserves the schedulability). Assume that the original partition set is Γ. Partition Π 𝑖 ∈ Γ is enlarged by a factor of k, resulting in the new partition set Γ ′ . If Γ is schedulable, Γ ′ must also be schedulable Lemma 5.4 (Shrinking all partitions by a common factor preserves the schedulability). Assume that the original partition set is Γ. Also assume there exists a common factor k, such that for any partition Π 𝑖 ∈ Γ, its period and budget are multiples of k. By dividing all partitions' periods and budgets by k, we obtain a new partition set, Γ ′ . If Γ is schedulable, Γ ′ must also be schedulable
This section explains how we prove Lemma 5.3. Here, schedulability is specified using the braided virtual timeline, 𝜋, whose construction is illustrated in Fig. 9. Even though partition priorities vary Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation 127:17
over time, we observe that it is possible to account for the aggregate interference between partitions in a systematic way. We define the aggregate interference as a ghost state in Fig. 9 Here, 𝐼 𝑖 (⌊𝑡/𝑇 𝑖 ⌋) denotes the amount of temporal interference incurred on Π 𝑖 in the ⌊𝑡/𝑇 𝑖 ⌋-th period, i.e., within the
In particular, it complements the virtual time for Π 𝑖 in that upon any invocation of the scheduler, either its virtual time or the interference will increment by 1. This leads to the following lemma.
Lemma 5.5. Temporal interference and virtual time complement each other
Thus, the reasoning of a partition's virtual time reduces to the reasoning of the amount of temporal interference it experiences. We further demonstrate below that this aggregate value can be broken down into portions that allow relatively straightforward computation.
Breaking down the temporal interference. Here, we demonstrate how the aggregate interference can be constructed under the EDF scheduling. Fig. 14 illustrates two different ways a partition Π 𝑗 may interfere with Π 𝑖 . Here, the period of Π 𝑖 spans from 𝑡 𝑠 to 𝑡 𝑒 , where 𝑡 𝑒 = 𝑡 𝑠 + 𝑇 𝑖 . Above it, the blue blocks represent the execution of Π 𝑗 , where 𝑎 𝑗 and 𝑒 𝑗 denote its first and last arrival within [𝑡 𝑠 , 𝑡 𝑒 ), respectively. The intuition is that any interference must come from the unfinished workload of other partitions, which happen to occupy a higher priority at the moment. We categorize them as below.
• If a period of Π 𝑗 starts before 𝑡 𝑠 but ends within [𝑡 𝑠 , 𝑡 𝑒 ), as illustrated by the period that ends at 𝑎 𝑗 , a portion of its execution will preempt Π 𝑖 and count toward the temporal interference. We call it the remaining workload because only the portion that is not finished before 𝑡 𝑠 will interfere with Π 𝑖 . We use 𝑤𝑟 𝑖 (Π 𝑗 , 𝜋 𝑗 , 𝑡 𝑠 , 𝑡 𝑒 ) to denote it since the value depends on Π 𝑗 's remaining budget, which is easily computable if 𝜋 𝑗 is known. • Otherwise, if a whole period of Π 𝑗 is within the window [𝑡 𝑠 , 𝑡 𝑒 ), it will execute for its full budget before Π 𝑖 can finish. We call it the whole period workload and denote it as 𝑤𝑤 𝑖 (Π 𝑗 , 𝑡 𝑠 , 𝑡 𝑒 ). In the remainder of this paper, we use Γ to denote the set of partitions in the system. 𝑊 𝑅 𝑖 (Γ, 𝑡 𝑠 , 𝑡 𝑒 ) represents the total remaining workload from all other partitions, i.e. it equals 𝑗≠𝑖 𝑤𝑟 𝑖 (Π 𝑗 , 𝜋 𝑗 , 𝑡 𝑠 , 𝑡 𝑒 ).
Similarly, we let 𝑊𝑊 𝑖 (Γ, 𝑡 𝑠 , 𝑡 𝑒 ) stand for the total whole-period workload from all other partitions. The sum of the two is denoted as 𝑊 𝑖 (Γ, 𝑡 𝑠 , 𝑡 𝑒 ), which includes all other partitions' workloads that may interfere with Π 𝑖 within a particular window [𝑡 𝑠 , 𝑡 𝑒 ).
Lastly, we prove that this accounting of workload indeed serves as an upper bound on the amount of interference. Why is it a bound instead of equaling the exact interference? Recall that we do not have a proof for the system's schedulability yet. Given such a situation, the best we can do is to 15. Enlarging Π 𝑖 by a factor of k prove that the exact interference cannot go beyond the total workload, which is constrained by the budget enforcement mechanism. It requires a schedulability proof to demonstrate that the full workload will be carried out and count as interference.
Lemma 5.6. The total workload is a faithful upper bound on the interference. For any partition Π 𝑖 ∈ Γ, and any of its period [𝑘 * 𝑇 𝑖 , 𝑘 * 𝑇 𝑖 + 𝑇 𝑖 ),
Proof. Recall that the aggregate interference is defined iteratively as in Fig. 9. At each step t, if the time slot [𝑡, 𝑡 + 1) counts as interference, it must be occupied by some partition whose deadline is closer than 𝑡 + 𝑇 𝑖 , thus included in the total workload. □
On top of it, the reasoning of braided virtual timelines reduces to the reasoning of workloads from other partitions, with formal proof that such a computation of workloads is a correct bound on a partition's temporal behavior.
Assume that the original set is Γ and the partition Π 𝑖 ∈ Γ is enlarged by a factor of k, resulting in the set Γ ′ . Given that Γ is schedulable, we now demonstrate the proof that Γ ′ is also schedulable. We consider the updated Π 𝑖 (denoted as Π ′ 𝑖 ) and other partitions separately. Lemma 5.7. The enlarged partition itself is schedulable.
Proof. Fig. 15 illustrates the schedule of a system before (the top half) and after (the bottom half) the enlarging of Π 𝑖 . As shown in the figure, the priority of Π ′ 𝑖 is effectively lowered after its enlargement, and the execution of other partitions is shifted earlier compared to the schedule before. Nevertheless, despite the variation in the actual schedule, the interference from other partitions does not increase because their aggregate workload from time 0 to 𝑡 𝑒 does not change, and the portion that is finished before 𝑡 𝑠 can only become bigger instead of smaller. On the other hand, the schedulability of Π 𝑖 implies that all periods of Π 𝑖 are schedulable within [𝑡 𝑠 , 𝑡 𝑒 ), as shown in the top half of the figure. Combining the two factors, merging these periods (by enlarging the partition) will leave at least 𝑘 * 𝐶 𝑖 available time for Π ′ 𝑖 execution. Thus Π ′ 𝑖 is schedulable. □
On the other hand, an enlarged partition incurs less interference on others. The intuition is that the enlargement in effect combines multiple periods together, lowering their overall priority. We omit proof details in this paper. These two properties together prove that enlarging a partition preserves the schedulability of the system.
Finally, we examine the last step in Example 5.2, i.e., shrinking all partitions by a common factor. Fig. 16 illustrates that the two schedules before and after the shrinking match each other by a factor of k. It is straightforward to see that shrinking the entire partition set can be viewed as adopting a different measurement of time and should not affect the schedulability of the system. We omit proof details in this paper.
This concludes the schedulability proof of the original partition set.
Notice that this paper aims to tackle the information flow security challenge in real-time systems. As discussed in Sec. 2.2, this is a unique problem for systems that integrate potentially untrusted partitions and that schedule them in a non-static manner. For traditional real-time systems that do not suffer from information flow security vulnerabilities, they can usually adopt the same EDF scheduler (Fig. 7) to schedule real-time tasks. In this situation, temporal isolation means schedulability, i.e., each task is given its full budget within every period, regardless of the behavior of other tasks. Our framework can be easily applied to reason about the schedulability of tasks, just by replacing partition parameters in this section with task parameters.
In this section, we explain the local scheduling within a partition and prove the temporal isolation property under the EDF-based partition scheduling. 17 shows the local scheduler for a partition. Here, 𝑝 𝑖 and 𝑒 𝑖 denote the period and budget of task 𝜏 𝑖 . It uses an array index to track the start of new periods for each task. It also maintains an array, 𝑄 𝑡𝑎𝑠𝑘 , to enforce tasks' budgets. At any invocation, it schedules the highest-priority task that is available to execute. Otherwise, an idle task will execute.
Notice that lsched relies on the global time, t, to maintain the index and 𝑄 𝑡𝑎𝑠𝑘 array for its tasks. This makes it vulnerable to interferences from other partitions. For example, as illustrated in Fig. 2, different invocation points of the enclosing partition (time 0, 1, and 5 in (a) vs. time 2, 3, and 6 in (b)) may result in a different schedule of its tasks. Such reordering may lead to illegal information flow between partitions, as described in Sec. 2.2.
As discussed in Sec. 6.1, the application of hierarchical scheduling may lead to temporal interference and further covert channels between partitions.
There are two approaches that we can take to address this vulnerability. One is to adopt a more sophisticated local schedule transformation that buffers task arrivals so that the resulting schedule is deterministic [Yoon et al. 2021]. Fig. 19 illustrates a secured partition containing the green task (𝜏 1 ) and the red task (𝜏 0 ). Unlike in Fig. 2, this secure partition defers the arrival of task 𝜏 0 so that it produces consistent schedules.
The other approach is to impose restrictions on task arrivals such that they are deterministic in the partition's local view despite that the partition schedule floats around (e.g., being preempted at different points in different runs). More specifically, we require that tasks' periods are multiples of the partitions' period and that tasks' arrivals are always synchronized with the boundaries of the partition's periods (i.e., 'bound' tasks [Davis and Burns 2005]). Fig. 20 demonstrates that bound tasks exhibit consistent arrival patterns regardless of other partitions. This is common among real-time applications where tasks must execute periodically and are synchronized with the base period of their enclosing partition. We take the second approach in this paper.
In this section, we formally prove that the local scheduler of a partition is oblivious to other partitions if its tasks' parameters are properly restricted. Fig. 18 shows such an oblivious local scheduler. Instead of relying on the global time, obliv_lsched maintains its own local time, lt, which only increments when the enclosing partition is scheduled. Assume that the partition has
This work builds on top of real-time CertiKOS [Liu et al. 2020], a single-core OS kernel featuring user-level preemption and a fixed-priority scheduler. We extend it with a hierarchical scheduler with EDF partitions and fixed-priority local schedulers (as shown in Fig. 17) in each partition. Budget enforcement is imposed on both partition-and task-level schedulers.
Evaluation Setup. The system is measured on an Intel NUC mini PC with an Intel Core i5-7300U processor operating at 2.6GHz (Turbo Boost is disabled) and the main memory of 8GB. The local APIC timers are configured to generate timer interrupts every millisecond, while the task and partition scheduling granularity are at every tick. This is already practical for a system with a limited number of tasks. We leave the optimization toward a more efficient task look-up and a tickless scheduling model for future work.
The evaluation consists of three parts: micro-benchmark, macro-benchmark, and temporal isolation. The first two are intended to evaluate the feasibility of using the verified scheduler in practice, while the last one is intended to show that temporal isolation is guaranteed.
Micro-benchmark. We first measure the cost of individual scheduler operations to reveal the overhead introduced by the hierarchical scheduler. We execute the task set shown in Table . 1 on CertiKOS for 5 minutes and collect the duration of each scheduler operation. To examine the impact of different workloads on the overheads, we vary the number of loaded partitions for multiple execution rounds.
Fig. 22-(a) presents the cost of re-schedule, in which the partition-level scheduler first selects a partition and then asks its local scheduler to select the next task to run. As shown in Fig. 7, we use a while loop to search the partition with the earliest deadline. Thus, its cost is proportional to the total number of partitions. To be noted, the cost of operations is measured in CPU cycles, which are collected by inserting RTDSC instructions at the beginning (𝑠 𝑖 ) and end (𝑒 𝑖 ) of each scheduler operation. We use 𝑖=1..𝑁 𝑒 𝑖 -𝑠 𝑖 𝑁 -𝑂 𝜖 to compute the average operation overhead, where 𝑁 is the total number of operation invocations during the measurement period. 𝑂 𝜖 is the performance measurement framework overhead which is calculated by instrumenting an empty function. We disabled Turbo Boost to ensure the TSC count equals the CPU cycle. Comparing the partition reschedule overhead (Fig. 22-(b)) with the whole re-schedule operation (Fig. 22-(a)), we can find that the partition-level scheduling does not impose a significant extra overhead.
Fig. 22-(c) shows the partition-budget replenishment operation, which occurs when a new period of a partition begins. The latency of such operation is minimal because this operation is essentially two instructions: an add instruction (of the utilization of the current scheduler workload and the admitting task) and a comparison (<100) instruction. Fig. 22-(d) shows the cost of partition depletion operation. It is called when the budget of a partition is depleted ś the scheduler will suspend the partition. The costs of partition replenishment and partition depletion are both negligible and do not increase with the number of partitions.
Macro-benchmark. To evaluate the overall overhead introduced by the hierarchical scheduler, we use task response time measured from the moment when a task arrives to when it completes its execution. For measurements, we instrument the scheduler with a response time trace ś the CPU cycle of the beginning and end time points are recorded by the scheduler. Because the response time of a task varies in the different periods due to the task/partition-level preemption, we compare the recorded response time trace with the nominal response times (i.e., analytically calculated from task parameters). We reuse the task set that is defined in Table . 1, taking Partitions 1ś4 and multiplying their budgets and all the execution times by 2. We collected the response time trace for 20 seconds from CertiKOS. We define the overhead as the difference of the measured response time from the nominal one. As Table 2 shows, the overall overhead is considerably small when considering that the response times are in milliseconds (from 2 ms to about 800 ms). Temporal isolation. To demonstrate the obliviousness of a partition's local scheduling of tasks, we execute the same partition alone, with another partition, and with three other partitions, respectively. We instrument the scheduler with a set of traces, where each of them corresponds to a partition. At each schedule point, when the local_sched() function returns, we record the task ID and the global time for the current partition. We reuse the task set that is defined in Table . 1, taking the first four partitions and multiplying the budget and all execution time for each task in the first three of them by 3 (hence the total utilization is 100%). This demonstrates the property that is stated in Theorem 6.1; that is, a partition's local behavior is indeed oblivious to other partitions. For each partition activation (after their arrival, marked as '↑'), even if it is preempted by some other partitions, e.g., at 150 ms, comparing sub-figures (a), (b), and (c), the local tasks are still scheduled the same as if no partition preemption has occurred. To be noted, Theorem 6.1 holds for all the cases; hence, we only created the single set as an example to demonstrate the property.
Coq proof. We prove in Coq that each partition is reserved its full budget within every period and that task scheduling is oblivious to other partitions.
Fig. 24 details the proof efforts involved in this extension. The main proof challenge of this work, i.e., the dynamic computation of time maps and the high-level reasoning on top of it, takes more than 18k LOC in Coq. On the other hand, the local task scheduler and its obliviousness to other partitions take 11k LOC in Coq.
Task models discussed throughout this paper assume that the kernel overhead is negligible, which is consistent with our performance evaluation result. However, non-preemptible kernel code, the interrupt handler, and the scheduler itself all consume time and eat into resources that are intended for user applications.
On the one hand, existing work reduces kernel overhead by injecting preemption points in lengthy system calls [Klein et al. 2009]. On the other hand, a formal worst-case bound is needed if the temporal reasoning takes into account kernel overhead.
Another subtlety lies in microarchitectural-level interferences between tasks. Even though our schedulability proof guarantees a certain execution time for a user task during each period, the number of executed instructions varies if another task is sharing a common cache line and may evict previously cached entries. Mitigation techniques [Ge et al. 2019;Sha et al. 2016] mainly involve properly partitioning of shared hardware resources, ranging from cache lines to memory banks, so that interference between tasks is reduced.
These techniques are largely orthogonal to the temporal isolation proof in this work, which is specified on a logical notion of time slots, i.e. the duration between two timer interrupts. Nevertheless, mitigations of these caching effects fall into the existing reasoning framework. As discussed in [Heiser et al. 2019], we can encode these microarchitectural resources in the machine model (without concrete numbers for the execution cost) and prove that partitioning decouples the executions of different tasks.
This work adopts a tick-based scheduler, as shown in Fig. 7, which is invoked at every timer interrupt. This is a reasonable setting by itself, and we choose this design for its regularity. However, there exist more sophisticated scheduler implementations that are invoked less frequently to achieve better performance.
For example, a tickless scheduler proactively calculates the next scheduling event (e.g., starting of a new period), and sets the timer interrupt to trigger at the specified future instant (e.g., by utilizing the TSC-deadline mode of a CPU). In this way, the scheduler is only invoked when it needs to update its internal state and recalculate the task to schedule.
Our framework can be extended to accommodate such a tickless setting. The intuition is that the tick-based and tickless schedulers still follow the same scheduling policy. They only differ in their implementations, which matters for performance. Suppose that the EDF scheduler psched in Fig. 7 is replaced by a tickless one, tl_psched. We can prove that the two schedulers' states match with each other every time when tl_psched is invoked. And for time instants when only psched is invoked, its internal state does not change. In this way, we prove the contextual equivalence between the two, and further reasoning can be based on psched as shown in this paper.
Mechanized Schedulability Analysis. One of the motivations for mechanized schedulability analysis is that paper proofs are error-prone. Wilding [Wilding 1998] points out that the original paper proof for EDF in [Liu and Layland 1973] contains errors. Instead, they prove the same schedulability test for EDF using a theorem prover such that the result is machine-checkable. There are also work on the modeling and verification of real-time communication protocols [Dutertre 2000;Zhang et al. 2012] and response time analyses [Cerqueira et al. 2016;Fradet et al. 2018;Maida et al. 2022;Roux et al. 2022]. However, all of them are developed on an abstract model and their results do not apply to any scheduler source code directly. Guo et al. [Guo et al. 2019] tackle the connection between a mechanized schedulability analysis and the scheduler's source code. However, their approach requires intrusive modifications on both sides, and it is unclear whether it is feasible for more sophisticated algorithms such as EDF partitions and their temporal isolation properties.
The recent work by Vanhems et al. [2022] features a mechanized proof for an EDF scheduler implementation. They adopt an abstraction-and-refinement approach to bridge the gap between the high-level reasoning and the concrete scheduler implementation. However, unlike our work, their proof does not connect to a user-facing criterion, e.g., the total utilization of all partitions does not exceed 100%. Instead, they build their proof on top of the assumption that within any arbitrary time interval, the total budget of jobs does not exceed the length of that interval.
A more fundamental difference is in the design goal of the work, which leads to different ways of formalizing scheduling behaviors. Vanhems et al. [2022] was only designed for schedulability of tasks but not for information flow security of partitions, which is all that is expected of traditional real-time systems. As a result, it formalizes schedulability as the absence of deadline miss. On the contrary, this paper aims to prove the confidentiality of partitions. This requires our formalization to be expressive enough to specify the scheduling behavior of both partitions and their tasks. We use braided virtual timeline to faithfully characterize temporal behaviors of individual partitions. Thanks to its expressiveness, we first use this formalization to prove schedulability, which is a property of braided virtual timelines. We then leverage this property to reason about the behavior of a single partition and prove that its local schedule of tasks is not affected by other partitions.
Formal Verification of Real-Time OS Kernels. Most of existing work on verified real-time OS kernels [Andronick et al. 2016;Xu et al. 2016] do not address end-user real-time guarantees, i.e. schedulability of components.
Liu et al. [Liu et al. 2020] propose the virtual timeline framework to address temporal isolation between components. One of their main contributions is a structured way of lifting the reasoning into an abstract domain while guaranteeing the faithfulness of this abstraction. In particular, they leverage the fixed hierarchy among tasks to compute the temporal behavior of each of them in decreasing order of priority. This enables a straightforward static construction of the abstraction, called virtual time maps, but is also a limitation since it is tightly coupled with the fixed-priority scheduling. It cannot extend to other scheduling algorithms directly.
On the contrary, this work proposes a generic abstraction that can describe dynamic-priority scheduling and connect with the scheduler's source code. In particular, it proposes an innovative use of a priority queue to make the precedence relation between tasks explicit, and further constructs time maps dynamically on top of it. This is a significant difference from [Liu et al. 2020] and it reflects a generic structure among preemptive scheduling. For example, fixed-priority scheduling can be easily characterized as a special case where the priority queue remains constant.
OS Kernels and Isolation. OS Kernels have long served the role of managing physical resources and ensuring isolation between different components. While the formal verification of spatial isolation has been tackled by the literature [Murray et al. 2013;Nelson et al. 2017], they do not provide as strong temporal isolation guarantees. For example, both works rely on the static allocation of time slots to establish temporal isolation between components, which is too restrictive. Liu et al. [Liu et al. 2020] verify an OS kernel with both temporal and spatial isolation, but they are limited to the fixed-priority scheduling. As a comparison, our work finds a generic way of handling any preemptive scheduling algorithm and proving related temporal isolation properties.
On the implementation side, Ge et al. [Ge et al. 2019] mitigate micro-architectural-level interferences by making those hardware resources explicit and properly partitioning them among independent tasks. Heiser et al. [Heiser et al. 2019] discuss possible approaches toward its formal verification.
Lyons et al. [Lyons et al. 2018] design a capability-based interface to allow users to reserve CPU bandwidth for critical tasks. Their underlying algorithm is based on sporadic servers. As a comparison, our work can accommodate similar reservation mechanisms (e.g., polling servers) while also providing a formal isolation guarantee. In particular, the EDF algorithm we prove allows us to manage CPU utilization in a compositional way.
This paper addresses dynamic-priority partitions with temporal isolation. In particular, hierarchical scheduling has be historically adopted by centrally developed systems, where all components are trusted and thus there is no security concern. However, with the increasing trend of accommodating multiple real-time applications from different vendors on a single processor, such a scheme may lead to covert channels. We propose using budget-enforcing EDF partitions and imposing restrictions on tasks within a partition to achieve a balance between flexibility, high-utilization, and temporal isolation.
In tackling the challenges with formally verifying EDF partitions, we adopt a dynamic construction of virtual timelines to lift the reasoning of a concrete scheduler into an abstract domain. This is a significant innovation since EDF scheduling results in braided timelines that intersect and shift priorities and are never properly layered on each other. On top of it, we prove that an EDF partition always receives its full budget and that its local task schedule is oblivious to the other partitions. These entail temporal isolation between partitions.
It is a sufficient condition. If the utilization bound test fails, the partitions need to be tested against the exact analysis [Joseph and Pandya 1986]. Proc. ACM Program. Lang., Vol. 6, No. OOPSLA2, Article 127. Publication date: October
Proc. ACM Program. Lang., Vol. 6, No. OOPSLA2, Article 127. Publication date: October 2022.
Mengqi Liu, Zhong Shao, Hao Chen, Man-Ki Yoon, and Jung-Eun Kim