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.
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
I co-lectured COMP4161 Advanced Topics in Software Verification in T3 2023.