Our Partners

Time Protection

aka Timing Channel Prevention

Aim

Design, implementation, evaluation and verification of black-box OS abstractions and mechanisms for time protection: the prevention of timing channels.

Highlights

• Gernot Heiser, Toby Murray and Gerwin Klein won a 3-year (2019–2021) Discovery Grant from the ARC for verifying time protection.
• As a consequence, we're hiring postdocs with a suitable formal-methods background.
• We undertook a comprehensive analysis of microarchitectural timing channels on multiple Intel and ARM processors and the effectiveness of hardware-provided defences .

Overview

Micro-architectural timing channels result from competing access to shared, finite hardware resources. Sharing may be time-multiplexed (intra-core) or concurrent (inter-core).

Unauthorised information leakage is a violation of a system's security policy (see the background page for further explanation). Enforcing security is a primary responsibility of the operating system (OS); yet no contemporary, general-purpose OS has the means for preventing this violation. Our aim is to change this.

Our formally verified seL4 microkernel provably prevents other security violations, including through covert storage channels. This makes timing channels the last, fundamentally unsolved security problem in operating systems, and seL4 the ideal platform for solving it.

In particular, the OS must provide mandatory enforcement of timing-channel freedom, i.e. security enforcement must not depend on application cooperation. Mandatory enforcement is the only way to ensure that untrusted code operating on secret information does not leak it. Such code is commonplace: legacy software stacks running on untrustworthy mainstream OSes such as Linux, Macos or Windows, smartphone apps, browser plugins and server-provided Javascript routinely process confidential data. Furthermore, the use of gadgets in the Spectre attack has shown that even supposedly trustworthy code can be turned into a Trojan.

Hence we are looking for black-box OS-level mechanisms for providing temporary isolation. For spatial isolation such mechanisms are well-established, the core mechanism is memory protection. Here we are working on providing the corresponding temporal isolation, which we accordingly call time protection.

Approach

Our earlier investigations have shown that complete time protection is not possible on present hardware, hence solving this problem requires a hardware-software co-design approach. In other words: we need a new, security-oriented, hardware-software contract.

Consequently, we are pursuing a number of directions concurrently, with the ultimate aim of verified time protection.

Hardware-software contract

• We have defined the high-level properties of the HW-SW contract that the OS needs to provide time protection.
• We are working with the PULP team at the Integrated Systems Lab of ETH Zurich on a processor that provides sufficient mechanisms to allow the OS to provide full time protection. This will based on ETH's Ariane, a 64-bit RISC-V CPU.
• We are active on the RISC-V Foundation's Security Standing Committee to ensure the architecture will provide the right mechanisms, and help make RISC-V the most secure processor architecture.

OS mechanisms

We have designed and implemented (in seL4) fundamental time-protection mechanisms. These consist of:

• A new kernel clone mechanism that provides a policy-free way of setting up a system without any memory shared between security partitions (save a small number of kernel data structures that are accessed carefully to ensure deterministic execution). This eliminates any channels through a shared kernel image.

  Kernel cloning provides a way of identifying security-domain switches, thus informing the kernel at which context switches additional scrubbing operations are needed. This is a policy-free way of minimising isolation overheads.

• Security-partition switches that carefully reset all shared micro-architectural state, while making switch times completely deterministic, and in particular, independent of previous execution history.

• Mechanisms for partitioning lower-level caches, where flushing cost would be high and would not help if those caches are shared across cores. This employs page colouring, and extends to kernel code and data.

• Partitioning of interrupt sources, so the system is able to use interrupt-driven I/O, unlike classical separation kernels, which disable all interrupts and rely on high-overhead polled I/O.

We have demonstrated that these mechanisms are effective, to the degree that the hardware provides the right mechanisms for scrubbing or partitioning state. Please see the downloads page for accessing the relevant artefacts.

OS Abstractions

