Last Updated: November 2015
My PhD student Sidney Amani is lead author on our upcoming ASPLOS 2016 paper, which reports on his work building verified file systems using verifying domain specific languages. This work was carried out as part of NICTA's Trustworthy File Systems team, and includes Liam O'Connor who I'm also supervising with Gabi Keller.
I and Deian Stefan are Program Committee chairs for PLAS 2016. Stay tuned for further details.
I am a Senior Researcher in the Software Systems Research Group of NICTA, and 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 Sydney with my wife and two children, breathe (and sometimes write) 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.
My research is focused on the problem of how to build highly secure computing systems cost-effectively. As part of this, I lead NICTA's work on proving computer software and systems secure, and am leading or otherwise involved in a number of projects as part of NICTA's Trustworthy Systems activity, as detailed on my NICTA 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. My NICTA page has a specific list of some current and past collaborations, some of which are explained in context below.
My NICTA page also lists grants I have been awarded.
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 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.
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 ]. I am currently collaborating with researchers from the University of Adelaide, Saarland University and WPI on techniques for detecting and responding to timing side-channel attacks.
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 Trustworthy File Systems project, has been to write verified systems software in a Domain Specific Language (DSL). The DSL is carefully designed to enable the system to be cheaply proved correct and is coupled with a verifying compiler that automatically proves that the compiled code implements the DSL's 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 Trustworthy File Systems 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.
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 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 , 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 Organisation (DSTO), in which we are building and formally verifying as secure a Cross-Domain device that allows users to interact with both highly-classified and lower-classification networks from a single display (monitor), keyboard and mouse. The device aims to be far more secure than existing solutions while also offering much greater usability, and is built and being verified on top of the seL4 kernel and its proofs of information flow enforcement.
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. While still in its very early stages, this has so far seen me engaging with some of Australia's leading researchers in Psychology and Human Decision Making.
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 software.
I am currently teaching:
I have previously taught:
I have also taught half-day courses to industry on Software Model Checking for C code using CBMC. If your company develops embedded 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.
Current PhD students:
Previous research students:
I serve, and have served, on a range of Program Committees, listed below and on my NICTA page. I am also editing a special issue of the Journal of Computer Security, and serving as a member of the Technical Community that developed the Protection Profile for General Purpose Operating Systems v4.0 (released August 2015).