The seL4 Microkit is a new, lean and simple OS environment built on the seL4 microkernel aimed at embedded and cyberphysical systems. Originally fully static, dynamic features were recently proposed and prototyped. This project is to evaluate these features in terms of performance and usability, e.g. in terms of enabling on-the-fly software upgrades and late application loading.

School

Computer Science and Engineering

Research Area

Operating 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. Sample code demonstrating the use of the Microkit dynamic features for realistic uses;
  2. Written report of a critical assessment of usability and performance of the Microkit.
Senior  Systems Consultant Peter Chubb
Senior Systems Consultant
Empty profile image
Snr Operating Systems Engineer