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.

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.

Roger is interested in formal verification, and theoretical computer science in general. Roger currently works on the PISTIs-V project, in particular on the reasoning framework of real-time properties of seL4's scheduler.

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.

Vincent is interested in logic, program semantics, and information-flow security.

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.

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.

Daniel has been attempting to prove properties about blocking system calls.

Jakub is interested in FPGAs, device drivers, efficient system design and high-performance systems. Has deep experience in 5G/LTE in L1 (Physical layer) and interfacing custom hardware in commercial settings.

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

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

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 was on studying driver dataflow dynamics in the sDDF.

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.

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

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

Joshua is interested in performance measurement and optimisation. His thesis topic is ‘Performance Limits of a Microkernel-based System’

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 formal verification and parallel computing.

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

Szymon is interested in memory management, secure operating systems.

Alex is working on a Human Interface stack (keyboards, mice, display) for LionsOS

Alex is working on understanding and optimising virtualisation performance on seL4/LionsOS

Callum is looking into LionsOS IOMMU support.

Etkin is interested in kernels. His thesis topic is to do with adding persistence to LionsOS

Fadi is working on an ARINC 653 OS on seL4.

Hongtian is interested in programming languages and formal methods.

Jean is working on Secure Boot Process of LionsOS

Jonah is cautiously optimistic about getting a Bluetooth client working on LionsOS.

Lucas is working on a LionsOS-based Wifi Router.

Ryan is working on over-the-air update for SunSwift firmware.

Alex is working on a native USB stack for LionsOS.

Amirul is working on improving multiple protocol support in the firewall project.

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

Daiva is working on improving PMU support in LionsOS

Emrys is working on improved ICMP support in the firewall project.

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

Hary is working on the Firewall LionsOS project, to add proper Network Address Translation (NAT) to it.

Jimmy is working on the Pancake to Viper transpiler.

Larry is interested in operating system design, implementation and optimisation.

He is interested in systems research

Peng is working on the Automatic validation of SPIN models

Annotating device drivers written in Pancake for SMT backend automated verification.

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.

My research area is programming languages and software verification. My contributions to type systems around ownership, immutability, and capabilities redefined the security guarantees that modern software engineering can provide. I am currently working on some ideas for the modern module systems designs based on capabilities, combinations of abstract and algebraic effects, including for the world of fully verified and secure software targeting embedded and quantum computing systems.

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

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.

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.

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