Having developed seL4 mechanisms able to provide time protection, we now are working on suitable abstractions that integrate with the existing seL4 model, in particular the new scheduling-context capabilities that provide a principled treatment of time as a resource, with the aim of supporting mixed-criticality real-time systems.

Our aim is a similarly principled model that combines both types of temporal isolation, temporal integrity for real time, and temporal confidentiality for security.

Verifying time protection

The ultimate aim is to be able to prove that our system provides complete time protection. This will require formally specifying the hardware-software contract (at as abstract a level as possible), including formally defining partitionable vs flushable hardware resources.

Specifically we are working on a operational specification of the required properties, so that time protection can be verified as a functional-correctness property without explicit reasoning about time. This approach will allow us to extend seL4's existing proofs of information flow security to also provide assurance about timing channels.

Preparatory work

Proofs

When we started this line of work a few years ago, we provided a formal proof of the absence of side channels using a lattice scheduler. However, this work is based on idealised hardware.

Mechanisms

We also empirically investigated a number of defence mechanisms suitable for black-box enforcement. The evaluations showed that these mechanisms are effective on some hardware, but fail to close channels completely on other.

Survey of attacks

In order to better understand the problem we conducted a comprehensive survey of micro-architectural timing channels.

Assessment of hardware mechanisms

Following the discovery that our defence mechanisms were not fully effective, we conducted a thorough analysis of microarchitectural timing channels of multiple generations of Intel and ARM processors. We examined the mechanisms provided by the hardware and measured their effectiveness. Our results show that all microarchitectural state we examined can be used for timing channels, including two channels (TLB and branch target buffer) that have not been demonstrated before.

More importantly, our investigation uncovered on each examined platform at least one channel that cannot be closed with any state-flushing operation provided by the hardware. This is summarised in an arXiv paper, and we provide the complete, updated results.

2020

		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
		Andrew Kwong, Daniel Genkin, Daniel Gruss and Yuval Yarom RAMBleed: reading bits in memory without accessing them IEEE Symposium on Security and Privacy, pp. 310-326, San Francisco, CA, USA, May, 2020
		Jo Van Bulck, Daniel Moghimi, Michael Schwarz, Moritz Lipp, Marina Minkin, Daniel Genkin, Yuval Yarom, Berk Sunar, Daniel Gruss and Frank Piessens LVI: Hijacking transient execution through microarchitectural load value injection IEEE Symposium on Security and Privacy, pp. 1452-1470, San Francisco, May, 2020
		Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Luca Benini and Gernot Heiser Prevention of microarchitectural covert channels on an open-source 64-bit RISC-V core Workshop on Computer Architecture Research with RISC-V (CARRV), Valencia, Spain, May, 2020
		Gernot Heiser, Gerwin Klein and June Andronick seL4 in Australia: From research to real-world trustworthy systems Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020
		Gernot Heiser Verified seL4 on secure RISC-V processors at linux.conf.au, Gold Coast, January, 2020

