Researcher

Keywords

Fields of Research (FoR)

Computational logic and formal languages, Formal methods for software, Programming languages, Operating systems

Biography

I am an Australian computer engineer who pivoted to formal methods research after a 5-year early career stint (2008-2014) as an OS-level software developer with NICTA spin-out Open Kernel Labs, Inc. (including following its acquisition by General Dynamics). My long-term objective since 2014 has been to gain the skills, experience, and qualifications necessary to assist, conduct, and eventually lead groundbreaking research and development aimed...view more

I am an Australian computer engineer who pivoted to formal methods research after a 5-year early career stint (2008-2014) as an OS-level software developer with NICTA spin-out Open Kernel Labs, Inc. (including following its acquisition by General Dynamics). My long-term objective since 2014 has been to gain the skills, experience, and qualifications necessary to assist, conduct, and eventually lead groundbreaking research and development aimed at improving the trustworthiness and reliability of system-critical software.

To this end, in 2016 I completed a master's degree by coursework focused on computer security and formal methods. In 2020, I attained my doctorate for my dissertation on the application of interactive theorem proving to make feasible the verification of both information-flow security and its preservation by a compiler for concurrent programs that share memory both (1) between threads and (2) between security domains.

From 2020 to 2023 I was proud to work as a postdoctoral Research Fellow for the CS Security Research group of the University of Melbourne's School of Computing and Information Systems (CIS), in close collaboration with the Trustworthy Systems research group of UNSW Sydney's School of Computer Science and Engineering (CSE), my alma mater, aimed at the provable elimination of information leakage through timing channels (ARC DP190103743).

Since 2023 I have held the position of Senior Research Associate working with the Trustworthy Systems research group at UNSW Sydney's School of CSE and an Honorary (Fellow) position with the University of Melbourne's School of CIS.

I am a trans nonbinary person and in professional contexts prefer Rob and they/them but otherwise don't care what pronouns you use for me.


My Qualifications

  • Doctor of Philosophy: Computer Science and Engineering (UNSW Sydney, November 2020)
  • Master of Information Technology, with Excellence (UNSW Sydney, August 2016)
  • Bachelor of Engineering: Computer Engineering, with Honours Class 1 (UNSW Sydney, May 2010)

My Awards


My Research Activities

I research and develop formal methods, primarily for proving absences of information flow in systems for high-assurance use cases. In the past, my focus was on complications arising from concurrency and refinement to enable secure compilation; more recently, it has been on how to prove an OS enforces absences of information leaks through the microarchitecture. More broadly, I am interested in all applications of interactive theorem proving, as well as anything to do with the design and construction of software systems with formally proved functional-correctness and security properties at scale.


My Research Supervision


Supervision keywords


Areas of supervision

I am willing to discuss potential supervision with anyone interested in a pursuing a Higher Degree Research candidature on a topic in my areas of research.

Please contact me by email to discuss our research interests and your circumstances. If you have a professional online presence, especially hosted or verified by any institutional websites (e.g. employer or university), public code repositories (e.g. GitHub) or publication databases (e.g. DBLP), please include any links to those.


Currently supervising

  • Pengbo Yan, PhD student (University of Melbourne): Formally verifying the security of probabilistic oblivious algorithms.
  • Kevin Tran, PhD student (UNSW): A framework for reasoning about the multi-core seL4 code.
  • Junming Zhao, PhD student (UNSW): Compositional formal verification of network services in the seL4 Device Driver Framework.
  • Kurt Wu, PhD student (UNSW): Verifying inter-component communications in LionsOS.

My Teaching

I have co-lectured:

  • COMP3161/9164 Concepts of Programming Languages in T3 2024 and 2025.
  • COMP4161 Advanced Topics in Software Verification in T3 2023, 2024 and 2025.
View less