Towards verified microkernels for real-time mixed-criticality systems

摘要

Today's embedded systems are becoming increasingly complex. We are seeing many devices consolidate both mission-critical real-timesubsystems with convenience functionality such as networking stacks and graphical user interfaces. For example, medical implants suchas pacemakers now provide wireless monitoring and control; bugs within the wireless subsystem must not be able to affect the safetycriticalreal-time operations of the pacemaker. Traditionally, this is achieved by using multiple processors with limited communicationchannels. However, these extra processors add significant overheads of size, weight and power.The mixed-criticality design promises to mitigate these overheads by consolidating multiple subsystems onto a single CPU, but this entailsboth mission-critical and convenience functionality sharing the same processor. In order to enforce isolation between subsystems ofdiffering criticalities, we require a trustworthy supervisor to mediate control over the processor and provide behavioural guarantees.In this thesis, we explore several ingredients required to construct a high-assurance mixed-criticality real-time system. We propose thatthe formal verification and design of the seL4 microkernel makes it highly suited as a trustworthy foundation for these systems. We showhow to compute interrupt response time guarantees which complement seL4's guarantees of functional correctness. We also explore thedesign space for such microkernels, which must balance the competing goals of formal verification and real-time responsiveness. Weinvestigate the limits of interrupt latency for non-preemptible microkernels, and question whether fully-preemptible kernels are necessaryfor low-interrupt latency applications.We show that C can achieve equivalent performance to hand-optimised assembly for performance-critical kernel code, thereby allowingsuch code to be formally verified using C verification frameworks and maintain trustworthiness.We also present a practical framework for applying the capabilities of model checkers and SMT solvers to reason about compiled binaries.This framework can automatically detect infeasible paths and compute loop bounds, increasing the accuracy and the trustworthiness ofresponse time guarantees.