- January 2015 Toby recently visited the University of Oxford and Imperial College London where he spoke (video, slides) about the work of the information flow project.
- September 2014 We are applying the work developed during the information flow project to build and reason about an seL4-based cross domain solution device, in a collaboration with the Defence Science and Technology Organisation (DSTO), led jointly by Toby and Kevin Elphinstone.
- August 2014 Matthew Brassil has left the information flow project to undertake a PhD in Mathematics at the University of British Columbia.
- February 2014 Toby has recently been assisting as part of the Timing Channels project, which is closely related and complementary to the Information Flow project. The former takes an empirical focus to addressing and measuring timing channels, for instance, which are not covered by the formal information flow proofs of the latter project.
- September 2013 Following the successful completion of the seL4 noninterference proof, Daniel Matichuk has left the project to begin a PhD at NICTA in proof engineering.
- March 2013: The noninterference proof is complete! It applies to a version of seL4 with a modified scheduler that implements fixed partition scheduling, as seL4's original scheduler was never designed to enforce isolation and leaked information via its scheduling decisions. The full result, including its implications, and an analysis of its limitations, such as covert channels not covered by the proof, are reported in our Oakland 2013 paper.
- October 2012: The information flow proofs for seL4 are proceeding well. The top-level information flow security statement we are proving and the confidentiality proof calculus we are using to prove it are described in our CPP'12 paper.
- June 2012: Proving confidentiality enforcement for seL4 under refinement requires an abstract kernel specification that is largely deterministic. The seL4 abstract spec is nondeterministic, but manually creating a deterministic refinement of this spec would duplicate about 98% of it. We are avoiding this problem by making the seL4 abstract specification extensible, as described in our SEFM'12 short paper.
- August 2011: We have proved that seL4 enforces integrity and authority confinement. See our ITP'11 paper for more information.
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.
- Authority confinement: that the authority distribution in future states does not exceed that implied by the current access control policy, for well-formed policies. Authority confinement ensures that seL4 can enforce static security policies.
- Integrity: that the currently-running thread cannot modify anything that is not allowed according to the access control policy.
Following these results, proving noninterference basically boils down to proving that seL4 correctly enforces confidentiality.
- Confidentiality: that the currently-running thread cannot read anything that is not allowed according to the access control policy.
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:
- Reasoning about noninterference compositionally in concurrent systems, whose components may re-use memory locations for data of differing classifications throughout their lifetime.
- Dealing with nondeterminism in the kernel specifications; ensuring the noninterference theorem is preserved by refinement so that it holds ultimately at the code level.
- Scaling traditional confidentiality properties to an entire kernel specification with appropriate automation to make the proof tractable.
- Reconciling features such a pre-emption (for responsiveness) with separation.
- Implementing, and proving confidentiality enforcement for, a fixed partition-scheduler for seL4, whose scheduling decisions do not leak information between isolated domains.
Contact: Toby Murray , toby.murray<at>nicta.com.au
||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, December, 2012
|Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein|
seL4 enforces integrity
Interactive Theorem Proving (ITP), 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, pp. 5, Napa, USA, May, 2011