Funding Our Partners

Guaranteeing timeliness of MCS on seL4

Aim

A framework for guaranteeing deadlines in mixed-criticality systems built on seL4.

Overview

seL4, owing to its formally proved correctness and isolation guarantees, is the strongest foundation for building critical systems. For a mixed-criticality real-time system (MCS), spatial isolation (memory safety) needs to be complemented by temporal isolation (timing safety).

In previous research we have laid the foundation for temporal safety guarantees in seL4:

1. We performed a sound, complete and high-assurance worst-case execution time (WCET) analysis of seL4, to our knowledge the first ever such analysis for a protected-mode real-time operating system.
2. We developed a scheduling model with capability-authorised access to processor time, resulting in the new MCS version of seL4 that is currently undergoing formal verification.

We now aim to develop these building blocks into a general framework for reasoning about timeliness in seL4-based MCS. This consists of several steps:

1. re-establish WCET for the latest MCS seL4 kernel for the RISC-V architecture;
2. extract worst-case instruction latencies from an actual RISC-V processor implementation;
3. develop a reasoning framework for guaranteeing deadlines of critical components in an MCS in the presence of preemption by untrusted components.

WCET analysis of seL4-MCS on RISC-V

General approach

The WCET analysis of the kernel must establish the worst-case latency of any kernel operation possible during the execution of the MCS. Note that thanks to seL4's capability-based access control, it is possible to restrict a system to use only a subset of kernel operations. For example, an MCS may not require creating or destroying kernel objects after initialisation (and object destruction tends to have the highest WCET of all kernel operations).

Hence it makes sense to do the WCET analysis separately for each kernel operation, to give the system designer the option of building a system with a lower WCET (e.g. by not handing user code the right to destroy objects).

WCET analysis must be sound (providing a safe upper bound) and complete (executing all possible code paths). This requires static analysis of the binary, avoiding assumptions about compiler behaviour. The analysis uses a model of the processor's microarchitecture, including instruction latencies, cache behaviour, and other timing-relevant features.

The figure shows a typical WCET analysis pipeline. A tool extracts the control-flow graph (CFG) from the binary. This is fed into an analysis tool to incorporate the microarchitectural timing information.

The analysis tool generates linear constraints describing possible execution paths, which are solved using integer linear programming to identify candidate worst-case paths and their execution times.

For loops that do not have a constant iteration count, hard bounds on iterations must be provided; these are in general impossible to extract from the information available in the program binary.

Many candidate paths are infeasible due to mutually exclusive conditions that depend on input data. These should be identified to reduce the pessimism of the analysis. As for loop bounds, such refutations are generally not possible from the information contained in the program binary.

Our prior work

Our earlier work on WCET analysis of seL4 pioneered scaling a sound analysis to the complete seL4 kernel. It furthermore used seL4's translation validation framework to inject sound loop bounds and infeasible-path refutations proved on the seL4 source code into the WCET analysis.

Unfortunately, we can no longer use the earlier work, for a number of reasons. Firstly, it was performed for (32-bit) Armv6 and Armv7 processors, for which Arm published the required instruction latencies. Arm no longer does this for its later processor generation, so the analysis could not be maintained for Arm processors.

Furthermore, the earlier work was done for the then seL4 kernel, which pre-dated the MCS kernel. That kernel was much simpler than the MCS version, meaning that significant work is required to re-establish the analysis for the more complex MCS kernel, and for 64-bit architectures.

Re-establishing seL4's WCET

The open RISC-V architecture, which has spawned open-source implementations such as the CVA6 makes it possible to obtain sound instruction latencies for WCET analysis, thus allowing us to re-establish the WCET analysis for seL4.

However, our prior work was based on a heavily modified fork of the NUS Chronos tool, which had become unmaintained by the time our work was completed. Rather than trying to revive the original toolchain (with no one around that knows its internals) we have now adopted the more modern Heptane tool.

Heptane, however, still required significant enhancements: in particular, its support for RISC-V was incomplete, and it could not model the complex access patterns and control-flow idioms characteristic of kernel code.

With some help from Prof. Isabelle Puaut, whose group created Heptane, we implemented the missing architectural support for 64-bit RISC-V and generalised the data-cache analysis to handle the arbitrary pointer-based accesses used throughout the kernel. We also added new capability to analyse complex control flows, including non-local jumps, compiler optimisations like tail and sibling calls, and termination of kernel execution via a mode switch. To make whole-kernel analysis practical, we re-engineered the fixed-point iteration algorithm used in the cache analyses, achieving substantial efficiency gains. Finally, we also resolved memory leaks, ensuring the tool could complete its analysis with reasonable speed and memory consumption while preserving soundness.

Status

Our Heptane fork can now successfully perform a complete static analysis of the entire seL4 kernel, and we are in the process of getting our changes upstreamed. While the analysis is structurally complete, the timing outputs are not yet meaningful because they rely on placeholder values for instruction latencies, cache-miss penalties, and loop bounds.

We also are still to re-establish the integration of verified loop bounds and infeasible-path refutations from the seL4 proofs.

Extracting latencies from a processor implementation

Rather than relying on simulated or otherwise guestimated instruction latencies, we are working with our partner PlanV to extract sound latencies from the Verilog implementation of the open-source RISC-V processor used in the PISTIs-V Project.

Reasoning framework for guaranteeing timeliness

Once WCET analysis is complete with correct hardware latencies and loop bounds, the next step is to build a schedulability analysis framework. The aim is to account for possible preemptions of a critical component, based on a formalisation of the system's software architecture, to establish safe deadlines.

This will enable us to achieve the stated aim of establishing end-to-end timing guarantees for MCS on seL4.

Support

This project is supported by Cyberagentur as part of the PISTIs-V Project under the Ecosystem formally verifiable IT – Provable cybersecurity (EvIT) program.

Availability

Latest News

• 2025-09-11: Our modifications to Heptane are able to process the complete MCS kernel for the RISC-V architecture and are ready for upstreaming.
• 2025-03-07: Our evaluation of existing tools indicates that Heptane is the most promising starting point for re-doing the WCET analysis of seL4, including moving to the MCS kernel and RISC-V.

People

Contact

Gernot Heiser, gernot@unsw.edu.au

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 Mixed-criticality scheduling and resource sharing for high-assurance operating systems PhD Thesis, UNSW, August, 2018
		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
		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, July, 2017
		Thomas Sewell, Felix 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