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.

翻译：微架构时序信道是计算机安全的主要威胁。最近，一组称为时间保护的操作系统机制作为一种阻止通过此类信道泄露信息的原则性方法被提出，并在seL4微内核中实现了原型。我们对时间保护及底层硬件机制进行了形式化，使其能够与已证明seL4中不存在存储信道的信息流证明建立关联。