Research Group Leader
 |
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 Professor |
Carroll's research is on formal methods, semantics, security, program correctness and probability. |
|
 |
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 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 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. |
|
 |
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. |
|
Engineers and Research Assistants
 |
Ben Nott Research Assistant |
Ben has deep research interests in formal methods and metamathemtics. Ben is working on Pancake language semantics and program verification. |
|
 |
Courtney Darville Research Assistant |
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 OS Engineer |
Eric is working on the sel4 Core Platform |
|
 |
Gordon Sau Research Assistant |
Gordon is working on adding support for memory-mapped IO for Pancake. |
|
 |
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 |
|
 |
Ivan Velickovic Research Assistant |
Ivan is working on the seL4 Core Platform and device driver virtualisation on seL4. |
|
 |
James Archer OS Engineer |
James is working to improve the locking in multicore seL4. |
|
 |
Jingyao Zhou OS Engineer |
Jingyao is interested in real-time operating systems and hardware. She presently works on device virtualisation for seL4 |
|
 |
Krishnan Winter OS Engineer |
Krishnan is working on exercising the Pancake language for real device drivers |
|
 |
Mathieu Paturel Research Assistant |
Mathieu is interested in formal methods, in particular bringing its cost down. He is presently working on verifying user level components running on top of the seL4 core platform, a very thin operating operating system. |
|
 |
Matthew Rossouw OS Engineer |
Matt is working on User-space networking, sDDF, network benchmarking and performance |
|
 |
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 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. |
|
|
Research Students
 |
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. |
|
Coursework Students
 |
Alwin Joshy Honours Thesis Student |
Supervised by
Gernot Heiser
|
Alwin is working on fast paths in seL4 and on a secure multi-server OS on seL4 |
|
 |
Arthur Wang Honours Thesis Student |
Supervised by
Gernot Heiser
|
Arthur is working on IOMMU management on seL4. |
|
 |
Dan Shea Honours Thesis Student |
Supervised by
Gernot Heiser
|
Dan is working on adding an IRQ fast path to seL4. |
|
 |
Jasper Di Francesco Honours Thesis Student |
Supervised by
Gernot Heiser
|
Jasper is building a native web server for the seL4 core platform. His honours thesis is on performance limits for protected-mode real-time OSes. |
|
 |
Lucy Parker Honours Thesis Student |
Supervised by
Gernot Heiser
|
Lucy is working on the Device Driver Framework, to optimise device drivers running on seL4. |
|
 |
Patrick Hao Honours Thesis Student |
Supervised by
Gernot Heiser
|
Patrick is working on applying seL4 to the automotive space. |
|
 |
Thomas Bove Honours Thesis Student |
Supervised by
Gernot Heiser
|
Tom is working on hardware implementations of time protection. |
|
Student Interns and Visitors
|
Charran Kethees Student Intern |
Supervised by
Johannes Åman Pohjola
|
Charran is working on the development and verification of Hoare Logic for the interaction trees. |
|
 |
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 Student Intern |
Supervised by
Johannes Åman Pohjola
|
Thomas Qu is interested in type theory and software verification. |
|
 |
Waleed Shahid Student Intern |
Supervised by
Gernot Heiser
|
Waleed is analyzing and optimizing seL4's worst case cold-cache performance. |
|
Support
 |
Birgit Brecknell Project Manager |
Birgit works part time with the TS group as project manager for strategic and external projects |
|
 |
Christopher Irving Administrator |
Christopher is training as a system administrator to maintain the machines and infrastructure of Trustworthy Systems. |
|
 |
Tessa Lunney Administrator; Administrative Assistant |
Tessa works part-time as the Administrative Assistant, managing the office. She works Mondays, Wednesdays, and Fridays. |
|
Affiliates
 |
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. |
|
 |
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. |
|
 |
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. |
|
 |
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. |
|
 |
Robert Sison Visiting Fellow; Research Fellow, University of Melbourne |
Robert is broadly interested in discovering how best to design and construct software systems with formally proved functional-correctness and security properties at scale. Their current research concerns the formal verification of operating systems to enforce increasingly useful forms of information-flow security, also known as confidentiality. |
|