Skip to main content

Quick links: Research Group Leader, Research and Engineering Leaders, Researchers, Engineers, Research Students, Coursework Students, Support

Research Group Leader

June Andronick June Andronick Principal Researcher; Conjoint Associate Professor, UNSW

June leads the Trustworthy Systems research group. 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.

Research and Engineering Leaders

Gernot Heiser Gernot Heiser Chief Research Scientist; Scientia Professor and John Lions Chair, UNSW

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.

Gerwin Klein Gerwin Klein Chief Research Scientist; Conjoint Professor, UNSW

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 Principal Research Engineer; Conjoint Associate Professor, UNSW

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.

Kevin Elphinstone Kevin Elphinstone Principal Researcher; Associate Professor, UNSW

Small operating system kernels 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.

Michael Norrish Michael Norrish Principal Researcher; Principal Research Scientist, 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 Hoefner Peter Hoefner Principal Research Scientist; Conjoint Associate Professor, UNSW

Peter's research interests are Formal Methods, more specifically he is interested in methods for describing software systems, in particular distributed and concurrent systems such as routing protocols or hybrid systems. For analysing and verifying these techniques he uses algebraic techniques such as process algebra and semirings. Moreover he uses off-the-shelf verification tools (automated theorem provers, model checkers) to automate the developed approaches.

Rafal Kolanski Rafal Kolanski Proof Engineer

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.

Researchers

Carroll Morgan Carroll Morgan Senior Principal Researcher; Professor, UNSW

Formal methods; semantics; security; program correctness; probability.

Christine Rizkallah Christine Rizkallah Researcher; Lecturer, UNSW

Higher-Order Logic - Interactive Theorem Proving - Formal Verification

Johannes Åman Pohjola Johannes Åman Pohjola Research Scientist; Conjoint Lecturer, UNSW

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 Chief Research Scientist; Conjoint Professor, UNSW

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.

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.

Tony Hosking Tony Hosking Contributed Researcher; Professor, ANU

Tony's research includes language runtime systems, memory management (garbage collection), and transactional memory.

Yuval Yarom Researcher; Senior Lecturer, UofA

Yuval's main research interests are computer security and cryptography, with a current focus on microarchitectural attacks and defences.

Engineers

Alison Felizzi OS Engineer

Alison works on the seL4 operating system and infrastructure.

Amirreza Zarrabi Amirreza Zarrabi Proof Engineer

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.

Branden Robinson Branden Robinson OS Engineer

Branden is interested in all kinds of software development, and hopes to learn about verification and proof techniques as part of his work in the group.

Callum Bannister Callum Bannister Proof Engineer; UNSW

Callum's research interests are in functional programming and formal verification. His current work is in separation logic.

Corey Lewis Senior Research Engineer

Corey is a senior proof engineer within the Trustworthy Systems group, and is currently the lead engineer for verifying multi-core seL4. His research interests include formal methods, functional programming and program verification. He has also been interested in mathematically analysing graph models of large real world networks.

Curtis Millar Curtis Millar OS Engineer; Casual Academic, UNSW

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.

Ed Pierzchalski Ed Pierzchalski Proof Engineer

Ed is a proof engineer working on extending the seL4 proof to more architectures.

James Ye OS Engineer

James is interested in OS design and implementation.

Jasper Lowell OS Engineer

Jasper is interested in protecting critical infastructure systems. His current work involves redesigning seL4's untrusted boot code so that it can deliver higher levels of assurance and sets a firm foundation for future formal verification work.

Kent Mcleod Kent Mcleod Research Engineer

Kent is mostly concerned with low-level operating systems and drivers.

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 Proof Engineer

Michael is learning the techniques to become a proof engineer.

Miki Tanaka Miki Tanaka Senior Research Engineer

Miki is mainly interested in formal verification techniques and their application to software systems.

Mitchell Buckley Mitchell Buckley Proof Engineer

Mitchell has a formal education in mathematics and a research background in category theory, Hopf algebra and formalised mathematics. He now writes proofs that verify functional correctness of the seL4 micro-kernel.

Qian Ge Qian Ge OS Engineer; UNSW

Qian has just finished a PhD on eliminating timing side channels from seL4 with lightweight countermeasures.

Siwei Zhuang Siwei Zhuang Research Engineer

Operating System internals, Device drivers and Embedded System Architecture.

Sylvain Gauthier OS Engineer

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

Victor Phan Proof Engineer

Formal verification.

Vincent Jackson Vincent Jackson Proof Engineer; Graduate Verification Engineer, UNSW

Vincent is interested in proof theory, type theory, and theorem proving.

Yanyan Shen Yanyan Shen Research Engineer

Yanyan is currently researching how to improve the trustworthiness of commodity hardware through software to enable the verified microkernel to be used in situations previously needing an air gap. Multi-core processors are used to provide redundancy and cross-core checking is employed to detect divergence caused by hardware faults. The aim is to increase the trustworthiness of a virtual air gap created by the microkernel, and thus systems running on COTS hardware.

Yu Hou OS Engineer

Yu is mainly interested in low level stuff such as operating systems and compilers.

Zilin Chen Zilin Chen Research Engineer; UNSW

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

Research Students

Robert Sison Robert Sison PhD Student; UNSW Sydney
Supervised by Michael Norrish

Robert is broadly interested in discovering how one may design and construct software systems with formally proved information-flow security properties at scale. The research focus of his PhD is to determine the requirements for verifying formally that a compiler doesn't break the information-flow security properties of the programs it's compiling – even when those programs use concurrency, and reuse system resources to process information of differing classification levels at different times.

Coursework Students

Emmet Murray Emmet Murray Research Assistant; UNSW
Supervised by Michael Norrish

Interested in formal verification, programming language research

Support

Birgit Brecknell Birgit Brecknell Coordinator

Birgit works part time with the TS group to cut red tape and act as a single point of contact for administrative processes.

Luke Mondy Luke Mondy System Administrator/Computer Systems Support Officer; PhD Student, USyd

Luke is a systems administrator and research support tech for the Trustworthy Systems group.

He is also currently completing a PhD in computational geodynamics.

Peter Chubb Peter Chubb Principal Research Engineer; Conjoint Senior Lecturer, UNSW

Peter's research interests include operating system algorithms for scalability, especially storage, scheduling, memory management, and locking. He is also interested in capacity planning, systems performance measurement and optimisation. His main expertise is in Unix and Linux kernels, and low level system support built on these. He contributes to low-level open-source systems tools like QEMU and U-Boot as needed for TS projects, and maintains the Trustworthy Systems website.

Served by Apache on Linux on seL4.