Trustworthy Systems

Academic Staff

Scott Buckley Scott Buckley  Research Associate

Scott is a postdoctoral fellow, working on verifying time protection: modeling microarchitectural state behaviour and proving that seL4's time protection mechanisms prevent leaks through time-based microarchitectural side channels. Prior to this work Scott completed his PhD in programming languages and formal methods at Macquarie University, Sydney.


Aidan Williams  Research Scientist

Mr Aidan Williams was a principal research engineer, focussing his efforts on the Digital Audio Networking project. His active research interests include digital audio networking, and new L2/L3 bridging protocols (rbridge). Other research interests include home networking, IPv6, zeroconf protocols, computer and network security, cryptographic techniques, intrusion detection, computer architecture, and operating systems.

He is now CEO for Audinate.

Felix Rauch  Research Scientist

Dr Rauch Valenti's research interests include operating systems, distributed storage systems and parallel and distributed systems like clusters of PCs. His focus is on the performance and efficiency of these systems. He now works at Google.

Sergio Ruocco  Research Scientist

Dr Ruocco's research interests include the analysis, design, and implementation of object-oriented software architectures of concurrent, distributed, time-sensitive systems (including hard real-time and Quality of Service-aware systems). He is also interested in researching novel approaches to low-level, embedded system software development. He is now a researcher at Astar in Singapore.

Simon Winwood  Researcher

Simon is interested in software correctness, in particular formally verified systems and language based security. He worked on the l4.verified project. He is now at Galois.

Toby Murray Toby Murray  Senior Researcher; Lecturer, University of Melbourne

Toby's research interests broadly concern the application of formal methods to enable the cost-effective development of secure software and systems. He is now an Associate Professor at the University of Melbourne.

Yao Shi Yao Shi  Researcher; Conjoint Lecturer, UNSW

Yao is interested in operating system analysis, compiler optimizations, concurrent program analysis and software reliability. He was a developer of Open64 compiler and has rich experience on the internals of mainstream compilers. He now works at Nvidia.

Engineers and Research Assistants

Andi Cheng Andi Cheng  Research Assistant

Andi's main interests lie in operating systems and embedded systems, and their use in small satellite systems.

Andy Bui Andy Bui  Research Assistant

Andy is working on improving the device driver framework.

Chi Kam Chi Kam  Research Assistant

Felix's research interests include operating system design, embedded systems in general and formal methods, particularly interactive theorem proving.

Curtis Millar Curtis Millar  OS Engineer; Casual Academic

Curtis is interested in improving systems level security through advancements in platform architecture, tooling, and education. Curtis now works at Apple.

Damon Lee Damon Lee  OS Engineer

Damon is interested in operating systems, hardware, and the relationships between the two. Damon now works at Kry10.

Dan Padilha Dan Padilha  Research Assistant

Dan is a research engineer in the Power Management group. He is interested in operating system design and hardware development, and has dabbled lightly in Linux kernel hacking. He is also interested in website development.

Hesham Almatary  OS Engineer

Hesham left the TS group in 2018 to go to Cambridge University for further study. His work while here, and before joining the group, was mostly around the RISC-V port of seL4.

Kent Mcleod Kent Mcleod  Research Engineer

Kent worked on many low-level systems projects, including rump kernels on seL4. He now works at Kry10.

Matthew Brecknell Matthew Brecknell  Proof Engineer

Matthew is interested in formal verification of software, using mechanised theorem provers. His current challenge is figuring out how to rapidly, yet sustainably evolve large bodies of existing proofs to meet new requirements. He now works at Kry10.

Matthew Rossouw Matthew Rossouw  OS Engineer

Matt is working on various sDDF drivers, user-space networking and network performance analysis

Michael McInerney  Senior Proof Engineer

Michael was working on verifying functional correctness for the MCS version of seL4. He is now at Proofcraft.

Remy Seassau Remy Seassau  Research Assistant

Remy is working with Johannes on a compiler for pancake.

Ryan Barry Ryan Barry  Proof Engineer

Ryan was a software engineer who specialises in interactive theorem proving and concurrency theory. He is currently working on security proofs for the RISC-V architecture as part of the Time Protection project. He is now a PhD student at ANU.

