Red Hat Collaboratory Colloquium Series: Dionisio de Niz, Mixed-Trust Real-Time Computation

Abstract
Certification authorities (e.g., FAA) allow the validation of different parts of a system with different degrees of rigor depending on their level of criticality. Formal methods have been recognized as important to verify safety-critical components. Unfortunately, a verified property can be easily compromised if the verified components are not protected from misbehaviors of the unverified ones (e.g., due to bugs). Thus, trust requires that both verification and protection of components are jointly considered. 

A key challenge to building trust is the complexity of today’s operating systems (OSs) making them impractical to verify. Building a trusted system is challenging because the underlying operating systems (OSs) that implement protection mechanisms are extremely hard (if even possible) to thoroughly verify. Thus, there has been a trend to minimize the trusted computing base (TCB) by developing small verified hypervisors (HVs) and microkernels, e.g., seL4, CertiKOS}, and uberXMHF. In these systems, trusted and untrusted components co-exist on a single hardware platform but in a completely isolated and disjoint manner. We thus call this approach disjoint-trust computing. The fundamental limitation of disjoint-trust computing is that it does not allow the use of untrusted components in critical functionality whose safety must be assured through verification. 

In this talk, we present the real-time mixed-trust computing (RT-MTC) framework. Unlike disjoint-trust computing, it gives the flexibility to use untrusted components even for CPS critical functionality. In this framework, untrusted components are monitored by verified components ensuring that the output of the untrusted components always lead to safe states (e.g., avoiding crashes). These monitoring components are known as logical enforcers. To ensure trust, these enforcers are protected by a verified micro-hypervisor. To preserve the timing guarantees of the system, RT-MTC uses temporal enforcers, which are small, self-contained codeblocks that perform a default safety action (e.g., hover in a quadrotor) if the untrusted component has not produced a correct output by a specified time. Temporal enforcers are contained within the verified micro-hypervisor. Our framework incorporates two schedulers: (i) a preemptive fixed-priority scheduler in the VM to run the untrusted components and (ii) a non-preemptive fixed-priority scheduler within the HV to run trusted components. To verify the timing correctness of safety-critical applications in our mixed-trust framework, we develop a new task model and schedulability analysis. We also present the design and implementation of a coordination protocol between the two schedulers to preserve the synchronization between the trusted and untrusted components while preventing dependencies that can compromise the trusted component. 

Finally, we discuss the extension of this framework for trusted mode degradation. While a number of real-time modal models have been proposed, they fail to address the challenges presented here in at least two important respects. First, previous models consider mode transitions as simple task parameter changes without taking into account the computation required by the transition and the synchronization between the modes and the transition. Second, previous work does not address the challenges imposed by the need to preserve safety guarantees during the transition. Our work addresses these issues by extending the RT-MTC framework to include degradation modes and creating a schedulability model based on the digraph model that supports this extension.

Speaker
Dionisio de Niz is a Principal Researcher and the Technical Director of the Assuring Cyber-Physical Systems directorate at the Software Engineering Institute at Carnegie Mellon University. He received a Master of Science in Information Networking and a Ph.D. in Electrical and Computer Engineering both from Carnegie Mellon University. His research interest includes Cyber-Physical Systems, Real-Time Systems, Model-Based Engineering (MBE), and Security of CPS. In the Real-time arena he has recently focused on multicore processors and mixed-criticality scheduling and more recently in real-time mixed-trust computing. In MBE, he has focused on the symbolic integration of analysis using analysis contracts. Dr. de Niz co-edited and co-authored the book “Cyber-Physical Systems” where the authors discuss different application areas of CPS and the different foundational domains including real-time scheduling, logical verification, and CPS security. He has participated and/or helped in the organization of multiple workshops with industry on real-time multicore systems (two co-sponsored by the FAA and three by different services of the US military) and Safety Assurance of Nuclear Energy. He is a member of the executive committee of the IEEE Technical Committee on Real-Time Systems. Dr. de Niz participates regularly in technical program committees of the real-time systems conferences such as RTSS, RTAS, RTCSA, etc. where he also publishes a large part of his work. 

Location
In Person
Boston University
Center for Data Sciences (CDS)
665 Commonwealth Ave
Room 365 (3rd floor)
Boston, MA 02215

Lunch will be available for in-person attendees

Remote Access
Click to access meeting via Zoom
If the direct link doesn’t work use Meeting ID: 944 0022 9257; Passcode: 564023

About the Collaboratory
A partnership between Red Hat and Boston University, the Red Hat Collaboratory connects BU faculty and students with industry practitioners working in open-source software communities. The Collaboratory aims to advance research focused on emerging technologies in a number of areas including operating systems, cloud computing services, machine learning and automation, and big data platforms.