Trustworthy Systems

Towards provable timing-channel prevention


Gernot Heiser, Toby Murray and Gerwin Klein


UNSW Sydney

University of Melbourne


We describe our ongoing research that aims to eliminate microarchitectural timing channels through time protection, which eliminates the root cause of these channels, competition for capacity-limited hardware resources. A proof-of- concept implementation of time protection demonstrated the approach can be effective and low overhead, but also that present hardware fails to support the approach in some aspects and that we need an improved hardare-software con- tract to achieve real security. We have demonstrated that these mechanisms are not hard to provide, and are working on their inclusion in the RISC-V ISA. Assuming compliant hardware, we outline how we think we can then formally prove that timing channels are eliminated.

BibTeX Entry

    author           = {Heiser, Gernot and Murray, Toby and Klein, Gerwin},
    date             = {2020-8-31},
    doi              = {},
    issn             = {0163-5980},
    issue            = {1},
    journal          = {ACM Operating Systems Review},
    keywords         = {sel4 microkernels covert channels information security information leakage protection timing
                        channels formal methods},
    month            = aug,
    pages            = {1-7},
    paperurl         = {},
    publisher        = {ACM},
    title            = {Towards Provable Timing-Channel Prevention},
    volume           = {54},
    year             = {2020}