Shanush Prema Thasarathan Shanush Prema Thasarathan  Intern; Undergraduate @ UNSW - BE ME Electrical Engineering

Siwei Zhuang Siwei Zhuang  Senior OS Engineer

Siwei works on low-level systems including operating system internals, device drivers, and embedded systems architecture.

Steve Xie Steve Xie  Research Assistant


Xin Gao Xin Gao  Research Engineer

symbolic computation and fourier analysis. Xin now works at Huawei.

Yutaka Nagashima  Research Assistant

Yutaka's research interests include proof assistants and proof automation.

Student Interns

Thomas Liang Thomas Liang  Student Intern
Supervised by Johannes Åman Pohjola

Thomas is learning about interactive theorem proving and working on automating verification of Pancake programs.


Aaron Carroll Aaron Carroll  PhD Student
Supervised by Gernot Heiser

Aaron works on smartphone energy management, and is primarily interested in how multi-core applications processors can be used to reduce energy consumption when combined with well-established techniques such as frequency/voltage scaling. He also works on understanding how energy is consumed within smartphones, using physical instrumentation and measurement on real-world devices. Recently, Aaron has been exploring techniques which exploit multi-core CPUs to improve sequential performance.

Adam Christopher Walker Adam Christopher Walker  PhD Student
Supervised by Leonid Ryzhyk

Adam is interested in using formal techniques to synthesize device drivers from existing device specifications. This approach will dramatically reduce the number of operating system faults caused by drivers as well as driver development time.

Andrew Baumann  PhD Student
Supervised by Gernot Heiser

Andrew's research interests included dynamic update and hot-swapping, and component- and microkernel-based operating systems. His primary focus was the development and application of dynamic update techniques to operating systems. After completing his PhD, Andrew held a post-doctoral position at ETH Zurich. He was for many years a researcher at Microsoft Research, and is now at Google.

Andrew Boyton Andrew Boyton  PhD Student
Supervised by Gerwin Klein

Andrew is interested in proving computer programs to work the way that they should. Currently he is proving initialisation code that sets up the user level programs that run on seL4.

Anna Lyons Anna Lyons  PhD Student
Supervised by Gernot Heiser

Anna was a senior engineer on the seL4 team, taking the role after completing her PhD on the mixed-criticality API and design for seL4. Anna is dedicated to bringing seL4 to the world, by building a strong team of engineers who together build a great platform and community. Anna left Trustworthy Systems in June 2019 to join Ghost Locomotion, and is now at Apple.

Bernard Blackham Bernard Blackham  PhD Student
Supervised by Gernot Heiser

Bernard's research interests include worst-case execution time analysis, operating system design, process checkpointing, and generally messing with executables. He now works at Nvidia.

Cameron Bourke Cameron Bourke  Honours Thesis Student
Supervised by Gernot Heiser

Cameron works on providing profiling support to seL4

Charles Lewis Charles Lewis  Student Intern
Supervised by Johannes Åman Pohjola

Charles is working on memory safety for Pancake.

Daniel Potts  PhD Student
Supervised by Gernot Heiser

Distributed systems, mircokernels, embedded control systems. Dan held senior positions at Open Kernel Labs, General Dynamics and Nothrop Grunman and now works at Ghost Locomotion.

David C. Snowdon  PhD Student; UNSW
Supervised by Gernot Heiser

Dr Snowdon's research interests include embedded system design and operating system directed power management. His undergraduate thesis involved the design of a telemetry and control system for the UNSW solar powered car, Sunswift. He co-founded Metamako which was acquired by Arista Networks.

David Cock David Cock  PhD Student
Supervised by Gernot Heiser

David's research area was metrics and countermeasures for side-channel leaks in componentized secure systems. He is now a researcher at ETH Zurich.

My previous research areas include: High-performance architectural simulation, Domain-specific languages, Theorem Prover performance and automation, Kernel development, Verified software

I am currently a Post-Doc at ETH Zurich.

David Greenaway David Greenaway  PhD Student
Supervised by June Andronick

David was researching how formal verification of low-level C code can be simplified, using automatic specification abstraction in Isabelle/HOL. He now works at Google.

David Pollack David Pollack  Honours Thesis Student
Supervised by Gernot Heiser

