Trustworthy Systems

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.

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

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

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.

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.

Thomas is interested in software verification, programming languages and operating systems. He has contributed extensively to major software verification projects such as the seL4 verified microkernel and the CakeML verified compiler.

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.

Ivan is working on the seL4 Microkit, seL4 Device Driver Framework, virtualisation on seL4, and LionsOS. Most of his time is spent mentoring and helping others in the team towards building a functional and usable LionsOS.

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

Adam is interested in formal verification and programming language theory. Adam is working on verifying components of the Pancake ecosystem.

Bill is involved in low-level work for the sDDF and LionsOS.

Cheng is working on adding persistence to seL4 components. This involves implementing filesystems and block device drivers on top of LionsOS.

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

Julia is working on implementing time protection on top of seL4.

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

Liam is working on formalising device controllers and verifying their drivers against that interface.

Simon is investigating worst case execution time for seL4 on RISC-V and learning about verification.

Terry is doing low-level sDDF and LionsOS work, and is currently looking at clock initialisation on a variety of platforms.

Tiana is working on Pancake

Dao has a special interest in programming languages, logic and software verification. He is currently working on the decompilation-into-logic framework for Pancake and coinductive proofs.

Guangtao is working on secure, high-performance microservices on seL4

Junming is interested in memory management and formal methods. She is currently working on verifiying a Pancake ethernet driver using SMT solvers.

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

Kurt is working on verification of sDDF components under weak memory models. He is interested in parallel computing, system semantics and formal verification.

Minh is currently working on new verified compiler optimizations for the Pancake programming language.

Szymon is interested in memory management, secure operating systems.

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

Chirag is working on a secure file system for SDcard storage.

Halogen is interested in compilers, programming languages and low level programming. They are working on improving usability and safety for Pancake.

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.

James is interested in operating systems. He is also interested in FPGA research.

Joong Do (JD) is a thesis student working on designing and developing an ARINC 653-compliant userspace scheduler on seL4 MCS using the Microkit.

He is interested in low-level systems development and software verification, and their intersection.

Lesley works on sDDF/LionsOS drivers, and various networking, hardware and FPGA projects. Currently responsible for the sDDF/LionsOS I2C protocol, drivers/hardware for the device interface formalism project, and various odd jobs around the hardware lab. Lesley's honours thesis is on studying driver dataflow dynamics in the sDDF.

Michael is a 4th year Advanced Computer Science student interested in Operating Systems development. He is currently working on two projects: creating a Linux library with the goal of emulating the seL4 Microkit, and a core management tool for multi-core systems within LionsOS.

Richard is working on evaluating programming languages for verified LionsOS components.

Sai is working on verifying time protection enforcement on the seL4 microkernel. In particular, he is validating addresses touched in said enforcement are within partitions allocated to a given context.

Thomas is a fourth-year student working on the verification of the seL4 microkernel. His honours thesis is part of the Time Protection project, one part of the proof that seL4 is free of microarchitectural timing channels.

Varun is working on adding time protected shared memory and notifications into seL4

Anton is working on the specification of an sDDF driver interface and implementation.

Ethan is working on implementing choice trees in HOL4.

Freya is working on a research internship to establish multikernel support in the Microkit based on Kent McLeod's multikernel seL4.

George is working on formalizing device controllers

Mingyuan is working on writing an IDL compiler for a general-purpose OS written with the seL4 microkernel.

Formal Verifications

Tasfia is implementing and evaluating dynamic features for the sel4 microkit.

Working on Pancake

Tristan is looking into adding new device classes to the seL4 Device Driver Framework.

Udit is working on dynamic features in sDDF

Yifei is attempting to improve the performance of the LionsOS Virtual Machine monitor

Alex manages Trustworthy Systems infrastructure. He also assists researchers whenever they may have questions about Linux, networking, device drivers, bootloaders, or anything else.

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

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

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

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 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 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, a non-standard analyst by training, working on the correctness proof seL4-based OS code.