Our earlier work on Time Protection
We have evaluated a number of mechanisms that can be used to prevent timing channels. The experience from this work informs our present activities.
Empirical approach
Instruction-based scheduling
|
|
Exynos4412 channel with IBS. Bandwidth = 400 b/s. |
Instruction-based scheduling (IBS), tries to stop an attacker exploiting a channel, by removing any visible clocks: if they can't tell how long something takes, they can't spot the variation caused by a timing-based leak. The attraction of IBS is that it works (in principle) for any channel, while the downside is that to work, we need to remove access to every time source; a restrictive assumption.
IBS is implemented in seL4 by using the performance counters to generate preemption interrupts after a fixed number of instructions. This should, in theory, prevent the use of the preemption tick as a real-time clock.
As the figure on the right demonstrates, however, IBS is only moderately effective on modern processors. While the variation is reduced, there is still clearly a channel. This residual variation is thanks to the imprecise delivery of exceptions, which is getting more variable with every new processor model, and is clearly influenced but sensitive state (here cache misses) but visible to any process on the CPU. Such effects seriously limit the usefulness of IBS.
Cache colouring
|
|
Exynos4412 channel with cache colouring. Bandwidth = 27 b/s. |
A second mitigation strategy, implemented and evaluated in seL4, is cache colouring (CC). This strategy is specific to the cache channel, and relies on exploiting a common feature of set-associative caches to partition the cache between processes.
This partitioning is done on the basis of the physical address of a frame (the details vary between processors). On seL4, all memory allocation is done a user level, and so basic partitioning requires no kernel changes, even to partition dynamically-allocated kernel objects. Some modifications were made to seL4 to permit the kernel stack and code to be partitioned, but these are quite small.
As the figure on the right demonstrates, cache colouring is generally effective in reducing channel bandwidth. Future work on limiting local channel bandwidth in seL4 therefore focuses on cache partitioning and, more generally, resource partitioning.
Scheduled delivery
|
|
OpenSSL 1.0.c response times, before and after SD, contrasted with constant-time OpenSSL 1.0.1e. |
Scheduled delivery (SD) is used to mitigate remote timing channels. The approach here is to precisely delay the delivery of messages using real-time scheduling, in order to mask timing variations that might otherwise leak information. As for colouring, this requires no modification to the seL4 kernel, as all synchronisation (including interrupt delivery) occurs via kernel-controlled endpoints.
The diagram at right shows the effect of SD on the Lucky-13 attack against OpenSSL (vulnerable version 1.0.1c, CVE-2013-0169). Here, a variation in the time required to process two otherwise-indistinguishable packets leaks sensitive information, which can be used as a decryption oracle. The leftmost pair of peaks shows the distribution of response times for the vulnerable version, and the rightmost pair, that for the constant-time reimplementation in OpenSSL 1.0.1e. The centre pair is for SD, and shows that we can mitigate this leak with lower latency cost, and better security (the peaks are more closely matched).
The Formal Approach
We have also considered a formal approach to the problem: can we prove the absence of side channels, in the style of the L4.verified proof. This work is covered in detail in several of the publications listed below, including a verified lattice scheduler.
One major outcome of this line of work is the formalisation of the probabilistic language and verification framework pGCL in Isabelle/HOL, which is now freely available in the archive of formal proofs.