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.
Current |
Past
|
Gernot Heiser, gernot@unsw.edu.au
|
 
|
Gernot Heiser 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 |
|
|
|
Gernot Heiser 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 |
|
|
|
Gernot Heiser For safety's sake: we need a new hardware-software contract! IEEE Design and Test, Volume 35, Issue 2, pp. 27-30, March, 2018 |
|
|
|
Gernot Heiser Flying autonomous aircraft: Mixed-criticality support in seL4 at linux.conf.au, Sydney, January, 2018 |
|
|
|
Anna Lyons 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 |
|
|
|
Thomas Sewell 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 |
|
|
|
Bernard Blackham 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 |
|
|
|
Gernot Heiser 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 M. 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 M. 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 |