The Last Mile: An Empirical Study of Some Timing Channels on seL4

Select |




Print


Cock, David; Ge, Qian; Murray, Toby; Heiser, Gernot

Cock, David; Ge, Qian; Murray, Toby; Heiser, Gernot


2014-11-03


Conference Material


ACM Conference on Computer and Communications Security (CCS)


Scottsdale, AZ, USA


570-581


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.


seL4 sidechannels covertchannels timingchannels


http://www.sigsac.org/ccs/CCS2014/


nicta:8295


Cock, David; Ge, Qian; Murray, Toby; Heiser, Gernot. The Last Mile: An Empirical Study of Some Timing Channels on seL4. In: ACM Conference on Computer and Communications Security (CCS); Scottsdale, AZ, USA. 2014-11-03. 570-581.



Loading citation data...

Citation counts
(Requires subscription to view)