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.
About me
I am an Australian formal methods researcher who pivoted to academia
after a 5-year early career stint (2008-2014) as an OS-level software
engineer with NICTA spin-out Open Kernel Labs, Inc.
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 worked for
the CS Security Research group of
The University of Melbourne's
School of CIS,
collaborating with
the Trustworthy Systems research group of UNSW's School of CSE, my alma mater,
aimed at the provable elimination of information leakage through timing channels.
I am a trans nonbinary person and in professional contexts would appreciate being referred to with they/them pronouns.
Research 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 at my institutional email address 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.
Other contact
On other professional matters, feel free to email me at either of my institutional or personal email address - no unsolicited attachments please.
https://orcid.org/0000-0003-0313-9764