Key umbrella projects
- LionsOS — Secure, fast, adaptable
- The seL4 Microkernel — World's highest-assured operating system kernel
All current projects and research activities
In alphabetical order.
- Device Drivers — secure, high-performance device drivers for seL4
- Device formalisation — Formalisation of device interfaces
- Djawula — Making OS security real – finally!
- INSPECTA — Industrial Scale Proof Engineering for Critical Trustworthy Applications
- LionsOS — Secure, fast, adaptable
- Carrels — Secure Containerization for High-Assurance Microservices
- Microkit — a lean, fast, easy to use OS framework for seL4
- Microkit Verification — push-button verification of real-world OS code
- Pancake — A language for formally verified device drivers
- CakeML — Provably correct compilation of a functional language
- Pancake transpiler — Verification via Pancake-to-Viper transpiler
- PISTIs-V — Protected Integrity and Security of Transmissions Integrating seL4 and RISC-V
- Compositional Proof Methods — for system-wide safety and security properties
- Kernel-Userland Integration — connecting user-level proofs to the seL4 spec
- The seL4 Microkernel — World's highest-assured operating system kernel
- Real-Time Analysis — Guaranteeing real-time safety on seL4
- Time Protection — Principled prevention of unauthorised information flow through the timing of events
Our past projects
- AutoCorres — Simplify formal verification of low-level C code
- CAmkES — Component Architecture for microkernel-based Embedded Systems
- CASE — Cyber Assured Systems Engineering
- CDDC — Cross Domain Desktop Compositor
- Clustered Multikernel — modelling and verification of an early version of the multiprocessor seL4 kernel
- Cogent — Code and proof co-generation from high-level specifications
- Device and Driver Co-Validation — validated device drivers from device design workflow
- Dingo — untangling the interface between device drivers and the OS
- e4meter — Student-developed power meter
- eChronos — A formally verified high-assurance RTOS for microcontrollers
- Eisbach — High Level Proof Methods for Isabelle
- Energy Management — Operating-system mechanisms and techniques for managing energy and power in embedded systems
- Gelato — Linux on Itanium
- Information Flow — Reasoning about information flow and seL4
- L4 microkernels — Microkernels before seL4
- Laot — man-in-the-middle defence for critical infrastructure
- Mixed-Criticality Real-time Systems — Real-time scheduling for seL4
- Multicore seL4 Verification — Towards verifying a big-lock seL4 kernel
- Mungi — Single-address-space OS for 64-bit architectures
- Proof Engineering — Engineering large-scale proofs
- Proof Measurement and Estimation — How long will it take and what will it cost?
- Proving Compilation Correctness — Verification of the seL4 binary
- QB50 satellite payload — UNSW/NICTA CubeSat project
- seL4 on RISC-V — verified seL4 on RISC-V processors
- SMACCM — Air Team of the DARPA HACMS Program
- System Initialisation — Proof of correct system setup after boot
- Termite — Automatic synthesis of device drivers
- The seL4 Verification — Verifying the world's highest-assured operating system
- TLB Formalisation — Reasoning under Cached Address Translations
- Trustworthy COTS — Dependable systems on unreliable hardware
- ULDD — Userlevel Device Drivers for L4 and Linux
- Virtualisation — using seL4 as a hypervisor
- WCET Analysis — Proving worst-case execution-times for seL4