News

(archive)

Last Updated: November 2021

Two Papers in Journal of Functional Programming Special Issue on Secure Compilation

I am delighted to announce the publication of two papers in the Special Issue on Secure Compilation of the Journal of Functional Programming (JFP). Each is an archival paper reporting on a major piece of work I've been lucky enough to have been involved in.

Together these two papers highlight the breadth of recent work on secure compilation. Check out the special issue to see even more.

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.

SecRSL paper at OOPSLA 2021

I'm delighted to announce that my PhD student Pengbo Yan and I have a paper pdf that will be appearing at OOPSLA 2021. Our paper describes SecRSL which is a program logic we developed for proving that concurrent C programs that make use of C11's Release-Acquire weak memory features are information-flow secure. SecRSL is the first information flow logic developed for a high-level language able to reason about weak-memory concurrency. Moreover it is the first security separation logic proved sound over an axiomatic memory model, and so our paper also presents the first formal definition of information flow security for an axiomatic memory model. We describe not only SecRSL but also how we applied it to verify a range of secure concurrency primitives and how, by taking advantage of C11's weak-memory concurrency features, those primitives perform much better than their traditional sequentially-consistent counterparts. We hope SecRSL will herald many more secure concurrent programs in future.

SecRSL is the latest success from my ongoing COVERN 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

Note: the following is a historical snapshot of my research. See the News Archive page for a more up-to-date picture.

My research is focused on the problem of how to build highly secure computing systems cost-effectively. As part of this, I lead Data61's work on proving computer software and systems secure, and am leading or otherwise involved in a number of projects as part of Data61's Trustworthy Systems activity, as detailed on my Data61 page. Below are listed my current active areas of research and collaboration. My interest in security, and belief about the best ways to build secure systems more effectively, is very broad. Thus I tend to collaborate across various disciplines including Software Engineering, Systems, Hardware Security, Formal Methods, Programming Languages and Human Factors.

Information Flow   One of the biggest challenges faced in security today is how to ensure that computer systems can keep their secrets from well-motivated adversaries — just think of how many news stories you've read about personal information having been stolen and publicised by attackers. For this reason, a large part of my research has investigated how to guarantee the absence of unwanted information leaks in computer software and systems. I led the team that completed the world's first proof [IEEE Symposium on Security and Privacy ("Oakland" S&P) 2013 pdf] of information flow security for a general-purpose operating system kernel, seL4, which you can read more about on the Information Flow project page. This proof, along with subsequent work, guarantees that seL4 will prevent all unwanted information leaks up to timing channels, i.e. that it is free of unwanted storage channels.

My current work in this space aims to understand how to verify information flow security for concurrent programs (like those that run on top of seL4), and how to compile such programs while making sure they still preserve their security guarantees. This work is being carried out under the banner of the open-source COVERN project [IEEE European Symposium on Security and Privacy (EuroS&P) 2018 ], which builds on our earlier work for exploring these questions [IEEE Computer Security Foundations Symposium (CSF) 2016 ].

Alongisde this work, I've also been exploring how to build program logics for proving information flow security of low-level C code. A recent short paper [Workshop on Programming Languages and Analysis for Security (PLAS) 2017 pdf] describes the main ideas, developed in collaboration with Samuel Gruetter (MIT).

Timing Channels   Timing channels leak information (whether intentionally or not) to an adversary who can observe differences in the relative timing of different events. Unlike for storage channels, we are not yet able to prove the absence of timing channels in systems, largely because many timing channels exploit the timing properties of hardware microarchitectural features, like caches, which are not even documented, so are very difficult to reason about formally. For this reason, these channels must be dealt with empirically. I have been involved in NICTA's Timing and Side Channels activity, where we pioneered new techniques for empirically measuring the effectiveness of various timing channel mitigation techniques for seL4 [ACM Conference on Computer and Communications Security (CCS) 2014 pdf].

