Last Mile
References:
The Last Mile: An empirical study of timing channels on seL4,
Leakage in Trustworthy Systems, by David Cock, August 2014.
Overview
Side channel data collection.
seL4 on Exynos4412 platform:
Scope
serverl timing channels on seL4 based system with their defenses with low overhead.
Do not consider noise-adding solutions (due to their overhead);
Only consider black box techniques (require no insight into the internals of software running on seL4, as retrofitting security into complex software is generally impossible);
Only on some example cases, not a comprenhensive converage of timing channels;
Two vulnerabilities:
- One local vul + two countermeasures:
- the cache-contention channel
- high bandwidth
- e.g. cloud: learn encryption keys [Zhang et al., 2012]
- instruction-based scheduling [Stefan et al., 2013]
- cache colouring [Liedtke et al., 1997]
- One remote vul:
- Lucky 13 attack of AlFardan and Paterson [2013] against DTLS in OpenSSL 1.0.1c.
More
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?