skip to main content


Title: Blinder: Partition-Oblivious Hierarchical Scheduling
Hierarchical scheduling enables modular reasoning of the temporal behavior of individual applications by partitioning CPU time and thus isolating potential mis-behavior. However, conventional time-partitioning mechanisms fail to achieve strong temporal isolation from a security viewpoint; variations in the executions of partitions can be perceived by others, which enables an algorithmic covert timing-channel between partitions that are completely isolated from each other in the utilization of time. Thus, we present a run-time algorithm that makes partitions oblivious to others' varying behaviors even when an adversary has full control over their timings. It enables the use of dynamic time-partitioning mechanisms that provide improved responsiveness, while guaranteeing the algorithmic-level non-interference that static approaches would achieve. From an implementation on an existing operating system, we evaluate the costs of the solution in terms of the responsiveness as well as scheduling overhead.  more » « less
Award ID(s):
1763399 1715154 1521523 1945541
NSF-PAR ID:
10230367
Author(s) / Creator(s):
; ; ; ;
Date Published:
Journal Name:
Proceedings of the 30th USENIX Security Symposium (USENIX Security 2021)
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Timing predictability is a precondition for successful communication over a covert timing channel. Real-time systems are particularly vulnerable to timing channels because real-time applications can easily have temporal locality due to limited uncertainty in schedules. In this paper, we show that real-time applications can create hidden information flow even when the temporal isolation among the time partitions is strictly enforced. We then introduce an online algorithm that randomizes time-partition schedules to reduce the temporal locality, while guaranteeing the schedulability of, and thus the temporal isolation among, time partitions. We also present an analysis of the cost of the randomization on the responsiveness of real-time tasks. From an implementation on a Linux-based real-time operating system, we validate the analysis and evaluate the scheduling overhead as well as the impact on an experimental real-time system. 
    more » « less
  2. Distributed optimization algorithms are proposed to, potentially, reduce the computational time of large-scale optimization problems, such as security-constrained economic dispatch (SCED). While various geographical decomposition strategies have been presented in the literature, we proposed a temporal decomposition strategy to divide the SCED problem over the considered scheduling horizon. The proposed algorithm breaks SCED over the scheduling time and takes advantage of parallel computing using multi-core machines. In this paper, we investigate how to partition the overall time horizon. We study the effect of the number of partitions (i.e., SCED subproblems) on the overall performance of the distributed coordination algorithm and the effect of partitioning time interval on the optimal solution. In addition, the impact of system loading condition and ramp limits of the generating units on the number of iterations and solution time are analyzed. The results show that by increasing the number of subproblems, the computational burden of each subproblem is reduced, but more shared variables and constraints need to be modeled between the subproblems. This can result in increasing the total number of iterations and consequently the solution time. Moreover, since the load behavior affects the active ramping between the subproblems, the breaking hour determines the difference between shared variables. Hence, the optimal number of subproblems is problem dependent. A 3-bus and the IEEE 118-bus system are selected to analyze the effect of the number of partitions. 
    more » « less
  3. Ragusa, Maria Alessandra (Ed.)
    We study scheduling mechanisms that explore the trade-off between containing the spread of COVID-19 and performing in-person activity in organizations. Our mechanisms, referred to as group scheduling , are based on partitioning the population randomly into groups and scheduling each group on appropriate days with possible gaps (when no one is working and all are quarantined). Each group interacts with no other group and, importantly, any person who is symptomatic in a group is quarantined. We show that our mechanisms effectively trade-off in-person activity for more effective control of the COVID-19 virus spread. In particular, we show that a mechanism which partitions the population into two groups that alternatively work in-person for five days each, flatlines the number of COVID-19 cases quite effectively, while still maintaining in-person activity at 70% of pre-COVID-19 level. Other mechanisms that partitions into two groups with less continuous work days or more spacing or three groups achieve even more aggressive control of the virus at the cost of a somewhat lower in-person activity (about 50%). We demonstrate the efficacy of our mechanisms by theoretical analysis and extensive experimental simulations on various epidemiological models based on real-world data. 
    more » « less
  4. Real-time systems power safety-critical applications that require strong isolation among each other. Such isolation needs to be enforced at two orthogonal levels. On the micro-architectural level, this mainly involves avoiding interference through micro-architectural states, such as cache lines. On the algorithmic level, this is usually achieved by adopting real-time partitions to reserve resources for each application. Implementations of such systems are often complex and require formal verification to guarantee proper isolation. In this paper, we focus on algorithmic isolation, which is mainly related to scheduling-induced interferences. We address earliest-deadline-first (EDF) partitions to achieve compositionality and utilization, while imposing constraints on tasks' periods and enforcing budgets on these periodic partitions to ensure isolation between each other. The formal verification of such a real-time OS kernel is challenging due to the inherent complexity of the dynamic priority assignment on the partition level. We tackle this problem by adopting a dynamically constructed abstraction to lift the reasoning of a concrete scheduler into an abstract domain. Using this framework, we verify a real-time operating system kernel with budget-enforcing EDF partitions and prove that it indeed ensures isolation between partitions. All the proofs are mechanized in Coq. 
    more » « less
  5. Real-time systems power safety-critical applications that require strong isolation among each other. Such isolation needs to be enforced at two orthogonal levels. On the micro-architectural level, this mainly involves avoiding interference through micro-architectural states, such as cache lines. On the algorithmic level, this is usually achieved by adopting real-time partitions to reserve resources for each application. Implementations of such systems are often complex and require formal verification to guarantee proper isolation. In this paper, we focus on algorithmic isolation, which is mainly related to scheduling-induced interferences. We address earliest-deadline-first (EDF) partitions to achieve compositionality and utilization, while imposing constraints on tasks' periods and enforcing budgets on these periodic partitions to ensure isolation between each other. The formal verification of such a real-time OS kernel is challenging due to the inherent complexity of the dynamic priority assignment on the partition level. We tackle this problem by adopting a dynamically constructed abstraction to lift the reasoning of a concrete scheduler into an abstract domain. Using this framework, we verify a real-time operating system kernel with budget-enforcing EDF partitions and prove that it indeed ensures isolation between partitions. All the proofs are mechanized in Coq. 
    more » « less