  Timing channels are a significant and growing security threat in computer
systems, with no established solution. We have recently argued that the OS must
provide time protection, in analogy to the established memory protection, to
protect applications from information leakage through timing channels. Based on
a recently-proposed implementation of time protection in the seL4 microkernel,
we investigate how such an implementation could be formally proved to prevent
timing channels. We postulate that this should be possible by reasoning about a
highly abstracted representation of the shared hardware resources that cause
timing channels.
