# Can We Prove Time Protection?

## TL;DR

This paper explores the feasibility of formally proving time protection in operating systems to prevent timing channels, building on a recent implementation in seL4 and using abstract hardware models.

## Contribution

It introduces a formal reasoning approach for verifying time protection mechanisms in microkernels to mitigate timing channels.

## Key findings

- Proposed a formal proof approach for time protection
- Analyzed the abstraction of hardware resources for security guarantees
- Connected implementation in seL4 to formal verification methods

## Abstract

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.