News

(archive)

Last Updated: September 2022

Optus Breach Media

In the wake of a massive data breach at Australia's second-largest telecommunications company, Optus, I've spent the past week doing a string of media appearances, in an effort to explain to victims how they can protect themselves from the risk of potential identity theft and fraud, and to advocate for stronger privacy regimes and improved incentives to reduce the amount of sensitive data that Australian businesses are holding and to place the onus onto them for protecting it. This has been a wonderful foray into public engagement that began when I wrote the first practical guide for how impacted customers can respond to this breach, on my personal blog, where I have actively tracked developments during the week since. That was picked-up by multiple media resulting in a range of media appearances across TV, radio, and podcast, and input into various written pieces, as well as an op ed that I wrote for Ingenium. These included:

Congratulations Dongge Liu

I am delighted to announce that my (now former) PhD student Dongge Liu successfully passed his thesis examination. Dongge's thesis, Software Testing with Monte Carlo Tree Search, examines how to apply ideas from Artificial Intelligence to the problem of automatically generating tests for programs (for instance to find vulnerabilities). Dongge's research was a wonderful collaboration involving Ben Rubinstein, Gidon Ernst, and Thuan Pham, and we look forward to future collaborations in this area.

Eureka Prize for Outstanding Science in Safeguarding Australia

I'm humbled to announce that our entry (with Mark Beaumont of DST Group, and my ex-PhD student and now postdoc Robert Sison) was awarded the 2021 Australian Museum Eureka Prize for Outstanding Science in Safeguarding Australia. Our entry describes the Cross Domain Desktop Compositor (CDDC) [Annual Computer Security Applications Conference (ACSAC) 2016 pdf] and the formal methods we developed to analyse the security of its concurrent software design [IEEE European Symposium on Security & Privacy (EuroS&P) 2018 pdf]. Many others have contributed to the CDDC project since its original conception at DST Group, not least Kevin Elphinstone who co-led the CDDC collaboration with me at NICTA, and this recognition attests to the long-term team effort that continues to underpin the success of this project.

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.

  • COVERN: Proving information flow security of concurrent programs.
  • Time Protection: Proving timing channel freedom for seL4.
  • Insecurity Logic: Proving that programs have security vulnerabilities.
  • CATCH: Cybersecurity Assurance for Teams of Computers and Humans
  • AFLTeam: Collaborative Parallel Fuzzing

Past and Dormant Research Projects

Some of my past and dormant research projects include the following.

My Group

Researchers

Current postdocs:

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.

Publications

See my publications 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 ->

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 2022, I am teaching:

I previusly taught:

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 the coordinator for the Master of IT Cyber Security degree specialisation and am a Research Integrity Advisor. I am also Deputy Director of the Defence Science Institute.

I am an Associate Editor for IEEE Security & Privacy and serve on a range of Program Committees (see below). I am a member of IFIP WG 1.7 on Theoretical Foundations of Security Analysis and Design.

Steering Committees

  • ACM Workshop on Programming Languages and Analysis for Security (PLAS) (2016--2020)

Edited Books

Program Committees