Abstract
Today's embedded systems are becoming increasingly complex. We are seeing many devices consolidate both mission-critical real-time
subsystems with convenience functionality such as networking stacks and graphical user interfaces. For example, medical implants such
as pacemakers now provide wireless monitoring and control; bugs within the wireless subsystem must not be able to affect the safetycritical
real-time operations of the pacemaker. Traditionally, this is achieved by using multiple processors with limited communication
channels. 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 entails
both mission-critical and convenience functionality sharing the same processor. In order to enforce isolation between subsystems of
differing 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 that
the formal verification and design of the seL4 microkernel makes it highly suited as a trustworthy foundation for these systems. We show
how to compute interrupt response time guarantees which complement seL4's guarantees of functional correctness. We also explore the
design space for such microkernels, which must balance the competing goals of formal verification and real-time responsiveness. We
investigate the limits of interrupt latency for non-preemptible microkernels, and question whether fully-preemptible kernels are necessary
for low-interrupt latency applications.
We show that C can achieve equivalent performance to hand-optimised assembly for performance-critical kernel code, thereby allowing
such 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 of
response time guarantees.