Background on Time Protection

A hardware-mediated timing channel bypasses OS controls.

Definition

Time protection is the prevention of timing channels: unauthorised information flow encoded in the timing of events.

Details

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 draw 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.

Unlike the micro-architectural channels we are mostly concerned about, this is an algorithmic channel.

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.

Any side channel can be exploited as a covert channel (with usually drastically increased bandwidth) but the opposite is not true.

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 and eventually formal verification.

Back