News
(archive)
Last Updated: January 2025
CSF 2025
I'm Program Chair for CSF'25, with Dominique Unruh, which is taking place this June in beautiful Santa Cruz hosted by the wonderful General Chairs Owen Arden and Mohsen Lesani. The final submission round is the Winter Cycle, whose submission deadline is February 4, AoE. Please submit your best work!
Social Media Ban and Online Age Assurance Commentary
Over the past few months I have provided extensive commentary on the Australian Government's recently-legislated social media ban, ongoing
age assurance trial, and digital identity and attestation efforts. These have included several popular media pieces I have authored:
These expand on my
commentary earlier in the year in
The Conversation back in July when the media first began to focus on these topics.
Papers at ITP and FM 2024
Two of my fabulous PhD students each have papers respectively at ITP 2024 and FM 2024, two leading conferences in formal program verification. Pengbo Yan will present his recent work on verifying oblivious algorithms at FM, while Vincent Jackson will present at ITP an elegant formalisation of RGSep (a marriage of Rely-Guarantee and Separation Logic reasoning) via separation alegras. If you're attending either event, please check out their talks!
CrowdStrike Commentary
The large-scale outage caused by CrowdStrike on July 19 has offered a unique opportunity to shed light on better ways the cyber security industry can build their software, as well as to dispel some of the misinformation that has circulated since the outage. I've written multiple pieces on these topics including:
My comentary on this issue has been picked-up widely across media in Australia and globally, including
news.com.au,
Nine news,
SBS,
Yahoo News UK,
Kurdistan24,
Nation Thailand and many more.
EDEFuzz wins Distinguished Paper Award at ICSE 2024
Over the past couple of years, my PhD student Lianglu Pan has
been working on the first mechanical method for detecting Excessive Data Exposure (EDE) vulnerabilities in
web applications. This method was devised in collaboration with Lianglu's PhD supervisors,
Thuan Pham, Shaanan Cohney, and me. We're delighted to say that this work will appear at ICSE 2024. You can check out the paper
online, which was recognised with a Distinguished Paper award. If you're attending ICSE, please say hi to Lianglu!
About Me
I am an academic in the School of Computing and Information Systems of the University of Melbourne. Prior to joining Melbourne in May 2016,
I was employed in the Software Systems
Research Group of NICTA (now Data61), and was a Conjoint Senior Lecturer in the school of
Computer Science and Engineering of
UNSW. I joined NICTA and UNSW in 2010 from
Oxford, where I completed a D.Phil. (PhD) in Computer Science, awarded in 2011.
Before moving to Oxford, I worked for the
Defence Science and Technology Organisation after my undergraduate study
at the University of Adelaide.
I live in Melbourne with my wife and two children, enjoy (and sometimes write and
record) alternative music,
and spend too much time on Twitter
engaging a hot-cold obsession with Australian politics, security and privacy.
I love great ales, informed by my days in Oxford, and rich reds, like any Adelaide
native.
Research and Collaborations
My research is focused on the problem of how to build highly secure computing
systems cost-effectively. As part of this, I work on ways to assess the security of
computer systems, methods to ensure the absence of vulnerabilities
in programs and systems, methods to detect vulnerabilities in programs, methods for designing
secure systems, and related topics. Below is a snapshot of my current research projects.
Current Research Projects
My current research projects include the following. This list does not include PhD student projects that
are yet to be made public.
Past and Dormant Research Projects
Some of my past and dormant research projects include the following.
My Group
Researchers
Current postdocs:
Current Research Assistants:
Previous postdocs and Research Assistants:
Research Students
Current PhD students:
Previous research students:
- Zhiyuan Zhang, University of Melbourne (PhD thesis: The Security Impact of Microarchitecture Optimizations
; co-supervised with Chitchanok Chuengsatiansup and Yuval Yarom)
- Mo Zhang, University of Melbourne (PhD thesis: Secure User-Driven Pairing with Implantable Medical Devices; co-supervised with Vassilis Kostakos)
- Renlord Yang, University of Melbourne (PhD thesis: An empirical analysis of the systemic performance of decentralised cryptocurrency systems; co-supervised with Udaya Parampalli and Renata Borovica-Gajic)
- Dongge Liu, University of Melbourne (PhD thesis: Software Testing with Monte Carlo Tree Search; supervised with Ben Rubinstein, Gidon Ernst, and Thuan Pham)
- Duc Than Nguyen, University of Melbourne (MPhil thesis: Foundations for Reasoning about Holistic Specifications; supervised with Ben Rubinstein)
- Robert Sison, UNSW (PhD thesis: Proving Confidentiality and Its Preservation Under Compilation for Mixed-Sensitivity Concurrent Programs; jointly supervised with Carroll Morgan and Kai Engelhardt)
- Daniel Matichuk, UNSW (PhD thesis:
Automation for Proof Engineering:
Machine-Checked Proofs At Scale
; co-supervised with Gerwin Klein)
- David (Knobby) Clarke, University of Melbourne (PhD thesis: Analyses
of Java Programs over Weak Memory; co-supervised with Tim Miller and Antonette Mendoza)
- Yude Lin, University of Melbourne (PhD thesis: Symbolic Execution with Over-Approximation; co-supervised with Tim Miller and Harald Sondergaard)
- Sidney Amani, UNSW (PhD thesis: A Methodology
for Trustworthy File Systems )
- Japheth Lim, UNSW (Honours thesis: Automatically Proving the Correctness of C Code Generation)
- Sudeep Kanav (Masters student from TU Munich, thesis: Compiler Verification for a Data Format DSL)
Working with Me
I'm always looking for motivated students to work with. Check out my page for
prospective research students.
Software and Artifacts
My group has developed various pieces of software, plus formal
artifacts embedded in interactive theorem provers such as program logics and compilers.
All are available under open source licenses.
Software
SecC: Verified Security for Concurrent C Programs
SecC is the first autoactive program verifier able to verify information flow security
for concurrent C programs.
More Information ->
Legion: Principled Automatic Test Case Generation
Legion automatically generates test cases for programs, generalising traditional
concolic testing and fuzzing, orchestrating program exploration via Monte-Carlo
Tree Search.
More Information ->
Underflow: Compositional Vulnerability Detection for C Programs
Underflow is the first first automatic tool able to compositionally detect memory-safety and information-leakage vulnerabilities in C programs.
More Information ->
Algovis: Rudimentary, Interactive Algorithm Visualisation in Python
When teaching COMP90038 - Algorithms and Complexity (2021--2022) I created a simple visualisation framework
to allow introductory algorithms students to interactively visualise the various
algorithms, and to experiment with variations on those algorithms, to better understand
them.
More Information ->
Artifacts
A
general-purpose logic that enables one to perform under-approximate reasoning about relational
properties, and the fist logic able to prove when programs are insecure.
More Information ->
SecRSL: How to Prove Efficient, Concurrent Programs Secure
The first security separation program logic able to reason about C11's weak
memory concurrency features used by highly-efficient concurrent C programs.
More Information ->
VERONICA: Verified Secure Declassification for Concurrent Programs
VERONICA is a verification method, embedded in the Isabelle/HOL theorem prover, for verifying secure declassification policies for concurrent programs.
More Information ->
A program logic for concurrent C-like programs with pointers, arrays etc., for proving they do not leak sensitive information.
More Information ->
COVERN Compiler: Verified Secure Compilation for Concurrent Programs
The COVERN Compiler is a proof-of-concept compiler embedded in the Isabelle/HOL theorem prover that provably preserves information flow security when compiling concurrent programs.
More Information ->
COVERN Logic: Verified Security for Concurrent Programs
The COVERN logic, embedded in the Isabelle/HOL theorem prover, allows one to prove that concurrent programs do not leak sensitive information.
More Information ->
Bugs
Like any researcher who works on security, my work necessarily involves discovering bugs in software.
As somebody who works on tools for proving things about programs (including the presence of bugs),
my work not only uncovers bugs in ordinary programs but also bugs in
programs that reason about other programs. Below is a
list of some bugs I've uncovered in program analysis tools during my research:
Teaching
In 2023, I am teaching:
I previusly taught:
- COMP90038 - Algorithms and Complexity (2018--2022)
- SWEN90006 - Software Security & Testing (2016--2021)
- COMP4161 - Advanced Topics in Software Verification (2010, 2011, 2012, 2013, 2014 as Lecturer in Charge, 2015)
- COMP9241 - Advanced Operating Systems (Guest lecturer in Operating Systems Security, 2011, 2012, 2013, 2014, 2015)
I have also taught half-day courses to industry on topics including:
- Separation Logic
- Software Model Checking for C code using
CBMC
If your company develops
software and would like to know how you can more easily detect and remove bugs
during development, and would like to know more, please get in touch.
Service
I am
a
Research Integrity Advisor, serve as an undergraduate Academic Advisor, as well as regularly chairing Academic Misconduct Committee hearings, amongst other things. I am also Deputy Director of the Defence Science Institute.
I am an Associate Editor for IEEE Security & Privacy and ACM Transactions on Privacy and Security (TOPS), and serve on a range of Program Committees (see below).
I am a member of IFIP's WG 1.7 on Theoretical Foundations of Security
Analysis and Design and WG 2.3 on Programming Methodology.
Steering Committees
- IEEE Computer Security Foundations Symposium (2023--2027)
- International Conference on Formal Methods in Software Engineering (FormaliSE) (2023--2025)
- ACM Workshop on Programming Languages and Analysis for Security (PLAS) (2016--2020)
Edited Books
Program Committees
2026
- ACM CCS - Formal Methods and Programming Languages Track
2025
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2010
