Trustworthy Systems

Our Partners The University of Melbourne
The Australian Research Council

Time Protection
aka Timing Channel Prevention


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



A timing Channel based on cache contention

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.


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

OS mechanisms

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

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


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.


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.


Gernot Heiser




  • Curtis Millar
  • David Cock
  • Kevin Elphinstone
  • Qian Ge
  • Ryan Barry
  • Scott Buckley
  • Thomas Bove
  • Toby Murray
  • Yuval Yarom


Abstract PDF Nils Wistoff1, Robert Balas, Alessandro Ottaviano, Gernot Heiser and Luca Benini
ISA support for hardware resource partitioning in RISC-V
RISC-V Summit Europe, Munich, DE, June, 2024


Abstract PDF Marcelo Orenes-Vera, Hyunsung Yun, Nils Wistoff, Gernot Heiser, Luca Benini, David Wentzlaff and Margaret Martonosi
AutoCC: Automatic discovery of covert channels in time-shared hardware
International Symposium on Microarchitecture (MICRO), Toronto, ON, CA, October, 2023
PDF Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein and Gernot Heiser
Formalising the prevention of microarchitectural timing channels by operating systems
International Symposium on Formal Methods (FM), Lübeck, DE, March, 2023
Abstract PDF Scott Buckley, Robert Sison, Nils Wistoff, Curtis Millar, Toby Murray, Gerwin Klein and Gernot Heiser
Proving the absence of microarchitectural timing channels
arXiv preprint arXiv:2310.17046, 2023
Abstract PDF Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Gernot Heiser and Luca Benini
Systematic prevention of on-core timing channels by full temporal partitioning
IEEE Transactions on Computers, Volume 72, Number 5, pp. 1420–1430, 2023


Abstract PDF Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Luca Benini and Gernot Heiser
Microarchitectural timing channels and their prevention on an open-source 64-bit RISC-V core
Design, Automation and Test in Europe (DATE), virtual, February, 2021
Best Paper Award


Abstract PDF 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
Abstract PDF
Presentation Video
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
Abstract PDF 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
Abstract Slides
Gernot Heiser
Verified seL4 on secure RISC-V processors
at, Gold Coast, January, 2020


Abstract PDF Qian Ge
Principled elimination of microarchitectural timing channels through operating-system enforced time protection
PhD Thesis, UNSW, Sydney, Australia, October, 2019
Abstract Slides Gernot Heiser
Security needs a better hardware-software contract
Invited talk at Design Automation Conference (DAC), Las Vegas, NV, USA, June, 2019
Abstract PDF 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
Presentation Video
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser
Time protection: The missing OS abstraction
EuroSys Conference, Dresden, Germany, March, 2019
Best Paper Award
Abstract Slides Gernot Heiser
Security needs a new hardware-software contract
Keynote at HiPEAC Workshop Secure Hardware, Architectures, and Operating Systems (SeHAS), January, 2019


PDF 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.
Abstract PDF 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
Abstract PDF 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


Abstract PDF 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


Abstract PDF 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


Abstract PDF Yuval Yarom, Qian Ge, Fangfei Liu, Ruby B. Lee and Gernot Heiser
Mapping the Intel last-level cache
The Cryptology ePrint Archive, September, 2015
Abstract PDF 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


Abstract PDF 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
Abstract PDF David Cock
Leakage in trustworthy systems
PhD Thesis, UNSW, Sydney, Australia, August, 2014