Information Flow

Information Flow is one activity of the Trustworthy Systems project inside the Software System Research Group (SSRG).

• Aim: To produce a formal noninterference proof for the seL4 microkernel. This proof takes as input the current authority distribution within an seL4 system. An intransitive noninterference policy is derived from the authority distribution. The noninterference theorem says that the kernel enforces this noninterference policy.

  Unlike previous noninterference proofs for separation kernels, which generally provide no system calls to user-level applications, the noninterference proof for seL4 will be the first such proof for a general-purpose OS kernel, that provides standard facilities such as IPC, thread creation and revocation.

  To show the noninterference theorem, we need to show:

  • Authority confinement: that the authority distribution in future states does not exceed the current authority distribution.
  • Integrity: that the current subject cannot modify anything that is not allowed according to the authority distribution.
  • Confidentiality: that the current subject cannot read anything that is not allowed according to the authority distribution.

  The first requirement ensures that seL4 can enforce static noninterference policies. The second two requirements correspond to the traditional unwinding conditions for noninterference.

• Latest news: We have completed the first two steps above, namely proving authority confinement and integrity enforcement for seL4. See our ITP'11 paper for more information. We are currently well on the way to completing the third step, proving confidentiality.

• 
  

  Context: Within the context of the Trustworthy Systems project, the noninterference theorem is used to reason that seL4 isolates untrusted and trusted components. This is important because trusted components need to be verified to behave correctly; while untrusted components are generally too big to verify and can contain millions of lines of code. The noninterference theorem allows us to reason about the behaviour of trusted components independently of the untrusted components, by for instance reordering the actions of untrusted components that are interleaved with those of the trusted components.

  In systems that have no trusted components, however, and whose security goal can be stated in the form of a noninterference policy that needs to be enforced, the noninterference theorem should allow us to verify these systems directly without further effort, serving in these cases as the whole-system assurance theorem.

• Technical research challenges:

  • 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 domain-scheduler for seL4, whose scheduling decisions do not leak information between isolated domains.

• Contact: Toby Murray , toby.murray<at>nicta.com.au

People

Publications

		Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein seL4 enforces integrity 2nd International Conference on Interactive Theorem Proving, Nijmegen, The Netherlands, August, 2011
		Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood Provable security: How feasible is it? Proceedings of the 13th Workshop on Hot Topics in Operating Systems, Napa, CA, USA, May, 2011
		June Andronick, David Greenaway and Kevin Elphinstone Towards proving security in the presence of large untrusted components Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada, October, 2010