Trustworthy Systems

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 Chief Technology Officer for Audinate.

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.

Advancement of automated deduction, in particular first-order logic theorem proving; applications for software verification, knowledge representation, and business rules/process analysis; exploiting connections into related areas such as logic programming, description logics and nonmonotonic reasoning.

David is currently researching how formal verification of low-level C code can be simplified, using automatic specification abstraction in Isabelle/HOL.

Matthias' research interest is in Formal Methods, more specifically in interactive theorem proving, software verification, and concurrency.

Toby's research interests broadly concern the application of formal methods to enable the cost-effective development of secure software and systems.

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.

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

Angus is learning about seL4 through the current driver initiative

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

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

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.

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

Damon is interested in operating systems, hardware, and the relationships between the two.

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.

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.

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.

Kent left TS to work for a startup in July 2020.

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 is currently working on verifying functional correctness for the MCS version of seL4.

Remy is working with Johannes on a compiler for pancake.

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

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

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.

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.

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 is now researcher at Microsoft Research, Redmond.

My current research area is metrics and countermeasures for side-channel leaks in componentized secure systems.

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.

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

I am interested in Interactive theorem proving. My PhD project is about mechanizing optimality properties in SAT based planning algorithms.

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

Cameron works on providing profiling support to seL4

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.

Mr Chapman's research interests include computer architectures, embedded systems, operating systems and virtual machines. His thesis involves developing a virtual machine monitor for the Itanium architecture, with a number of novel features.

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.

Alex was training to be a system administrator in our group. He left to become part of a Cloud Computing provider.

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

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

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.

Franck's research interests include software verification techniques, static analysis, model-checking, SMT-solvers, as well as infinite state systems, verification and control of timed systems, timed logics or worst-case execution time.

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

Leonid's research interests are centred around the use of formal techniques for building better operating systems.

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.

Distributed systems, mircokernels, embedded control systems.

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.

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.

Overloaded systems & Admission control Network protocol stacks Device drivers

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.

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.

Mothy is broadly interested in operating systems, distributed systems, and networks. His current interests include building distributed applications using declarative queries and software dataflow, and efficient execution of software dataflow graphs directly inside virtual machines.

Virtualisation Microkernels Performance of Virtualised Guests

Dr Varuni Witana joined NICTA as a senior researcher in February 2004. She is attached to the Embedded, Real-Time & Operating Systems (ERTOS) program and is currently working on the Digital Audio Networking project. Her active research interests include digital audio networking, precision networked clock synchronization. Other research interests include 802.11 wireless networking and multimedia communications.