Fields of Research (FoR)Computational logic and formal languages, Formal methods for software, Programming languages, Operating systems
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 prefer Rob informally and they/them but otherwise don't care what pronouns you use for me.
- 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)
- 2023: Distinguished Artifact Reviewer, OOPSLA External Review / Artifact Evaluation Committee (SPLASH 2023)
- 2021: Distinguished Artifact Reviewer, OOPSLA Artifact Evaluation Committee (SPLASH 2021)
- 2021: Co-recipient of the Australian Museum Eureka Prize for Outstanding Science in Safeguarding Australia (for research contributions to the Cross Domain Desktop Compositor)
- 2016-2020: CSIRO Data61 Research Project Award (PhD top-up scholarship)
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
Areas of supervision
I am happy to co-supervise anybody who is interested in a pursuing a Higher Degree Research candidature on any of the topics in my area of research.
Please contact me by email, initially with no attachments (no CVs, transcripts, etc.) - let's discuss our research interests and your circumstances first. 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.
- Pengbo Yan, PhD student (University of Melbourne): Development of formal methods to verify the obliviousness of probabilistic algorithms.
I co-lectured COMP4161 Advanced Topics in Software Verification in T3 2023.