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 national iAwards, following its earlier success winning three South Australia iAwards:

  • 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 ACSAC'16 paper (see publication list below).
• 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

Publications

		Rob Sison and Toby Murray Verified secure compilation for mixed-sensitivity concurrent programs Journal of Functional Programming, Volume 31, pp. e18, 2021
		Rob Sison Proving confidentiality and its preservation under compilation for mixed-sensitivity concurrent programs PhD Thesis, UNSW, Sydney, Australia, October, 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
		Gidon Ernst and Toby Murray SecCSL: security concurrent separation logic International Conference on Computer Aided Verification, pp. 208–230, July, 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
		Mark Beaumont, Jim McCarthy and Toby Murray The Cross Domain Desktop Compositor: Using hardware-based video compositing for a multi-level secure user interface Annual Computer Security Applications Conference (ACSAC), December, 2016