Proving the Absence of Microarchitectural Timing Channels

TL;DR

This paper formalizes time protection mechanisms to prevent microarchitectural timing channels, linking hardware and OS security proofs to enhance computer security.

Contribution

It provides a formal framework connecting hardware mechanisms and OS time protection with existing information-flow security proofs.

Findings

Formalization of time protection and hardware mechanisms

Linking hardware and OS security proofs

Enhanced assurance against timing channels

Abstract

Microarchitectural timing channels are a major threat to computer security. A set of OS mechanisms called time protection was recently proposed as a principled way of preventing information leakage through such channels and prototyped in the seL4 microkernel. We formalise time protection and the underlying hardware mechanisms in a way that allows linking them to the information-flow proofs that showed the absence of storage channels in seL4.