The University of New South Wales

Quick links: Alumni Research Group Leader, Research and Engineering Leaders, Researchers, Engineers and Research Assistants, Research Students, Support, Affiliates

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.

Research and Engineering Leaders

Carroll Morgan Carroll Morgan  Professor

Carrolls research is on formal methods, semantics, security, program correctness and probability.

Christine Rizkallah Christine Rizkallah  Lecturer

Christine is interested in Higher-Order Logic, - Interactive Theorem Proving, and Formal Verification. She works primarily on the Cogent project.

Corey Lewis Corey Lewis  OS 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.

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.

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 currently is the technical lead of the verification of the seL4 MCS extensions.

Researchers

Ambroise Lafont Ambroise Lafont  Research Associate

Ambroise is working on the Cogent project.

Craig McLaughlin Craig McLaughlin  Research Associate

Craig's research interests include type theory, logic, programming languages, compilers, and formal verification.

Johannes ├ůman Pohjola Johannes ├ůman Pohjola  Lecturer

Johannes is interested in beauty and truth. Specifically, he works on interactive theorem proving, program verification and concurrency theory.

Rob van Glabbeek Rob van Glabbeek  Conjoint Professor; Chief Research Scientist, CSIRO's Data61

Rob strives to create and study comprehensive models and theories of concurrent processes, thereby answering fundamental questions such as: which problems can be solved in a distributed way, using only asynchronous communication, and which cannot. These insights are applied to the modelling, verification and analysis of distributed systems, in particular to popular routing protocols in wireless mesh networks.

Scott Buckley Scott Buckley  Research Associate

Scott works in the time protection team.

Engineers and Research Assistants

Curtis Millar Curtis Millar  OS Engineer; Casual Academic

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

Jashank Jeremy Jashank Jeremy  Research Assistant

Jashank is interested in programming languages as expressive aids for developing correct software; and in operating systems as fundamental infrastructure for developing robust and portable systems.

Jingyao Zhou Jingyao Zhou  OS Engineer

Jingyao is interested in real-time operating systems and hardware.

Michael McInerney  Senior Proof Engineer

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

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.

Siwei Zhuang Siwei Zhuang  Senior OS Engineer

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

Sylvain Gauthier  OS Engineer

Sylvain is interested in working on and understanding UNIX systems and operating systems Kernels.

Zoltan Kocsis Zoltan Kocsis  Senior Proof Engineer

Zoltan, a non-standard analyst by training, works on the correctness proof for the seL4 kernel.

Research Students

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

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

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.

Support

Birgit Brecknell Birgit Brecknell  Project Manager

Birgit works part time with the TS group as project manager for strategic and external projects

Peter Chubb Peter Chubb  Senior Systems Consultant; Conjoint Senior Lecturer

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.

Affiliates

Gerwin Klein Gerwin Klein  Conjoint 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 Ihor Kuz  Conjoint Associate Professor; Engineer at Kry10

Ihor's research interests include operating systems and distributed systems. With regards to operating systems, he focuses on the design of flexible and modular operating systems, as well as security and safety properties of such systems. In distributed systems, he is interested in distributed system middleware, supporting services, and management of distributed resources.

He left the Trustworthy Systems group to work for Kry10 in July 2021.

June Andronick June Andronick  Conjoint 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 Rafal Kolanski  Conjoint 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 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. His current research concerns the formal verification of operating systems to enforce increasingly useful forms of information-flow security, also known as confidentiality.