This page describes our information flow verification projects.
Aim: To produce formal proofs and frameworks for reasoning about information flow security and seL4-based systems. For now, this work excludes timing channels, which must be dealt with using complementary techniques being developed as part of the Timing Channels project.
A major previous success of this project was the development of the world's first proof of information flow security for the implementation of a general-purpose kernel, namely seL4. This theorem now serves as the foundation on which we are developing compositional frameworks for proving the informationn flow security of concurrent systems built on top of seL4. In an ongoing collaboration with DSTO we will build and verify a secure seL4-based cross-domain solution, providing an ideal case study on which to apply these frameworks.
The seL4 information flow proof proof takes as input the current access control policy of an seL4 system. An intransitive noninterference policy is derived from the access control policy. The noninterference theorem says that the kernel enforces this noninterference policy, or in other words shows that the kernel allows no other information flows than those implied by the current access control policy.
Unlike previous noninterference proofs for separation kernels, which generally provide no system calls to user-level applications, the noninterference proof for seL4 is the first such proof for a general-purpose OS kernel, that provides standard facilities such as IPC, thread creation and revocation. It is also the first such proof of its kind to apply not just to a design-level model of the OS kernel but to the actual C code that implements the kernel and enforces its security.
Method: Before proving noninterference, we first proved that the kernel correctly enforces data integrity and authority confinement. These results were published at ITP'11.
Following these results, proving noninterference basically boils down to proving that seL4 correctly enforces confidentiality.
Integrity and confidentiality together yield the unwinding conditions needed to prove noninterference for seL4. The specific formulation of noninterference we proved is presented in detail in our CPP'12 paper. The noninterference proof for seL4 was itself publishedat the 2013 IEEE Symposium on Security and Privacy.
Context: Within the context of the Trustworthy Systems project, this work complements that of the Whole-System Assurance activity, whose focus is on proving safety properties (like data integrity) of seL4-based systems with large untrusted components. We focus instead on information flow properties (like confidentiality, and certain forms of integrity). However there is much overlap between these activities.
In systems that have no trusted components, and whose security goal can be stated in the form of a noninterference policy that needs to be enforced, the seL4 noninterference theorem serves as whole-system assurance theorem.
Broadly, the noninterference theorem is a very powerful piece of evidence about seL4's utility as a separation kernel -- the strongest such piece of evidence ever produced for a general-purpose OS kernel.
Technical research challenges:
Contact: Toby Murray, toby.murray<at>nicta.com.au
|Gernot Heiser, Toby Murray and Gerwin Klein|
Towards provable timing-channel prevention
ACM Operating Systems Review, Volume 54, Issue 1, pp. 1-7, August, 2020
||Robert Sison and Toby Murray|
Verifying that a compiler preserves concurrent value-dependent information-flow security
International Conference on Interactive Theorem Proving, pp. 27:1–27:19, Portland, USA, September, 2019
|Carroll Morgan, Annabelle McIver and Tahiry Rabehaja|
Abstract hidden markov models: A monadic account of quantitative information flow
Mathematical Structures in Computer Science, Volume 15, Issue 1, pp. 36:1-36:50, March, 2019
|Toby Murray, Robert Sison and Kai Engelhardt|
COVERN: A logic for compositional verification of information flow control
European Conference on Security and Privacy (EuroS&P), London, United Kingdom, April, 2018
Per-thread compositional compilation for confidentiality-preserving concurrent programs
2nd Workshop on Principles of Secure Compilation, Los Angeles, January, 2018
|Toby Murray, Robert Sison, Ed Pierzchalski and Christine Rizkallah|
Compositional verification and refinement of concurrent value-dependent noninterference
IEEE Computer Security Foundations Symposium, pp. 417–431, Lisbon, Portugal, June, 2016
On high-assurance information-flow-secure programming languages
ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pp. 43–48, Prague, Czech Republic, July, 2015
||Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein|
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013
|Toby Murray and Thomas Sewell|
Above and beyond: seL4 noninterference and binary verification
Abstract, 2013 High Confidence Software and Systems Conference, Annapolis, MD, May, 2013.
|Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein|
Noninterference for operating system kernels
International Conference on Certified Programs and Proofs, pp. 126–142, Kyoto, Japan, December, 2012
|Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein|
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325–340, Nijmegen, The Netherlands, August, 2011
|Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood|
Provable security: How feasible is it?
Workshop on Hot Topics in Operating Systems (HotOS), pp. 5, Napa, USA, May, 2011