Key umbrella projects
- Concurrency and Protocol Verification
- External collaborations
- The seL4 Microkernel — World's highest-assured operating system
- The seL4 Verification — Verifying the 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
- Cogent — Code and proof co-generation from high-level specifications
- Concurrency and Protocol Verification
- Asynchronous Communication in Distributed Systems
- Formal Methods for Wireless Networks — Specification, Verification and Analysis
- Multicore seL4 Verification
- Probability and Nondeterminism
- Process Algebra
- External collaborations
- Analysis of Protocols for High-assurance Networks
- CASE — Cyber Assured Systems Engineering
- CDDC — Cross Domain Desktop Compositor
- MicroVM — A new foundation layer for managed language implementation
- The seL4 Microkernel — World's highest-assured operating system
- Mixed-Criticality Real-time Systems — Real-time scheduling for seL4
- Time Protection — Principled prevention of unauthorised information flow through the timing of events
- Virtualisation — using seL4 as a hypervisor
- The seL4 Verification — Verifying the world's highest-assured operating system
- Information Flow — Reasoning about information flow and seL4
- 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
- CAmkES — Component Architecture for microkernel-based Embedded Systems
Our past projects
- e4meter
- 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
- SMACCM — High-assurance UAV built on seL4 and eChronos
- 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
- Dingo — untangling the interface between device drivers and the OS
- Proof Measurement and Estimation — How long will it take and what will it cost%3f
- QB50 satellite payload — UNSW/NICTA CubeSat project
- Security Architecture — System architectures that enforce security properties
- Termite — Automatic synthesis of device drivers
- Verification-Enhanced Compiler Optimisation — optimising code based on manually proven properties
- Verified Garbage Collection — Verification of a concurrent real-time garbage collector under TSO
- Whole-System Assurance — Putting everything together