Our Partners

Cross Domain Desktop Compositor

The Cross Domain Desktop Compositor (CDDC) is a collaboration between Trustworthy Systems and DST Group.

Latest News

• 

  August 2017 The CDDC won two 2017 iAwards, following its earlier successwinning three South Australia iAwards. The CDDC was named the national:

  • Research and Development Project of the Year
  • Infrastructure and Platforms Innovation of the Year

  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.

Aim

The CDDC showcases a new way to build critical systems that are orders of magnitude more secure than traditional systems, by leveraging software verified to enforce information flow security built on top of seL4 in conjunction with secure hardware enforcement.

The CDDC allows users to access data and applications on multiple, physically separated networks on-screen simultaneously, providing a seamless user experience without sacrificing security.

Traditional systems for allowing user interaction with multiple networks rely heavily either on hardware enforced physical isolation, as in the case of KVM (Keyboard-Video-Mouse) switches which have low usability because content from different networks cannot be viewed on-screen simultaneously. Software solutions, on the other hand, offer high usability at the expense of security, and are typified by those based on virtualisation platforms whose trusted computing base (TCB) comprises millions of lines of unverified and potentially insecure code. Software solutions are also vulnerable to timing channels because they forego physical isolation. The CDDC aims to combine the best of each of these kinds of solutions, to jointly maximise both security and usability.

Method

To obtain the physical isolation security guarantees of hardware solutions, while maintaining the usability of software solutions, the CDDC employs a software-hardware co-enforcement design. Video data compositing is performed in trusted, secure hardware, which is in turn controlled by software running on seL4 which handles user input processing and switching.

• Hardware Enforcement and Video Composition: Video from each isolated network is composited on screen together to provide a unified user experience. This is enabled by sending window geometry information in-band in the video signal. This innovation, invented by our collaborators at DST Group, lies at the heart of the CDDC's design, further details of which for an earlier prototype are described in the following paper:
  • The Cross Domain Desktop Compositor: Using hardware-based video compositing for a multi-level secure user interface, Mark Beaumont, Jim McCarthy and Toby Murray, ACSAC 2016.
• Verified Secure Software Control: The secure hardware video compositing is controlled by software running on seL4, and so benefits from seL4's provable security and correctness guarantees. We are also actively working on developing new theories which will allow us to formally prove that the CDDC's software correctly controls information flows. This challenge is especially interesting because the CDDC's software, running on seL4, is a concurrent application comprising multiple software components that work in concert to enforce security.

Context

Never in history has data been more valuable to business and government and yet more vulnerable to cyber-attacks. All organisations face a dilemma: either keep data isolated to ensure its security, while decreasing its usability; or forego isolation and risk being compromised. Defence and banking are two examples where security takes precedence over usability: Defence, and internal banking systems, are protected from Internet borne attacks by deploying them on physically isolated networks. Isolation necessarily impedes efficiency: preventing an intelligence analyst from easily integrating public Internet-sourced information into classified analyses, or a bank manager from simultaneously using banking systems with everyday Internet functions. The CDDC allows achieving this same level of security without compromising usability.

Use Cases

The CDDC's use cases span not only Defence and national security, in which the operation of multiple, separate networks is ubiquitous, but also include critical systems, which must be isolated from the Internet but whose operation benefits from having access to Internet-available information, such as supervisory and control systems, medical systems, and finance and banking.

Contact

Gernot Heiser, gernot<at>unsw.edu.au

People

Publications

		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
		Rob 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, Rob 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
		Rob Sison Per-thread compositional compilation for confidentiality-preserving concurrent programs 2nd Workshop on Principles of Secure Compilation, Los Angeles, January, 2018
		Toby Murray, Rob 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