Trustworthy Systems

Research Group Leader

Gernot Heiser Gernot Heiser  Scientia Professor; John Lions Chair

Gernot's main research interests are in operating systems, especially microkernel-based systems, and their use in embedded/cyber-physical systems, OS security and robustness issues, general cyber-security, energy/power management, real-time systems, virtualization and architectural support for operating systems.

Academic Staff

Carroll Morgan Carroll Morgan  Professor

Carroll's research is on formal methods, semantics, security, program correctness and probability.

Craig McLaughlin Craig McLaughlin  Research Associate

Craig's research interests include type theory, logic, programming languages, compilers, and formal verification. He presently works on a formal security framework for a provably secure operating system

Johannes Åman Pohjola Johannes Åman Pohjola  Lecturer

Johannes is interested in beauty and truth. He works on interactive theorem proving, program verification and concurrency theory, specifically for the Pancake language

Kevin Elphinstone Kevin Elphinstone  Associate Professor

Kevin works on operating system microkernels and the infrastructure required to support larger systems upon them. His current focus includes secure embedded operating systems suitable for formal verification, and for being the basis of secure systems for embedded devices. He also has interests in componentised operating systems, operating systems in general, security, real-time systems, computer architecture as it pertains to operating systems, and virtualisation.

Robert Sison Robert Sison  Senior Research Associate

Rob is a postdoctoral researcher who is broadly interested in discovering how best to design and construct software systems with formally proved functional-correctness and security properties at scale.

Research and Engineering Leaders

Ivan Velickovic Ivan Velickovic  Senior OS Engineer

Ivan is working on the seL4 Microkit and device driver virtualisation on seL4.

Miki Tanaka Miki Tanaka  Senior Proof Engineer

Miki is interested in formal verification techniques and their application to software systems, and broadly proof engineering as a discipline. Miki has contributed to the verification of architecture porting for seL4 and also the verification of the seL4 MCS extensions as the technical lead. Miki is currently involved in a project for device driver verification using the Pancake language (based on cakeML/HOL4).

Peter Chubb Peter Chubb  Senior Systems Consultant

Peter's research interests include operating system abstractions for, intra alia, storage, scheduling, memory management, and locking. He is also interested in capacity planning, and in systems performance measurement and optimisation. His main expertise is in Unix and Linux kernels, and low level system support built on these. He also maintains the Trustworthy Systems website and internal infrastructure.

Engineers and Research Assistants

Alex Brown Alex Brown  Research Assistant

Alex is investigating virtIO interfaces on top of the Lions OS

Alwin Joshy Alwin Joshy  OS Engineer

Alwin is working on fast paths in seL4 and on a secure multi-server OS on seL4

Ben Nott Ben Nott  Research Assistant

Ben has deep research interests in formal methods and metamathemtics. Ben is working on Pancake language semantics and program verification.

Cheng Li Cheng Li  Research Assistant

Cheng is working on adding persistence to seL4 components.

Courtney Darville Courtney Darville  OS Engineer

Courtney works on secure multi-server operating system design, and on applying model checking to verify inter-component communication in a highly modular seL4-based OS.

Eric Chan Eric Chan  Research Assistant

Eric is working on device virtualisation for the Microkit.

Isitha Subasinghe Isitha Subasinghe  Research Assistant

Isitha's research interests include Operating Systems, Distributed Systems and Formal Verification. He presently works on verifying OS code using SMT solvers

James Archer James Archer  OS Engineer

James is working to improve the locking in multicore seL4.

Jingyao Zhou Jingyao Zhou  OS Engineer

Jingyao is interested in real-time operating systems and hardware. She presently works on device virtualisation for seL4

Junming Zhao Junming Zhao  Research Engineer

Junming is interested in memory management and formal methods. She is currently working on pancake serial driver.

Krishnan Winter Krishnan Winter  OS Engineer

Krishnan is working on OS development infrastructure, especially support for profiling.

