Trustworthy Systems

Quick links: Alumni Academic Staff, Research and Engineering Leaders, Researchers, Engineers and Research Assistants, Research Students, Coursework Students, Support, Affiliates, Alumni

Academic Staff

Aidan Williams  Administrator

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 Chief Technology Officer for Audinate.

Research and Engineering Leaders

Michael Norrish Michael Norrish  Principal Researcher; Associate Professor, ANU

Michael is interested in the use of mathematics and logic to help in the specification and development of computer hardware and software. He is interested both in working on specific applications projects in this area, and in the development of tools to make all such projects easier to work on.

Peter Baumgartner Peter Baumgartner  Principal Researcher; Adjunct Associate Professor, ANU

Advancement of automated deduction, in particular first-order logic theorem proving; applications for software verification, knowledge representation, and business rules/process analysis; exploiting connections into related areas such as logic programming, description logics and nonmonotonic reasoning.


David Greenaway David Greenaway  Researcher

David is currently researching how formal verification of low-level C code can be simplified, using automatic specification abstraction in Isabelle/HOL.

Matthias Daum Matthias Daum  Researcher

Matthias' research interest is in Formal Methods, more specifically in interactive theorem proving, software verification, and concurrency.

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.

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.

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.

Angus Finch Angus Finch  Research Assistant

Angus is learning about seL4 through the current driver initiative

Anna Lyons Anna Lyons  Senior Research Engineer

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

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.

Corey Lewis Corey Lewis  Senior Proof Engineer

Corey is a senior proof engineer within the Trustworthy Systems group and is currently the lead engineer for verifying multi-core seL4. During his time at TS he has been involved in a wide variety of projects to do with seL4. These include developing the original CapDL translation tools, helping complete the information flow proofs, and contributing to the verification of the seL4 MCS extensions. His research interests include formal methods, functional programming, and program verification.

Curtis Millar Curtis Millar  OS Engineer; Casual Academic

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

Damon Lee Damon Lee  OS Engineer

Damon is interested in operating systems, hardware, and the relationships between the two.

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.

David C. Snowdon  Research Engineer; UNSW

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.

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 left TS to work for a startup in July 2020.

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.

Michael McInerney  Senior Proof Engineer

Michael is currently working on verifying functional correctness for the MCS version of seL4.

Remy Seassau Remy Seassau  Research Assistant

Remy is working with Johannes on a compiler for pancake.

Ryan Barry Ryan Barry  Proof Engineer

Ryan is 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.

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.

Yutaka Nagashima  Research Assistant

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

Research Students

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.

Amirreza Zarrabi Amirreza Zarrabi  PhD Student; UNSW
Supervised by Amirreza Zarrabi

Amir is researching operating system architecture, and multiserver architectures for OS design. He is currently on a break from his PhD to work as a proof engineer.

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 is now researcher at Microsoft Research, Redmond.

David Cock David Cock  PhD Student
Supervised by Alwin Joshy

My current research area is metrics and countermeasures for side-channel leaks in componentized secure systems.

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.

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).

Mohammad Abdulaziz Mohammad Abdulaziz  PhD Student
Supervised by Michael Norrish

I am interested in Interactive theorem proving. My PhD project is about mechanizing optimality properties in SAT based planning algorithms.

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

Vincent is interested in program verification, higher-order logic, and type theory.

Coursework Students

Cameron Bourke Cameron Bourke  Honours Thesis Student
Supervised by Gernot Heiser

Cameron works on providing profiling support to seL4

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  UNSW Student
Supervised by Unknown

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.

Matthew Chapman 
Supervised by Unknown

Mr Chapman's research interests include computer architectures, embedded systems, operating systems and virtual machines. His thesis involves developing a virtual machine monitor for the Itanium architecture, with a number of novel features.

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.


Alex Piotrowski Alex Piotrowski  Research Assistant

Alex was training to be a system administrator in our group. He left to become part of a Cloud Computing provider.


Adam Christopher Walker Adam Christopher Walker  Visiting Student

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 Boyton Andrew Boyton  Visiting Researcher

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.

Bernard Blackham Bernard Blackham  Visiting Researcher

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

Etienne Le Sueur Etienne Le Sueur  Visiting Researcher

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.

Franck Cassez Franck Cassez  Visiting Researcher; Conjoint Associate Professor, UNSW

Franck's research interests include software verification techniques, static analysis, model-checking, SMT-solvers, as well as infinite state systems, verification and control of timed systems, timed logics or worst-case execution time.

Joseph Tuong Joseph Tuong  Student

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

Leonid Ryzhyk Leonid Ryzhyk  Researcher

Leonid's research interests are centred around the use of formal techniques for building better operating systems.

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.


Daniel Potts 

Distributed systems, mircokernels, embedded control systems.

Felix Rauch 

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.

Harvey Tuch 

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.

Luke Macpherson 

Overloaded systems & Admission control Network protocol stacks Device drivers

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.

Sergio Ruocco 

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.

Timothy Roscoe 

Mothy is broadly interested in operating systems, distributed systems, and networks. His current interests include building distributed applications using declarative queries and software dataflow, and efficient execution of software dataflow graphs directly inside virtual machines.

Tom Birch 

Virtualisation Microkernels Performance of Virtualised Guests

Varuni Witana 

Dr Varuni Witana joined NICTA as a senior researcher in February 2004. She is attached to the Embedded, Real-Time & Operating Systems (ERTOS) program and is currently working on the Digital Audio Networking project. Her active research interests include digital audio networking, precision networked clock synchronization. Other research interests include 802.11 wireless networking and multimedia communications.