The seL4 microkernel was the first (and seemingly only) protected-mode real-time operating system kernel that underwent a complete and sound worst-case execution-time analysis (WCET analysis). This work was performed on a long obsolete Armv7 processor, using a tool chain that is also obsolete.

This project is to investigate re-doing this work for 64-bit RISC-V processors, using a state-of-the-art, open-source tool, Otawa. Specifically, it is to trial Otawa on some simple code example, and then progress to actual kernel code, starting with a subset of the seL4 kernel.

School

Computer Science and Engineering

Research Area

Operating systems | Embedded systems | Real-time systems

The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.

  1. WCET results for at least a subset of the seL4 kernel code;
  2. Report describing experience, achievements, challenges and limitations of using Otawa on real-world kernel code.
Scientia Professor and John Lions Chair Gernot Heiser
Scientia Professor and John Lions Chair