Trustworthy Systems

Towards provable timing-channel prevention

Authors

Gernot Heiser, Toby Murray and Gerwin Klein

DATA61

UNSW Sydney

University of Melbourne

Abstract

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

  @article{Heiser_MK_20,
    author           = {Heiser, Gernot and Murray, Toby and Klein, Gerwin},
    date             = {2020-8-31},
    doi              = {https://doi.org/10.1145/3421473.3421475},
    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         = {https://trustworthy.systems/publications/full_text/Heiser_MK_20.pdf},
    publisher        = {ACM},
    title            = {Towards Provable Timing-Channel Prevention},
    volume           = {54},
    year             = {2020}
  }

Download