The first paper (public preprint) summarises some of the key contributions of Robert Sison's PhD thesis, on verified secure compilation
of concurrent programs while preserving information flow security.
I'm delighted to announce that my PhD student Pengbo Yan and I have a paper 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.
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
Research and Collaborations
Note: the following is a historical snapshot of my research. See the
News Archive page for a more up-to-date
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,
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 ]
of information flow security for a general-purpose operating
system kernel, seL4, which you can read more about on the
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.
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 ].
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 ]
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 ] 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
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
device called the Cross Domain Desktop Compositor (CDDC)
[Annual Computer Security Applications Conference (ACSAC) 2016 ].
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.
Reasoning about Capability-Based Software
Continuing the work I began during my D.Phil. (PhD), where I investigated
[thesis ] 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