The Quest for Assured Confidentiality
- 14:00 13th January 2015 ( week 0, Hilary Term 2015 )Tony Hoare Room, Robert Hooke Building
Protecting the confidentiality of sensitive information has been a goal of secure operating systems kernels for the last 30 years. However, monolithic kernels are routinely exploited and even smaller kernels and hypervisors cannot guarantee the absence of storage and timing channels.
The seL4 kernel was famously the world's first general-purpose kernel to have its C code implementation proved functionally correct. In this talk, we describe the ongoing quest to assure that seL4 can enforce strong confidentiality against untrustworthy programs, using both formal and empirical approaches.
The first step on this journey was a proof of intransitive noninterference for the seL4 implementation, which ensures confidentiality up to (1) potential storage channels in parts of the instruction set architecture (ISA) unused by seL4 and (2) timing channels. We then tackled ISA storage channels by additional proofs over a trustworthy formal model of the ARMv6 ISA. These confirmed a potential channel, since corrected, undetected by the noninterference proof.
However, timing channels remain beyond the reach of formal proof.
Therefore, we recently performed a thorough empirical analysis of the effectiveness of some well known timing channel countermeasures implemented in seL4. The results revealed that the effectiveness of each countermeasure is highly platform dependent, confirming the value of the empirical approach. Taken together, this body of work is the most comprehensive collection of evidence yet assembled on the ability of a general-purpose kernel to enforce confidentiality.
Speaker bio
Toby Murray is a Senior Researcher at NICTA and a Conjoint Lecturer in the School of Computer Science and Engineering at the University of New South Wales. His research focuses on the use of formal verification to build and assure highly secure systems. His current work is centred around building and assuring high security systems on the seL4 microkernel, as well as developing proof-producing domain specific languages (DSLs) for writing verified systems software at minimal cost.Toby previously led NICTA's Information Flow project which completed the world's first proof of intransitive noninterference for a general-purpose kernel, seL4, building on seL4's earlier landmark functional correctness verification.
Before joining NICTA, Toby obtained his D.Phil. from the University of Oxford in 2010. His thesis applied the process algebra CSP to analyse the security of reusable capability-based software abstractions, and was supervised by Gavin Lowe. Before that he worked for the Defence Science and Technology Organisation researching and developing next generation secure pervasive computing technology as part of the Annex project.
Share this:
