Building Highly-Secure Systems at Reasonable Cost -- Branching Out
with Formal Verification.


The past decade has witnessed a sea change in the perception of formal
software verification. For instance, the microkernel seL4, whose
correctness and security have been formally verified, is routinely
cited to argue the improving power of verification for critical
software. However, formal verification remains a long way from
influencing software development practice, not least because it remains
poorly integrated with programming languages.

In this talk I argue that, just as domain specific programming languages
improve programmer productivity, verification can be greatly simplified
by programming critical software in special purpose languages designed
for verification. I present some recent work applying this idea to
develop formally verified file systems code in collaboration with
UNSW's Programming Languages and Systems Group, where we developed
the world's first pure, functional language with a self-certifying
compiler to C. I will also present some early work applying these ideas
to develop security-critical systems in collaboration with the Australian
Government's Defence Science and Technology Group (formerly Defence
Science and Technology Organisation). Here, by carefully designing the
programming language to make security a first-class concern, we aim to
reduce the cost of verifying system security to near-zero, while achieving
unprecedented security guarantees. Finally, I draw on this collaboration
to explain the surprising interplay between security verification and
human factors that we are only just beginning to understand.


Bio:
——
Toby Murray is a Senior Researcher at Data61 (formerly NICTA), and a
Conjoint Senior Lecturer at UNSW. He leads the Programming Languages
and Information Flow Team of Data61's Trustworthy Systems Research
Group. His research is focussed on rigorous techniques for building
highly-secure systems cost-effectively.  He received his D.Phil. from
the University of Oxford in 2011. At NICTA he led the completion of the
world's first proof of information flow security for a general-purpose
OS kernel, seL4. His current research includes developing
self-certifying, verification-friendly domain specific languages to
cheaply build and verify secure systems software, and the theory to
underpin them. He is jointly leading a collaboration with the Defence
Science and Technology Group that is developing and verifying what aims
to be the world's most usable and secure cross-domain desktop device,
scheduled to undergo Defence trials later in 2016.