Trustworthy Systems

Towards verified microkernels for real-time mixed-criticality systems

Authors

Bernard Blackham

NICTA

UNSW

2013 ACM SIGBED Paul Caspi Memorial Dissertation Award and John Makepeace Bennett Award for Australasian Distinguished Doctoral Dissertation

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 safety- critical 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.

BibTeX Entry

  @phdthesis{Blackham:phd,
    address          = {Sydney, Australia},
    author           = {Blackham, Bernard},
    keywords         = {real-time systems; worst-case execution time; microkernels; mixed-criticality systems; reliable
                        systems},
    month            = oct,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7634.pdf},
    school           = {UNSW},
    title            = {Towards Verified Microkernels for Real-Time Mixed-Criticality Systems},
    year             = {2013}
  }

Download