David's research interests include operating systems and networks, particularly when they involve graphics or web technologies.

Dhammika Elkaduwe  PhD Student
Supervised by Kevin Elphinstone

Mr Eldakuwe was a PhD student in NICTA's Embedded, Real-Time, and Operating Systems program. He is interested in the development of secure embedded kernels.

Etienne Le Sueur Etienne Le Sueur  Masters Student
Supervised by Gernot Heiser

Etienne is interested in computer power management, energy efficiency and processor architecture. He recently completed his Masters of Computer Science in which he provides an analysis of the effectiveness of energy management mechanisms on computer processors.

Harvey Tuch  PhD Student
Supervised by Gerwin Klein

As a PhD student, Harvey worked on the application of formal verification techniques such as interactive theorem proving to systems software, in particular the L4 microkernel in the context of the L4.verified project. Other research interests include computer architecture, embedded systems and security.

Leonid Ryzhyk Leonid Ryzhyk  PhD Student
Supervised by Gernot Heiser

Leonid's research interests are centred around the use of formal techniques for building better operating systems. He now works at VMware Research.

Lucy Parker Lucy Parker  Honours Thesis Student
Supervised by Gernot Heiser

Lucy is worked on the Device Driver Framework, to optimise device drivers running on seL4.

Luke Macpherson  PhD Student
Supervised by Gernot Heiser

Overloaded systems & Admission control Network protocol stacks Device drivers

Matthew Chapman  PhD Student
Supervised by Gernot Heiser

Matt's research interests include computer architectures, embedded systems, operating systems and virtual machines. His thesis involved developing a virtual machine monitor for the Itanium architecture, with a number of novel features. He co-founded Exablaze, which was acquired by CISCO. He is now at d-Matrix.

Michael von Tessin Michael von Tessin  PhD Student
Supervised by Kevin Elphinstone

Michael is interested in operating systems (microkernels, multiprocessing, virtualisation, device drivers, networking, distributed systems), security (trusted computing, cryptography, security protocols) and formal verification (theorem proving, concurrency).

Nicholas Psomas Nicholas Psomas  Honours Thesis Student
Supervised by Unknown

My interests are wide, and I always like learning something new. I have specifically focused on areas such as operating systems, security and graphics/cv.

Patrick Hao Patrick Hao  Honours Thesis Student
Supervised by Gernot Heiser

Patrick is working on applying seL4 to the automotive space.

Sam Doak Sam Doak  Student Intern
Supervised by Gernot Heiser

Sam is working on seL4 stufff

Vincent Jackson Vincent Jackson  PhD Student; UNSW
Supervised by Christine Rizkallah

Vincent is interested in program verification, higher-order logic, and type theory. He is now a PhD student at the University of Melbourne

Zhi Yuan Qi Zhi Yuan Qi  Student Intern
Supervised by Johannes Åman Pohjola

Zhi is working on adding extensible disjunctive types in higher order logic in proof assistants like Isabelle/HOL.

Zilin Chen Zilin Chen  PhD Student; UNSW
Supervised by Gernot Heiser

Zilin's research is into functional programming, type theory, formal verification, compilers, and Embedded DSLs.


Ihor Kuz Ihor Kuz  Adjunct Associate Professor; Engineer at Kry10

Ihor worked at TS from 2003 until 2021. During that time he led the systems team and many of the projects TS was involved with. He now works as an Engineer at Kry10.

Ihor's research interests include operating systems and distributed systems. In particular the design of flexible and modular operating systems, security and safety properties of such systems, distributed system middleware, and management of distributed resources.

Joseph Tuong Joseph Tuong  Student

Formal methods, high-assurance systems and programming language theory & design.

Peter Gammie Peter Gammie  Visiting Researcher

Formal verification

Timothy Bourke Timothy Bourke  Visiting Researcher

Timothy is interested in the formal modelling and verification of embedded systems; particularly issues of programming language design and semantics for reactive and timing behaviours.


Matthew Warton 

My primary research interests are the performance and memory footprint of micro-kernels and micro-kernel based systems.

Philip O'Sullivan 

Philip's main research interest is in reliability and security of embedded operating systems.

Tom Birch 

Virtualisation Microkernels Performance of Virtualised Guests