CARNEGIE-MELLON UNIV PITTSBURGH PA PITTSBURGH United States
Pagination or Media Count:
The verification of Cyber-Physical Systems is increasingin importance given the push to deploy complex autonomous features with life-threatening consequences. However, verifying CPS not only demands the verification of the application code but also of the supporting OS. Unfortunately, the complexity of traditional monolithic kernels has prevented their full verification. As a result, a new generation of verified hypervisors capable of hosting a full OS within a VM has been created. Notwithstanding, the verified properties of the hypervisor only apply to the code within it and do not extend to the code running the VM. In this paper we create a new scheduling model with tasks consisting of two parts, an unverified part that runs in the VM and a verified part that runs within the verified hypervisor. The unverified part can contain bugs and hence is considered untrusted. The verified part, on the other hand, is considered trusted. Due to this mixture we call this a mixed-trust task. A mixed-trust task is designed to run only its untrusted part if the execution does not run into any bugs. The untrusted part implements complex computations and has the support of a full-blown OS. However, if this part fails to finished e.g., due tobugs the trusted part is automatically activated by a timer within the trusted hypervisor to ensure some safety property e.g. prevent a crash. The hypervisor ensures that the activation of the trusted part does not depend on the untrusted one. This execution model is implemented by the coordination of a verified non-preemptive scheduler in the hypervisor and a preemptive scheduler in the VM. Both the mixture of schedulers and the required independence of the hypervisor scheduler present key challenges that are addressed in this paper. In the paper we present the schedulability analysis for the mixed-trust scheduler, and its implementation based on the XMHF hypervisor and the ZSRM schedulers.
- Computer Programming and Software