Research Fellow in Verified OS Security
School of Computing and Information Systems,
The University of Melbourne
School of Computer Science and Engineering,
I mostly work on formal methods 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 secure compilation; at present, it is 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 engineer 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.
Since 2020 I have been proud to work as a postdoctoral Research Fellow for the CS Security Research group at 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. Our goal is the provable elimination of information leakage through timing channels (ARC DP190103743).
Please feel free to email me at my institutional or personal email address.