Mixed-Criticality Real-time Systems

• 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:

  • specification and analysis to the temporal properties of seL4-based systems
  • appropriate kernel mechanisms for supporting scheduling and isolated execution of multiple real-time and best-effort programs on seL4.

• Temporal properties of seL4-based systems: A prerequisite for reasoning about temporal properties of software running in protected mode is an understanding of the worst-case execution time (WCET) of kernel operations, in particular, interrupt latencies. Here we are working on:

  • Computing the worst-case execution time (and thus interrupt latency) of seL4. We have succeeded in 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 the worst-case execution time of seL4, whilst maintaining its verifiability. This involves careful examination and adaptation of the kernel design and implementation.
  • Improving the average-case performance of seL4, again while maintaining verifiability. This improves schedulability of lower-criticality workloads.

• Kernel mechanisms for real-time systems: We are evolving the seL4 API to support general mixed-criticality systems. This involves investigating the most appropriate kernel mechanisms for scheduling real-time tasks and sharing resources between them, which involves support for the following properties:

  • Temporal isolation: seL4 allows systems to be built that guarantee complete spatial isolation, however temporal isolation — that timing faults in one task should not lead to timing faults in another — is more complicated to ensure as time, unlike memory, is not fungible or renewable. We are extending the scheduling model to include reservations that, if schedulable, represent an upper-bound on task execution, thus providing temporal isolation.
  • Asymmetric Protection: Mixed-criticality systems require more than temporal isolation, since tasks of very high criticality may have conservative WCET estimates (produced by external certification authorities) which are unlikely to be used. Consequently, the ability to overcommit the processor, allowing low criticality tasks to run in the unused processing time of higher criticality tasks, is useful. In such a system, high criticality tasks are always guaranteed their full WCET, should they need it, however this protection is asymmetric: no such property holds for low criticality tasks.
  • Temporal capabilities: We are also investigating how seL4's capability-based resource-management model can be extended to cover time as a resource, by introducing capabilities for temporal reservations.
  • Cross-criticality resource sharing: Components of different criticalities should be able to safely share resources over IPC.

  This work is a collaboration with the Real-Time and Embedded Systems group at the Max Planck Institute for Software Systems. See our joint technical report.

• Worst-case execution-time analysis tools: Based on the Chronos WCET analyzer from NUS, we have 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.

• Safety-critical systems: The isolation guarantees provided by seL4 are useful in the context of safety-critical systems as well as secure systems. We are exploring the benefit that verified isolation properties can bring to the design, development, and analysis of safety-critical systems.

  As a first step, we are developing an seL4-based version of the AUTOSAR componentised automotive software platform that will provide strong isolation between application and system components.

• Previous research: NICTA's Potoroo project investigated the real-time properties of L4 kernels. Our current work builds upon this, but with fresh ideas, new approaches and the verified foundation of seL4.

• Contact: Gernot Heiser, gernot<at>nicta.com.au

Downloads

Click here to download our tools used for computing the worst-case execution time of seL4 from here.

People

Publications

		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 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