Trustworthy Systems

Timing analysis of a protected operating system kernel

Authors

Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser

NICTA

UNSW

National University of Singapore

Abstract

Operating systems offering virtual memory and protected address spaces have been an elusive target of static worst-case execution time (WCET) analysis. This is due to a combination of size, unstructured code and tight coupling with hardware. As a result, hard real-time systems are usually developed without memory protection, perhaps utilizing a lightweight real-time executive to provide OS abstractions.

This paper presents a WCET analysis of seL4, a third-generation microkernel. seL4 is the world’s first formally-verified operating-system kernel, featuring machine-checked correctness proofs of its complete functionality. This makes seL4 an ideal platform for security-critical systems. Adding temporal guarantees makes seL4 also a compelling platform for safety- and timing-critical systems. It creates a foundation for integrating hard real-time systems with less critical time-sharing components on the same processor, supporting enhanced functionality while keeping hardware and development costs low.

We believe this is one of the largest code bases on which a fully context-aware WCET analysis has been performed. This analysis is made possible due to the minimalistic nature of modern microkernels, and the degree of structure in seL4’s source code.

BibTeX Entry

  @inproceedings{Blackham_SCRH_11,
    address          = {Vienna, Austria},
    author           = {Blackham, Bernard and Shi, Yao and Chattopadhyay, Sudipta and Roychoudhury, Abhik and Heiser, Gernot},
    booktitle        = {IEEE Real-Time Systems Symposium},
    keywords         = {wcet, microkernels, trusted systems, real-time systems},
    month            = nov,
    pages            = {339--348},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/4863.pdf},
    publisher        = {IEEE Computer Society},
    title            = {Timing Analysis of a Protected Operating System Kernel},
    year             = {2011}
  }

Download