Trustworthy Systems

The last mile: An empirical study of some timing channels on seL4

Authors

David Cock, Qian Ge, Toby Murray and Gernot Heiser

NICTA

UNSW

Abstract

Storage channels can be provably eliminated in well-designed, high-assurance kernels. Timing channels remain the last mile for confidentiality and beyond the reach of formal analysis for these systems, so must be dealt with empirically. We perform such an analysis, collecting a large amount of data (about 2,000 hours of observations) on two representative timing channels, the locally-exploitable cache channel and a remote exploit of OpenSSL execution timing, on the verified seL4 microkernel. We also evaluate the effectiveness, in terms of reduction of worst-case bandwidth, of a number of black-box mitigation techniques (cache colouring, instruction-based scheduling and deterministic delivery of server responses) across a number of hardware platforms. Our (somewhat unexpected) results show that while these defences were highly effective a couple of processor generations ago, the trend towards imprecise events in modern microarchitectures weaken the defences and introduce new channels. This experience demonstrates the necessity of careful empirical analysis of timing channels.

BibTeX Entry

  @inproceedings{Cock_GMH_14,
    address          = {Scottsdale, AZ, USA},
    author           = {Cock, David and Ge, Qian and Murray, Toby and Heiser, Gernot},
    booktitle        = {ACM Conference on Computer and Communications Security},
    keywords         = {sel4 sidechannels covertchannels timingchannels},
    month            = nov,
    pages            = {570--581},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8295.pdf},
    publisher        = {ACM},
    title            = {The Last Mile: An Empirical Study of Some Timing Channels on {seL4}},
    year             = {2014}
  }

Download