Skip to main content

Timing Channels

Timing Channels

A timing Channel based on cache contention

A hardware-mediated timing channel bypasses OS controls.

Timing Channels is an activity of the Trustworthy Systems project.

Aim

Analysis of timing channels in security-critical, componentised systems and development of effective, light-weight operating-system mechanisms for their avoidance.

Highlights

Background

Side channels

The term side channel refers to the leakage of sensitive information over an unanticipated channel. A common case of interest is correlation of system response time (i.e. a timing channel) or power consumption with a cryptographic key.

As a trivial example of a remotely-exploitable timing channel, consider the following possible implementation of strcmp(), a C library routine used to test strings for equality:

int
strcmp(char *s1, char *s2) {
  for (; *s1; s1++) {
    if (*s1 != *s2) return *s1 - *s2;
  }
  return 0;
}

The runtime of this fragment is roughly proportional to the number of characters in the string prefixes which match. If one of the strings represents a secret (e.g. a password) and the other is known to the attacker (e.g. the user-supplied password), the secret will be revealed in short order. This behaviour is consistent with recent versions of the GNU C library.

Covert channels

Covert channels, in contrast, are those that are actively exploited by some untrustworthy agent (e.g. a trojan) to bypass the barriers enforced by system protection mechanisms. As a result, tunnels are created that allow information leakage between isolated protection domains. Processes from different protection domains can then transmit information through these tunnels, which allows an insider process (sender) from a domain to actively leak secrets to an outsider process (receiver) in another domain.

Unmitigated Exynos4 cache channel

Exynos4412 cache channel, unmitigated. B = 2,400 b/s. Colour gives probability.

Storage vs. Timing Channels

A storage channel is a (side or covert) channel that transmits data through some explicit element of the machine or system state, e.g. a register, a shared memory location, or some kernel state such as the scheduler queue. Existing work on seL4 has demonstrated that these channels can be provably eliminated in a minimal, carefully-constructed system.

Timing channels, on the other hand, are invisible to traditional specification methods, as time is not modelled. They are therefore not covered by the seL4 proof, and must be dealt with empirically. We thus consider methods that are not only low-overhead (there should be little or no cost for a system that doesn't employ them), but amenable to empirical validation.

What we are trying to achieve

The goal of this project is to investigate practical and efficient mitigation techniques for timing-based side channels and covert channels. We are particularly interested in attacks that target valuable secrets (e.g. encryption keys), and are practical on co-tenant (cloud) systems, as well as military-style cross-domain soluations. A motivating example is the known set of attacks against AES, which exploit the use of lookup tables to implement s-boxes. For this reason, our first efforts have been against the cache channel, which is generally the highest-bandwidth channel.

The figure at right demonstrates the magnitude of the problem, on a fairly recent ARM processor (Cortex A9, common in mobile phones as of 2014). Here, we have two notionally isolated processes, the sender and the receiver. The sender varies the size of its working set (and hence its cache footprint) along the horizontal axis, while the relative performance of a memory-bound task performed by the receiver is plotted on the vertical axis. As the sender dirties more and more of the cache, the receiver executes more and more slowly. The effect can be trivially exploited to transfer data (here at 2.4kb/s, as the processes do not execute concurrently).

As far as possible, we treat a sensitive component (one that handles a secret), as a black box. The principal advantage of this approach is to minimise the analysis and modification required in building a secure system from components.

Our work to date suggests that rather than injecting noise, to try to mask a side-channel signal, it is much more effective to eliminate the signal variation that the channel exploits: to increase determinism.

We take two parallel approaches to the problem: an empirical approach, where we make extensive experimental measurements for prototype implementations, and a formal approach, where we attempt to verify probabilistic properties of systems code, including the bandwidth of side or covert channels. We explain the empirical work first.

The Empirical Approach

There are three techniques that we have analysed (in the context of seL4) to date:

Instruction-based scheduling
Exynos4 channel with IBS

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
Cache coloured Exynos4 channel

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
Lucky-13 attack mitigated with 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.

Contacts

Qian Ge, qian.ge<at>nicta.com.au

People

To appear

Abstract PDF Qian Ge, Yuval Yarom, David Cock and Gernot Heiser
A survey of microarchitectural timing attacks and countermeasures on contemporary hardware
Journal of Cryptographic Engineering
Abstract PDF Gernot Heiser
For safety’s sake: we need a new hardware-software contract!
IEEE Design and Test

2016

Abstract PDF Fangfei Liu, Qian Ge, Yuval Yarom, Frank Mckeen, Carlos Rozas, Gernot Heiser and Ruby B Lee
CATalyst: defeating last-level cache side channel attacks in cloud computing
IEEE Symposium on High-Performance Computer Architecture, pp. 406-418, Barcelona, Spain, March, 2016

2015

Abstract PDF Yuval Yarom, Qian Ge, Fangfei Liu, Ruby B. Lee and Gernot Heiser
Mapping the Intel last-level cache
The Cryptology ePrint Archive, September, 2015
Abstract PDF Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser and Ruby B Lee
Last-level cache side-channel attacks are practical
IEEE Symposium on Security and Privacy, pp. 605-622, San Jose, CA, US, May, 2015

2014

Abstract PDF David Cock, Qian Ge, Toby Murray and Gernot Heiser
The last mile: An empirical study of some timing channels on seL4
ACM Conference on Computer and Communications Security, pp. 570-581, Scottsdale, AZ, USA, November, 2014
Abstract PDF David Cock
Leakage in trustworthy systems
PhD Thesis, UNSW, Sydney, Australia, August, 2014
Abstract PDF David Cock
From probabilistic operational semantics to information theory - side channels with pGCL in isabelle
Proceedings of the 5th International Conference on Interactive Theorem Proving, pp. 1–15, Vienna, Austria, July, 2014

2013

Abstract PDF David Cock
Practical probability: Applying pGCL to lattice scheduling
Proceedings of the 4th International Conference on Interactive Theorem Proving, pp. 1–16, Rennes, France, July, 2013

2012

Abstract PDF David Cock
Verifying probabilistic correctness in Isabelle with pGCL
Proceedings of the 7th Systems Software Verification, pp. 1–10, Sydney, Australia, November, 2012

2011

Abstract PDF David Cock
Exploitation as an inference problem
4th Workshop on Artificial Intelligence and Security, pp. 105–106, Chicago, IL, USA, October, 2011

Served by Apache on Linux on seL4.