Trustworthy Systems
About TS
About TS
Achievements
People
Partners and Sponsors
Diversity
Contact us
News
Research
Research
Operating systems
Formal methods
Programming languages
All projects
Publications
Software
Collaboration
Collaboration
Services
Our projects
Jobs
Jobs
Diversity
Students
Students
General Information
Courses We Run
PhD Research
Undergraduate Thesis Topics
Taste of Research Projects
Partners
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