News

(archive)

Last Updated: July 2024

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!

CCS 2023

I'm looking forward to attending ACM CCS 2023 where I'll be presenting the most recent outcomes of the COVERN project, in which we have developed the first proved sound methods for the auto-active verification of declassification policies for concurrent programs. This work was a long-running collaboration, the bulk of which was carried out while Mukesh Tiwari was working as a postdoc here in my group (and who recently joined Swansea University as a faculty member), and in collaboration with my ex-postdoc Gidon Ernst at LMU Munich, and David Naumann at Stevens Institute of Technology. If you're interested in learning more, I'd recommend checking out the extended version of our CCS 2023 paper or, if you happen to be in Copenhagen, drop me a line and let's meet up.

Invited Talk at ICFEM 2023

I'll be giving an invited talk at the 24th International Conference on Formal Engineering Methods (ICFEM 2023), which is taking place in Brisbane later this month. I'll be speaking about the history and recent achievements of the COVERN project, which has culminated in producing the first methods for what I call Practical Verified Concurrent Program Security (the slides for my talk).

Algovis Release

I've finally gotten around to publishing the rudimentary, interactive algorithm visualisation tool that I wrote when teaching COMP90038 - Algorithms and Complexity (2021--2022) to aid students' understanding of introductory algorithms and design techniques. The tool is called Algovis and you can get it from GitHub, including full documentation, which shows the visualisations in action.

Insecurity Separation Logic

I am delighted to announce that our long-running work to develop an automatic and compositional methods for detecting information leakage vulnerabilities in programs will appear at ICFEM 2023. This work includes not only the design of a new program logic for detecting leakage (Insecurity Separation Logic) but also the implementation of its automatic application inside two tools: our own Underflow tool, and as an extension to Meta's Infer static analyzer. All materials, plus an extended version of the paper, are available on the COVERN project website.

Welcome Aaron Bembenek!

I am delighted to welcome Aaron Bembenek who joins the CATCH MURI project as a postdoc working at the intersection of formal methods and machine learning. Aaron completed his PhD at Harvard, advised by Stephen Chong. Aaron brings a wealth of expertise, including in logic programming and automated solving.

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:

Working with Me

I'm always looking for motivated students to work with. Check out my page for prospective research students.

Papers

See my papers page.

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

Under-Approximate Relational Program Logic: How to Prove your Program is Insecure

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 ->

Security Concurrent Separation Logic (SecCSL): Proving Concurrent C Programs Information-Flow Secure

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:

I have also taught half-day courses to industry on topics including:

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

Edited Books

Program Committees

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2010