Cost-Effective Verified Systems via Verifying DSLs   While security proofs, like those for seL4 that I have led, can give extremely high levels of assurance for security-critical systems, they remain relatively expensive to perform. Much of my recent research has therefore focused on how to reduce the cost of verifying properties of systems software. One technique I have explored, in collaboration with Programming Languages researchers from UNSW (notably Gabi Keller) via NICTA's Cogent project, has been to write verified systems software in a Domain Specific Language (DSL). Cogent [International Conference on Functional Programming (ICFP) 2016 pdf] is a programming language that is carefully designed to enable systems written in it to be cheaply proved correct. It is coupled with a verifying compiler [International Conference on Interactive Theorem Proving (ITP) 2016 pdf] that automatically proves that the compiled code implements the Cogent source semantics. In conjunction with my PhD students Sidney Amani and Liam O'Connor (co-supervised with Gabi Keller), my undergraduate thesis student Japheth Lim, and the rest of the Cogent team, we have used this technique to build and (partially) formally verify correct Linux file systems far more cheaply than e.g. the verification for the seL4 kernel [International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) 2016 html].

Proof Cost Estimation   The effort required to verify software as being secure is an obvious barrier to its wide adoption. But just as important is the inability of software engineering managers to be able to predict the costs (and associated benefits) of proving their software correct. Another of my recent research activities has been to investigate this question in the context of NICTA's Proof, Measurement and Estimation (PME) project. As part of this work, my PhD student Daniel Matichuk and I, in collaboration with Empirical Software Engineering researchers and NICTA's PME team, explored the relationship between the size of a statement to be proved about a piece of software, and the amount of effort required to prove the statement (using as a proxy the number of lines required to write the proof, which we had already established [ACM/IEEE Symposium on Empirical Software Engineering and Measurement (ESEM) 2014 pdf] is strongly linearly related). To do so, we crunched historical data about the various seL4 proofs as well as some other large, publicly available software proofs. We established empirically for the first time [International Conference on Software Engineering (ICSE) 2015 pdf] that a consistent relationship exists here and that it is in fact quadratic. This work is the first step towards building a predictive model for estimating the level of effort required to verify a piece of software.

Proof Automation   Besides writing verified software in custom DSLs leveraging verifying compilation to dramatically ease the cost of formally verifying secure systems, another more direct approach I have investigated with my PhD student Daniel Matichuk has been to develop languages in which custom, automatic proof tactics can be written for the Isabelle proof assistant. Daniel designed and developed Eisbach [International Conference on Interactive Theorem Proving (ITP) 2014 pdf, Journal of Automated Reasoning (to appear)] the first such language that integrates with Isabelle's high-level notation for writing (structured) proofs, and so requires no knowledge of Isabelle's internals, making it usable by relative novices.

Highly-Secure and Usable, Verified Cross Domain Systems   All of the above research is aimed towards being able to build extremely secure systems — and to demonstrate via rigorous evidence that they are indeed so — at reasonable cost. I am currently leading, alongside Kevin Elphinstone, a collaboration with the Defence Science and Technology Group (DST Group), in which we are building and formally verifying as secure a clever Cross-Domain device called the Cross Domain Desktop Compositor (CDDC) [Annual Computer Security Applications Conference (ACSAC) 2016 pdf]. The CDDC allows users to interact with both highly-classified and lower-classification networks from a single display (monitor), keyboard and mouse. Its design makes it far more secure than existing solutions while also offering much greater usability, showing that with clever design usability and security need not be in conflict. We are currently working on building and verifying an seL4-based implementation of the device, leveraging our current work on verified information flow security.

Usable Security   As part of my work on building and verifying cross domain systems, I am also investigating how issues of usability and security, including human cognition and perception, interact with the process of formally proving a system secure. This work is still in its very early stages [Australian Computer Human Interaction Conference (OzCHI) 2018 pdf], and there remains much more to be done.

Reasoning about Capability-Based Software   Continuing the work I began during my D.Phil. (PhD), where I investigated [thesis pdf] techniques to formally reason about the security of capability-based security-enforcing software abstractions, I am currently collaborating with researchers from Imperial College London, Victoria University Wellington and Google on techniques for formally reasoning about risk and trust (including the absence of such) for capability-based software.

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

Google Scholar has a fairly complete list of my publications. You can also try my entry on DBLP, which may not be quite so complete.

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

Teaching

In 2020, I am teaching:

At UNSW, I 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 the coordinator for the Master of IT Cyber Security degree specialisation and am a Research Integrity Advisor.

I serve, and have served, on a range of Program Committees, listed below. I am a member of IFIP WG 1.7 on Theoretical Foundations of Security Analysis and Design.

Steering Committees

Edited Books

Program Committees