Verified information flow security

This page describes our information flow verification projects.

• Latest news:

  • August 2017 The CDDC won three iAwards in South Australia, and two national iAwards. The iAwards are an annual program of the Australian Information Industry Association (aiia) that recognise and reward the technology innovations that have the potential to, or are already having a positive impact on the community.
  • December 2016 An important and ongoing case study for the information flow project, for verifying the security of systems constructed on top of seL4, is the Cross Domain Desktop Compositor (CDDC), developed in collaboration with DST Group. Our paper on the CDDC recently appeared at ACSAC 2016, and describes an early hardware prototype of the device and the key insights to using hardware video compositing to deliver a highly usable cross domain interface with an incredibly small trusted computing base (TCB). We are currently working on a feature rich implementation built on top of seL4, leveraging its verified security properties and those of the CAmkES platform.
  • July 2016 The information flow project's Rob Sison has just entered UNSW's PhD program. Rob's doctoral research will build on our recent work on compositional theories for proving information flow security and secure refinement for concurrent programs.
  • July 2016 Our compositional theories of value-dependent noninterference and secure refinement, wich we presented at CSF 2016, are now publicly available as part of the Archive of Formal Proofs.
    • A Dependent Security Type System for Concurrent Imperative Programs
    • Compositional Security-Preserving Refinement for Concurrent Imperative Programs
  • June 2016 Toby and Rob just returned from CSF 2016, where they presented the first theory able to verify concurrent programs that must keep confidential information secret from attackers, where the secrecy of data can depend on other data in the system. Importantly, this theory can not only verify the security of such programs but also whether they have been securely compiled, for instance whether a compiler has inadvertently introduced any timing leaks by performing optimisations that depend on secret data. These theories are an important first step to verifying entire systems built on top of seL4.
  • May 2016 Toby has joined University of Melbourne, where he will continue the information flow project in close collaboration with Trustworthy Systems researchers in Sydney.
  • January 2015 Toby recently visited the University of Oxford and Imperial College London where he spoke (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 and completed 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 ni=trueenforces 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> unimelb.edu.au

People

Publications

		Robert Sison and Toby Murray Verified secure compilation for mixed-sensitivity concurrent programs Journal of Functional Programming, Volume 31, pp. e18, 2021
		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
		Robert Sison 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
		Toby Murray 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