Can We Prove Time Protection?

Gernot Heiser, Gerwin Klein, Toby Murray

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, i…