2019

		Claudio Canella, Daniel Genkin, Lukas Giner, Daniel Gruss, Moritz Lipp, Marina Minkin, Ahmad Moghimi, Frank Piessens, Michael Schwarz, Berk Sunar, Jo Van Bulck and Yuval Yarom Fallout: leaking data on meltdown-resistant CPUs ACM Conference on Computer and Communications Security, pp. 769-784, London, UK, November, 2019
		Daniel Genkin, Romain Poussier, Rui Qi Sim, Yuval Yarom and Yuanjing Zhao Cache vs. key-dependency: Side channeling an implementation of pilsung IACR Transactions on Cryptographic Hardware and Embedded Systems, Volume 2020, Issue 1, pp. 231-255, November, 2019
		Qian Ge Principled elimination of microarchitectural timing channels through operating-system enforced time protection PhD Thesis, UNSW, Sydney, Australia, October, 2019
		Anatoly Shusterman, Lachlan Kang, Yarden Haskal, Yosef Meltser, Prateek Mittal, Yossef Oren and Yuval Yarom Robust website fingerprinting through the cache occupancy channel USENIX Security Symposium, pp. 639-656, Santa Clara, August, 2019
		Gernot Heiser Security needs a better hardware-software contract Invited talk at Design Automation Conference (DAC), Las Vegas, NV, USA, June, 2019
		Gernot Heiser, Gerwin Klein and Toby Murray Can we prove time protection? Workshop on Hot Topics in Operating Systems (HotOS), pp. 23-29, Bertinoro, Italy, May, 2019
		Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Haburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwartz and Yuval Yarom Spectre attacks: Exploiting speculative execution IEEE Symposium on Security and Privacy, pp. 19-37, San Francisco, May, 2019 Distinguished Paper Award!
		Eyal Ronen, Robert Gillham, Daniel Genkin, Adi Shamir, David Wong and Yuval Yarom The 9 lives of bleichenbacher's CAT: new cache ATtacks on TLS implementations IEEE Symposium on Security and Privacy, pp. 966-983, San Francisco, May, 2019
		Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser Time protection: The missing OS abstraction EuroSys Conference, Dresden, Germany, March, 2019 Best Paper Award!

2018

		Qian Ge, Yuval Yarom and Gernot Heiser No security without time protection: we need a new hardware-software contract Asia-Pacific Workshop on Systems (APSys), Korea, August, 2018 Best Paper Award! Complete timing-channel data for evaluated x86 and Arm platforms.
		Qian Ge, Yuval Yarom, David Cock and Gernot Heiser A survey of microarchitectural timing attacks and countermeasures on contemporary hardware Journal of Cryptographic Engineering, Volume 8, Issue 1, pp. 1-27, April, 2018
		Gernot Heiser For safety's sake: we need a new hardware-software contract! IEEE Design and Test, Volume 35, Issue 2, pp. 27-30, March, 2018

2017

Qian Ge, Yuval Yarom, Frank Li and Gernot Heiser Your processor leaks information — and there's nothing you can do about it arXiv preprint arXiv:1612.04474, 2017

2016

Fangfei Liu, Qian Ge, Yuval Yarom, Frank Mckeen, Carlos Rozas, Gernot Heiser and Ruby B Lee CATalyst: defeating last-level cache side channel attacks in cloud computing IEEE Symposium on High-Performance Computer Architecture, pp. 406–418, Barcelona, Spain, March, 2016

2015

		Yuval Yarom, Qian Ge, Fangfei Liu, Ruby B. Lee and Gernot Heiser Mapping the Intel last-level cache The Cryptology ePrint Archive, September, 2015
		Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser and Ruby B Lee Last-level cache side-channel attacks are practical IEEE Symposium on Security and Privacy, pp. 605–622, San Jose, CA, US, May, 2015

2014

		David Cock, Qian Ge, Toby Murray and Gernot Heiser The last mile: An empirical study of some timing channels on seL4 ACM Conference on Computer and Communications Security, pp. 570–581, Scottsdale, AZ, USA, November, 2014
		David Cock Leakage in trustworthy systems PhD Thesis, UNSW, Sydney, Australia, August, 2014
		David Cock From probabilistic operational semantics to information theory — side channels with pGCL in isabelle Proceedings of the 5th International Conference on Interactive Theorem Proving, pp. 1–15, Vienna, Austria, July, 2014

2013

David Cock Practical probability: Applying pGCL to lattice scheduling Proceedings of the 4th International Conference on Interactive Theorem Proving, pp. 1–16, Rennes, France, July, 2013

2012

David Cock Verifying probabilistic correctness in Isabelle with pGCL Proceedings of the 7th Systems Software Verification, pp. 1–10, Sydney, Australia, November, 2012

2011

David Cock Exploitation as an inference problem 4th Workshop on Artificial Intelligence and Security, pp. 105–106, Chicago, IL, USA, October, 2011