Tiana Tsang Ung Tiana Tsang Ung  Research Assistant

Tiana is working on Pancake

Research Students

Kevin Tran Kevin Tran  PhD Student
Supervised by Johannes Åman Pohjola

Kevin's research is on creating a framework for reasoning about concurrent programs, with the ultimate goal of verifying multicore seL4.

Tran Dao Le Tran Dao Le  Masters Student
Supervised by Gernot Heiser

Dao is working on the decompilation-into-logic framework for Pancake.

Coursework Students

Anuraag Ganesh Anuraag Ganesh  Honours Thesis Student
Supervised by Gernot Heiser

Anuraag is working on Driver VMs: Re-use of unmodified Linux device drivers in seL4

Gordon Sau Gordon Sau  Honours Thesis Student
Supervised by Johannes Åman Pohjola

Gordon is working on adding support for memory-mapped IO for Pancake.

Guangtao Zhu Guangtao Zhu  Masters Student
Supervised by Gernot Heiser

GuangTao is working on optimising the multicore IPC performance for seL4 microkernel

Manmeet Dhaliwal  Masters Student
Supervised by Peter Chubb

Manmeet is working on a reference system which would demonstrate high-performance networking on seL4 using LionsOS, suitable for adapting to a variety of network-focussed use cases. Such a practical network router would then have a roadmap that proves its correctness.

Mathieu Paturel Mathieu Paturel  Honours Thesis Student
Supervised by Gernot Heiser

Mathieu is interested in formal methods, in particular bringing its cost down.

He is currently working on verifying user level components built on top of seL4 using SMT solvers.

Matthew Rossouw Matthew Rossouw  Honours Thesis Student
Supervised by Peter Chubb

Matt is working on network performance evaluation, analysis and optimisation

Michael He Michael He  Honours Thesis Student
Supervised by Gernot Heiser

Michael is working on adding PD Templates to the seL4 Microkit.

Nila Riahi Nila Riahi  Honours Thesis Student
Supervised by Gernot Heiser

Nila is working on core management in Lions OS.

Terry Bai Terry Bai  Masters Student
Supervised by Gernot Heiser

Terry is doing a master's thesis in TS.

Student Interns

Adam Stucci Adam Stucci  Student Intern
Supervised by Johannes Åman Pohjola

Adam is interested in programming language theory and is working on adding continuations to Pancake.

Bill Nguyen Bill Nguyen  Student Intern
Supervised by Peter Chubb

Bill is working on the Client programming model for Microkit.

Charran Kethees Charran Kethees  Student Intern
Supervised by Johannes Åman Pohjola

Charran is working on the development and verification of Hoare Logic over interaction trees.

Chirag Sawlani Chirag Sawlani  Student Intern
Supervised by Gernot Heiser

Chirag is working on WCET analysis using Otawa using RISC-V processors.

Damjan Stevanoski Damjan Stevanoski  Student Intern
Supervised by Peter Chubb

Damjan is working on improving VMM performance

Dominic Yeap-Holliday Dominic Yeap-Holliday  Student Intern
Supervised by Johannes Åman Pohjola

Dominic is working on compiler improvements to Pancake.

James Milosavljevic James Milosavljevic  Student Intern
Supervised by Peter Chubb

James is a 4th year undergraduate student completing a degree in computer engineering. He is currently working on a project to enable booting virtual machines off disk.

Joong Do Chiang Joong Do Chiang  Student Intern
Supervised by Johannes Åman Pohjola

Joong Do is working on developing and formally verifying a ring buffer library in Pancake. He is interested in low-level systems development and software verification, and their intersection.

Julia Broady  Student Intern
Supervised by Peter Chubb

Julia is working on adding support for hotplugging of devices to SDDF.

Ken Li Ken Li  Student Intern
Supervised by Johannes Åman Pohjola

Ken is working on evaluating Pancake by implementing device drivers on top of seL4.

