https://orcid.org/0000-0003-0313-9764
🔗
Senior Research Associate
School of Computer Science and Engineering (CSE)
UNSW Engineering
🔗
Honorary (Fellow)
School of Computing and Information Systems (CIS)
University of Melbourne
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.
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 C4 Systems).
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 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 at my institutional email address, 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.
On other professional matters, feel free to email me at either of my institutional or personal email address - again, no unsolicited attachments please.