Trustworthy Systems

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.

Mr Aidan Williams was a principal research engineer, focussing his efforts on the Digital Audio Networking project. His active research interests include digital audio networking, and new L2/L3 bridging protocols (rbridge). Other research interests include home networking, IPv6, zeroconf protocols, computer and network security, cryptographic techniques, intrusion detection, computer architecture, and operating systems.

He is now CEO for Audinate.

Dr Rauch Valenti's research interests include operating systems, distributed storage systems and parallel and distributed systems like clusters of PCs. His focus is on the performance and efficiency of these systems. He now works at Google.

Dr Ruocco's research interests include the analysis, design, and implementation of object-oriented software architectures of concurrent, distributed, time-sensitive systems (including hard real-time and Quality of Service-aware systems). He is also interested in researching novel approaches to low-level, embedded system software development. He is now a researcher at Astar in Singapore.

Simon is interested in software correctness, in particular formally verified systems and language based security. He worked on the l4.verified project. He is now at Galois.

Toby's research interests broadly concern the application of formal methods to enable the cost-effective development of secure software and systems. He is now an Associate Professor at the University of Melbourne.

Yao is interested in operating system analysis, compiler optimizations, concurrent program analysis and software reliability. He was a developer of Open64 compiler and has rich experience on the internals of mainstream compilers. He now works at Nvidia.

Alex is investigating virtIO interfaces on top of the Lions OS

Andi's main interests lie in operating systems and embedded systems, and their use in small satellite systems.

Andy is working on improving the device driver framework.

Felix's research interests include operating system design, embedded systems in general and formal methods, particularly interactive theorem proving.

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

Damon is interested in operating systems, hardware, and the relationships between the two. Damon now works at Kry10.

Dan is a research engineer in the Power Management group. He is interested in operating system design and hardware development, and has dabbled lightly in Linux kernel hacking. He is also interested in website development.

Eric is working on device virtualisation for the Microkit.

Hesham left the TS group in 2018 to go to Cambridge University for further study. His work while here, and before joining the group, was mostly around the RISC-V port of seL4.

Isitha's research interests include Operating Systems, Distributed Systems and Formal Verification. He presently works on verifying OS code using SMT solvers

Kent worked on many low-level systems projects, including rump kernels on seL4. He now works at Kry10.

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. He now works at Kry10.

Michael was working on verifying functional correctness for the MCS version of seL4. He is now at Proofcraft.

Remy is working with Johannes on a compiler for pancake.

Ryan was 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. He is now a PhD student at ANU.

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

UAV,OS, CONTROL,EMBEDDED SYS DEV

symbolic computation and fourier analysis. Xin now works at Huawei.

Yutaka's research interests include proof assistants and proof automation.

Gordon is working on adding support for memory-mapped IO for Pancake.

Nila is working on core management in Lions OS.

Dominic is working on compiler improvements to Pancake.

Ken is working on evaluating Pancake by implementing device drivers on top of seL4.

Michael is working on improving TCP performance for seL4.

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 is learning about interactive theorem proving and working on automating verification of Pancake programs.

Xavier is working on using SMT solvers for verification.

Aaron works on smartphone energy management, and is primarily interested in how multi-core applications processors can be used to reduce energy consumption when combined with well-established techniques such as frequency/voltage scaling. He also works on understanding how energy is consumed within smartphones, using physical instrumentation and measurement on real-world devices. Recently, Aaron has been exploring techniques which exploit multi-core CPUs to improve sequential performance.

Adam is interested in using formal techniques to synthesize device drivers from existing device specifications. This approach will dramatically reduce the number of operating system faults caused by drivers as well as driver development time.

Andrew's research interests included dynamic update and hot-swapping, and component- and microkernel-based operating systems. His primary focus was the development and application of dynamic update techniques to operating systems. After completing his PhD, Andrew held a post-doctoral position at ETH Zurich. He was for many years a researcher at Microsoft Research, and is now at Google.

Andrew is interested in proving computer programs to work the way that they should. Currently he is proving initialisation code that sets up the user level programs that run on seL4.

Anna was a senior engineer on the seL4 team, taking the role after completing her PhD on the mixed-criticality API and design for seL4. Anna is dedicated to bringing seL4 to the world, by building a strong team of engineers who together build a great platform and community. Anna left Trustworthy Systems in June 2019 to join Ghost Locomotion, and is now at Apple.

Bernard's research interests include worst-case execution time analysis, operating system design, process checkpointing, and generally messing with executables. He now works at Nvidia.

Cameron works on providing profiling support to seL4

Charles is working on memory safety for Pancake.

Distributed systems, mircokernels, embedded control systems. Dan held senior positions at Open Kernel Labs, General Dynamics and Nothrop Grunman and now works at Ghost Locomotion.

Dr Snowdon's research interests include embedded system design and operating system directed power management. His undergraduate thesis involved the design of a telemetry and control system for the UNSW solar powered car, Sunswift. He co-founded Metamako which was acquired by Arista Networks.

David's research area was metrics and countermeasures for side-channel leaks in componentized secure systems. He is now a researcher at ETH Zurich.

My previous research areas include: High-performance architectural simulation, Domain-specific languages, Theorem Prover performance and automation, Kernel development, Verified software

I am currently a Post-Doc at ETH Zurich.

David was researching how formal verification of low-level C code can be simplified, using automatic specification abstraction in Isabelle/HOL. He now works at Google.

David's research interests include operating systems and networks, particularly when they involve graphics or web technologies.

Mr Eldakuwe was a PhD student in NICTA's Embedded, Real-Time, and Operating Systems program. He is interested in the development of secure embedded kernels.

Etienne is interested in computer power management, energy efficiency and processor architecture. He recently completed his Masters of Computer Science in which he provides an analysis of the effectiveness of energy management mechanisms on computer processors.

As a PhD student, Harvey worked on the application of formal verification techniques such as interactive theorem proving to systems software, in particular the L4 microkernel in the context of the L4.verified project. Other research interests include computer architecture, embedded systems and security.

Leonid's research interests are centred around the use of formal techniques for building better operating systems. He now works at VMware Research.

Lucy is worked on the Device Driver Framework, to optimise device drivers running on seL4.

Overloaded systems & Admission control Network protocol stacks Device drivers

Matt's research interests include computer architectures, embedded systems, operating systems and virtual machines. His thesis involved developing a virtual machine monitor for the Itanium architecture, with a number of novel features. He co-founded Exablaze, which was acquired by CISCO. He is now at d-Matrix.

Michael is interested in operating systems (microkernels, multiprocessing, virtualisation, device drivers, networking, distributed systems), security (trusted computing, cryptography, security protocols) and formal verification (theorem proving, concurrency).

My interests are wide, and I always like learning something new. I have specifically focused on areas such as operating systems, security and graphics/cv.

Patrick is working on applying seL4 to the automotive space.

Sam is working on seL4 stufff

Vincent is interested in program verification, higher-order logic, and type theory. He is now a PhD student at the University of Melbourne

Zhi is working on adding extensible disjunctive types in higher order logic in proof assistants like Isabelle/HOL.

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

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.

Formal methods, high-assurance systems and programming language theory & design.

Formal verification

Timothy is interested in the formal modelling and verification of embedded systems; particularly issues of programming language design and semantics for reactive and timing behaviours.

My primary research interests are the performance and memory footprint of micro-kernels and micro-kernel based systems.

Philip's main research interest is in reliability and security of embedded operating systems.

Virtualisation Microkernels Performance of Virtualised Guests