Michael Maher Michael Maher  Student Intern
Supervised by Gernot Heiser

Michael is working on improving TCP performance for seL4.

Michael Mospan Michael Mospan  Student Intern
Supervised by Peter Chubb

Michael is a 3rd year Advanced Computer Science student interested in Operating Systems development. He is currently working on a project to create a Linux library with the goal of emulating the seL4 Microkit.

Ronald Chiang Ronald Chiang  Student Intern
Supervised by Johannes Åman Pohjola

Ronald is working on connecting interaction trees and state machines for Pancake device drivers.

Ryan Shi Ryan Shi  Student Intern
Supervised by Peter Chubb

Ryan is assisting in developing a native file system on the seL4 core platform.

In one line, Ryan wants to research more in the intersection of maths and CS. Ryan currently is pursuing a Pure Maths major and is exploring the areas of: - Functional Analysis - Topological Spaces - Time Series - Measure Theory

In the realm of CS, Ryan has a shallow background in Networking and Data Analysis. Ryan would like to learn more about the following areas: - Haskell / OCaml - Rust - C

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

Thomas Qu is interested in type theory and software verification.

Tristan Clinton-Muehr Tristan Clinton-Muehr  Student Intern
Supervised by Gernot Heiser

Tristan is a Taste-Of-Research scholar looking into adding new device classes to the seL4 Device Driver Framework.

Uzman Zwahir  Student Intern
Supervised by Peter Chubb

Uzman is working on adding persistence support to seL4 microkit apps. He has an interest in systems engineering, low level development, and basketball.

Xavier Cooney Xavier Cooney  Student Intern
Supervised by Gernot Heiser

Xavier is working on using SMT solvers for verification.

Xianghao Wang Xianghao Wang  Student Intern
Supervised by Peter Chubb

Xianghao is working on POSIX-style interfaces to seL4 I/O system

Students

Halogen Truong Halogen Truong  Research Assistant
Supervised by Johannes Åman Pohjola

Halogen is working on adding support for multiple entry points in the Pancake compiler stack.

Support

Christopher Irving Christopher Irving  System Administrator

Christopher is training as a system administrator to maintain the machines and infrastructure of Trustworthy Systems.

Tessa Lunney Tessa Lunney  Administrator

Tessa works part-time as the Administrative Officer, managing the office. She works Mondays, Thursdays, and Fridays.

Affiliates

Corey Lewis Corey Lewis  Visiting Fellow

Corey was a senior proof engineer and 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. Corey now works at Proofcraft.

Gerwin Klein Gerwin Klein  Adjunct Professor; Founder and Chief Scientist at Proofcraft

Gerwin's research interest is in Formal Methods, more specifically in interactive theorem proving, software verification, semantics of programming languages, and in the emerging field of proof engineering. Generally, he wants software systems to be dependable, and thinks that formal specification and proof can make a significant contribution towards that goal.

June Andronick June Andronick  Adjunct Professor; Founder and CEO at Proofcraft

June had joined the Trustworthy Systems research group in 2008 (in NICTA), and led the group from end of 2016 to end of 2020. Her main research interest is in formal verification and certification of software systems, more precisely in formal proof of correctness and security properties of programs using interactive theorem proving, as well as concurrency reasoning, targeting interruptible and multicore systems.

Michael Norrish Michael Norrish  Adjunct Associate Professor; 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. Michael now is a Associate Professor at ANU.

Rafal Kolanski Rafal Kolanski  Adjunct Lecturer; Founder at Proofcraft

Rafal worked as a proof engineer at Trustworthy Systems until April 2021. He led the Proof Engineering team from 2016 until 2021.

Rafal is interested in the formal verification of high assurance, system-level software, both from the perspective of verification in practice, but also proof maintenance and increasing the proof coverage of already verified systems.

Zoltan Kocsis Zoltan Kocsis  Adjunct Lecturer

Zoltan, a non-standard analyst by training, working on the correctness proof seL4-based OS code.