News
(archive)
Last Updated: June 2018
OpenGov Recognition of Excellence Award for the CDDC
New Paper on the Benefits and Drawbacks of Proofs for Secure Software
Paul van Oorschot and I have just made available a draft
of an upcoming paper, “Formal Proofs, the Fine Print and Side Effects”
[to appear at IEEE Secure Development Conference (SecDev) 2018 
],
which takes a critical look
at the role of formal proofs for developing secure software.
This paper is aimed primarily at those who want to better understand
what value and drawbacks proofs have for secure software development.
Formal verification is currently receiving a lot of attention. We believe
that it is important, especially for those outside the verification community, to
understand its value as well as its shortcomings.
Rather than seed doubt on the enterprise
of proof and formal verification, our aim is to stimulate interest
and further exploration.
To quote from the
anonymous reviewers:
“The paper provides a very readable introduction to the topic, clarifying the differing interpretations of "the meaning of proofs", and resulting misunderstandings. The presentation is elaborated with many examples from recent literature and state of the art verification efforts.
The paper raises a number of important unanswered questions on the relationship between formal methods and security assessments of real systems.”
We hope that this paper will seed ongoing efforts to better understand
how proofs can be used most effectively to build secure systems.
Welcome Gidon Ernst
COVERN: Open Source Release and EuroS&P
The COVERN project (Compositional Verification and Refinement of
Noninterference) has gone open source! This project is a major part of my group's ongoing work on verified Information Flow Security for concurrent programs. The COVERN project has developed two major artifacts (both of which are under active development):
- The COVERN logic: a program logic for compositionally verifying information flow security of shared-memory concurrent programs,
- The COVERN compiler: a proof of concept, formally verified compiler for shared-memory concurrent programs, that provably preserves information flow security (i.e. ensures that the compiled program does not leak information, if the source program was verified as secure in the COVERN logic).
At the heart of COVERN is its support for data-dependent classification, in which the sensitivity of data can be dictated by other data. The COVERN logic exploits this to allow natural specifications of information flow contracts between concurrently-executing components, to support compositional reasoning. The COVERN compiler is the first one we know of that is verified to preserve data-dependent noninterference for concurrent programs.
The COVERN logic is described in our research paper [IEEE European Symposium on Security & Privacy (EuroS&P) 2018 ]. That paper also discusses how we applied the COVERN logic to model
and verify the functionality of the software components of our award-winning Cross Domain Desktop Compositor (CDDC) system, and to our knowledge is the first foundational machine-checked proof of information flow
security for a non-trivial shared-memory concurrent program in the literature.
About Me
I am a Lecturer 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 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 ]
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. So far, we have developed
an initial framework for exploring these questions [IEEE Computer Security Foundations Symposium (CSF) 2016 ], which is publicly
available in the
Archive of Formal Proofs (AFP) as the two AFP entries:
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 ] 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 ].
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 ] 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 ] 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 
].
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 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 ].
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.
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.
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.
Teaching
In 2017, I am currently teaching:
I have previously taught:
- SWEN90006 - Software Testing and Reliability (2016)
And before that, at UNSW:
- COMP4161 - Advanced Topics in Software Verification (2010, 2011, 2012, 2013, 2014 as Lecturer in Charge, 2015)
- COMP9241 - Advanced Operating Systems (Guest lecturer in Operating Systems Security, 2011, 2012, 2013, 2014, 2015)
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.
