The Cross Domain Desktop Compositor (CDDC) is a collaboration between Data61 and DST Group.
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.
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.
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.
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.
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.
Gernot Heiser, gernot<at>unsw.edu.au
|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
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
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