Skip to main content

Cross Domain Desktop Compositor

CDDC Logo

Cross Domain Desktop Compositor

The Cross Domain Desktop Compositor (CDDC) is one activity of the Trustworthy Systems project, and is a collaboration between Data61 and DST Group.

Latest News

  • CDDC wins two national iAwards

    August 2017 The CDDC won two 2017 iAwards, following its earlier success winning 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 simulteneously. Software solutions, on the other hard, 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

Cross Domain Desktop Compositor

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:
  • 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

Toby Murray, toby.murray<at>data61.csiro.au & Kevin Elphinstone, kevin.elphinstone<at>data61.csiro.au

People


Publications

Abstract PDF Toby Murray, Robert Sison, Edward 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
Abstract PDF 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
Abstract
Slides
PDF 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
Abstract PDF 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.
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Served by Apache on Linux on seL4.