More Like this

1. Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation

   https://doi.org/10.1145/3563290  

   Liu, Mengqi; Shao, Zhong; Chen, Hao; Yoon, Man-Ki; Kim, Jung-Eun (October 2022, Proceedings of the ACM on Programming Languages)

   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
2. Alone together: compositional reasoning and inference for weak isolation

   https://doi.org/10.1145/3158115  

   Kaki, Gowtham; Nagar, Kartik; Najafzadeh, Mahsa; Jagannathan, Suresh (January 2018, Proceedings of the ACM on Programming Languages)

   Serializability is a well-understood correctness criterion that simplifies reasoning about the behavior of concurrent transactions by ensuring they are isolated from each other while they execute. However, enforcing serializable isolation comes at a steep cost in performance because it necessarily restricts opportunities to exploit concurrency even when such opportunities would not violate application-specific invariants. As a result, database systems in practice support, and often encourage, developers to implement transactions using weaker alternatives. These alternatives break the strong isolation guarantees offered by serializable transactions to permit greater concurrency. Unfortunately, the semantics of weak isolation is poorly understood, and usually explained only informally in terms of low-level implementation artifacts. Consequently, verifying high-level correctness properties in such environments remains a challenging problem. To address this issue, we present a novel program logic that enables compositional reasoning about the behavior of concurrently executing weakly-isolated transactions. Recognizing that the proof burden necessary to use this logic may dissuade application developers, we also describe an inference procedure based on this foundation that ascertains the weakest isolation level that still guarantees the safety of high-level consistency assertions associated with such transactions. The key to effective inference is the observation that weakly-isolated transactions can be viewed as functional (monadic) computations over an abstract database state, allowing us to treat their operations as state transformers over the database. This interpretation enables automated verification using off-the-shelf SMT solvers. Our development is parametric over a transaction’s specific isolation semantics, allowing it to be applicable over a range of concurrency control mechanisms. Case studies and experiments on real-world applications (written in an embedded DSL in OCaml) demonstrate the utility of our approach, and provide strong evidence that automated verification of weakly-isolated transactions can be placed on the same formal footing as their strongly-isolated serializable counterparts. 

   more » « less
3. Integrating Formal Schedulability Analysis into a Verified OS Kernel

   Guo, Xiaojie; Lesourd, Maxime; Liu, Mengqi; Rieg, Lionel; Shao, Zhong (July 2019, 31st International Conference on Computer Aided Verification (CAV))

   Formal verification of real-time systems is attractive because these systems often perform critical operations. Unlike non real-time systems, latency and response time guarantees are of critical importance in this setting, as much as functional correctness. Nevertheless, formal verification of real-time OSes usually stops the scheduling analysis at the policy level: they only prove that the scheduler (or its abstract model) satisfies some scheduling policy. In this paper, we go further and connect together Prosa, a verified schedulability analyzer, and RT-CertiKOS, a verified single-core sequential real-time OS kernel. Thus, we get a more general and extensible schedulability analysis proof for RT-CertiKOS, as well a concrete implementation validating Prosa models. It also showcases that it is realistic to connect two completely independent formal developments in a proof assistant. 

   more » « less
4. A Soft-Real-Time-Optimal Semi-Clustered Scheduler with a Constant Tardiness Bound

   https://doi.org/10.1109/RTCSA50079.2020.9203605  

   Ahmed, Shareef; Anderson, James H. (August 2020, Proceedings of the 26th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications)

   null (Ed.)

   Different global and semi-partitioned schedulers have been proposed that are soft-real-time (SRT) optimal for sporadic task systems, meaning they can guarantee bounded deadline tardiness. However, under known analyses, tardiness bounds increase with respect to the number of processors, which reduces the applicability of these schedulers in systems with a large number of processors. In this paper, a semi-clustered scheduler, SC-EDF, is presented that has a constant tardiness bound. SC-EDF partitions tasks into clusters, each of which may include one fractional processor. Each cluster is scheduled by G-EDF, and the fractional processors are realized using Pfair scheduling techniques. 

   more » « less
5. Blinder: Partition-Oblivious Hierarchical Scheduling

   Yoon, Man-Ki; Liu, Mengqi; Chen, Hao; Kim, Jung-Eun; Shao, Zhong (August 2021, Proceedings of the 30th USENIX Security Symposium (USENIX Security 2021))

   null (Ed.)

   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