Aim: develop a trustworthy platform for building mixed-criticality real-time systems.
Overview: Many trusted systems (i.e. systems whose safety, security or reliability we trust) must deliver a response to an external stimulus within a certain time period, and are therefore critical real-time systems. These include cyber-physical systems, such as medical implants (e.g. pacemakers), avionic systems and industrial controllers. A failure to perform a computation or operation within a given time may have catastrophic consequences in these environments.
Such systems are increasingly complex. An example are wearable or implanted medical devices, which combine life-supporting functionality with user interfaces to allow monitoring by the patient or network drivers and protocol stacks for remote monitoring. Other devices contain multiple real-time functions with different levels of criticality, such as automotive safety and control systems.
Subsystems of different criticality must be strongly isolated, in order to prevent malfunction of a less critical function affecting a highly-critical one. This isolation is often achieved by physical separation, however, this is frequently impossible, due to space and energy constraints (e.g. in medical implants) or where the number of different functions is becoming too large (e.g. in cars).
Trustworthiness of such a system can only be achieved if strong functional as well as temporal isolation (with tightly-controlled communication) can be guaranteed between subsystems. This puts stringent requirements on the underlying operating system, whose job it is to provide this isolation. Our real-time systems work aims at providing this foundation for trustworthiness. We focus primarily on the seL4 microkernel, as its formal verification already eliminates many sources of failure. Additional requirements for supporting mixed-criticality systems include:
Kernel mechanisms for real-time systems: We evolved the seL4 API to support general mixed-criticality systems. This resulted in mechanisms to treat time as a first-class resource in seL4. We introduced a notion of scheduling contexts, which are capability-protected kernel objects that represent the right to access the CPU and that can get passed along IPC channels. A thread can only execute if it is associated with a scheduling context.
Scheduling contexts define a thread's time budget and a period, and they guarantee that over the period the thread cannot consume more than its budget. This allows the construction of responsive systems, where less critical but latency-sensitive threads can preempt critical threads operating at longer time scales, while still guaranteeing that the critical threads meet their deadlines.
The ability to guarantee deadlines can even be maintained where threads of different criticalities share a service, time-out exceptions allow recovering from misbehaving low-criticality threads.
The new MCS variant of seL4 is presently undergoing verification. As it is backward compatible with the previously verified base seL4 kernel, it will become the new standard once its verification is complete.
Worst-case execution-time analysis tools: We created a toolset called graph-to-graph, which can analyse the WCET of the complete seL4 kernel (and other software). graph-to-graph utilises our translation validation framework to link the semantics-poor binary (which is the subject to the WCET analysis) to the semantics-rich C environment and all the theorems and invariants we have proved about the C code in the context of the functional correctness proof of seL4. This allows us to add proofs of difficult loop bounds in the existing verification framework, and link those proofs to the binary in a high-assurance fashion. Once those manual proofs are added, the rest of the analysis is fully automated.
WCET analysis of seL4: Using the above toolset we conducted a complete, sound analysis of latencies of all kernel operations on modern ARM processors (ARM11 and Cortex A8). This is the first ever published complete timing analysis of a protected multitasking kernel.
Improving worst-case responsiveness of seL4: Based on this analysis we improved the worst-case execution time of seL4, whilst maintaining its verifiability. This involves careful examination and adaptation of the kernel design and implementation.
Click here to download our tools used for computing the worst-case execution time of seL4 from here.
Gernot Heiser, firstname.lastname@example.org
The formally verified seL4 microkernel – a high-assurance foundation for MCS
Keynote at IEEE Conference on Embedded and Real-Time Computing and Applications, August, 2020
Verified seL4 on secure RISC-V processors
at linux.conf.au, Gold Coast, January, 2020
|Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser|
Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time
EuroSys Conference, Porto, Portugal, April, 2018
For safety's sake: we need a new hardware-software contract!
IEEE Design and Test, Volume 35, Issue 2, pp. 27-30, March, 2018
Flying autonomous aircraft: Mixed-criticality support in seL4
at linux.conf.au, Sydney, January, 2018
Mixed-criticality scheduling and resource sharing for high-assurance operating systems
PhD Thesis, UNSW, 2018
|Thomas Sewell, Felix Kam and Gernot Heiser|
High-assurance timing analysis for a high-assurance real-time OS
Real-Time Systems, Volume 53, Issue 5, pp. 812-853, September, 2017
Translation validation for verified, efficient and timely operating systems
PhD Thesis, UNSW, Sydney, Australia, 2017
|Thomas Sewell, Chi Kam and Gernot Heiser|
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016
Outstanding Paper award
||Anna Lyons and Gernot Heiser|
Mixed-criticality support in a high-assurance, general-purpose microkernel
Workshop on Mixed Criticality Systems, pp. 9–14, Rome, Italy, December, 2014
||Bernard Blackham, Mark Liffiton and Gernot Heiser|
Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 169–178, Berlin, Germany, April, 2014
Towards verified microkernels for real-time mixed-criticality systems
PhD Thesis, UNSW, Sydney, Australia, October, 2013
2013 ACM SIGBED Paul Caspi Memorial Dissertation Award and John Makepeace Bennett Award for Australasian Distinguished Doctoral Dissertation
||Bernard Blackham and Gernot Heiser|
Sequoll: A framework for model checking binaries
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 97–106, Philadelphia, USA, April, 2013
Best Paper Award
||Bernard Blackham, Vernon Tang and Gernot Heiser|
To preempt or not to preempt, that is the question
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
||Bernard Blackham, Yao Shi and Gernot Heiser|
Improving interrupt response time in a verifiable protected microkernel
EuroSys Conference, pp. 323–336, Bern, Switzerland, April, 2012
|Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser|
Timing analysis of a protected operating system kernel
IEEE Real-Time Systems Symposium, pp. 339–348, Vienna, Austria, November, 2011
|Bernard Blackham, Yao Shi and Gernot Heiser|
Protected hard real-time: The next frontier
Asia-Pacific Workshop on Systems (APSys), pp. 5, Shanghai, China, July, 2011
|Stefan M. Petters, Martin Lawitzky, Ryan Heffernan and Kevin Elphinstone|
Towards real multi-criticality scheduling
IEEE Conference on Embedded and Real-Time Computing and Applications, pp. 155–164, Beijing, China, August, 2009
Hypervisors for consumer electronics
IEEE Consumer Communications and Networking Conference, pp. 1–5, Las Vegas, NV, USA, January, 2009
|Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan Petters|
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007
|Stefan Petters, Patryk Zadarnowski and Gernot Heiser|
Measurements or static analysis or both?
Workshop on Worst-Case Execution-Time Analysis, pp. 5–11, Pisa, Italy, December, 2007