Trustworthy Systems

Key umbrella projects

• External collaborations
• seL4-based software stack — Security is no excuse for bad performance!
• The seL4 Microkernel — World's highest-assured operating system
• Time Protection — Principled prevention of unauthorised information flow through the timing of events

All current projects and research activities

In alphabetical order.

• CakeML — Provably correct compilation of a functional language
• Device Drivers — secure, high-performance device drivers for seL4
  • Device_virtualisation — Device virtualisation for seL4
• External collaborations
  • Makatea — Qubes-like OS on seL4
• Pancake — A language for formally verified device drivers
• Secure OS — Making OS security real – finally!
• seL4-based software stack — Security is no excuse for bad performance!
• seL4CP — The seL4 Core Platform – lean, fast, easy to use OS
• seL4CP Verification — Verifying an seL4-based OS
• The seL4 Microkernel — World's highest-assured operating system
  • Time Protection — Principled prevention of unauthorised information flow through the timing of events
  • Virtualisation — using seL4 as a hypervisor

Our past projects

• Analysis of Protocols for High-assurance Networks
• CAmkES — Component Architecture for microkernel-based Embedded Systems
• CASE — Cyber Assured Systems Engineering
• CDDC — Cross Domain Desktop Compositor
• Cogent — Code and proof co-generation from high-level specifications
• Concurrency and Protocol Verification
• Device and Driver Co-Validation — validated device drivers from device design workflow
• Dingo — untangling the interface between device drivers and the OS
• e4meter
• eChronos — A formally verified high-assurance RTOS for microcontrollers
• Energy Management — Operating-system mechanisms and techniques for managing energy and power in embedded systems
• Laot — man-in-the-middle defence for critical infrastructure
• Mixed-Criticality Real-time Systems — Real-time scheduling for seL4
• Probability and Nondeterminism
• Process Algebra
• RISC-V — verified seL4 on RISC-V processors
• SMACCM — High-assurance UAV built on seL4 and eChronos
• Termite — Automatic synthesis of device drivers
• The seL4 Verification — Verifying the world's highest-assured operating system
  • Eisbach — High Level Proof Methods for Isabelle
  • Information Flow — Reasoning about information flow and seL4
  • Multicore seL4 Verification
  • Proof Engineering — Engineering large-scale proofs
  • Proving Compilation Correctness — Binary verification of seL4
  • System Initialisation — Proof of correct system setup after boot
  • TLB Formalisation — Reasoning under Cached Address Translations
• Trustworthy Components — Component platform (CAmkES) and approaches to developing formally verified software components running on seL4
• Trustworthy COTS — Dependable systems on unreliable hardware
• Trustworthy Systems — past projects from the NICTA Trustworthy Systems research group
  • AutoCorres — Simplify formal verification of low-level C code
  • Automated Reasoning — better and faster general proof tools for software verification
  • Clustered Multikernel — modelling and verification of an early version of the multiprocessor seL4 kernel
  • Proof Measurement and Estimation — How long will it take and what will it cost?
  • QB50 satellite payload — UNSW/NICTA CubeSat project
  • Security Architecture — System architectures that enforce security properties
  • Verification-Enhanced Compiler Optimisation — optimising code based on manually proven properties
  • Whole-System Assurance — Putting everything together
• ULDD — Userlevel Device Drivers
• WCET Analysis — Proving worst-case execution-times for seL4