Cross Domain Desktop Compositor
- 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.
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.
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.
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.
|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
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, pp. 5, Napa, USA, May, 2011