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.
@article{arxiv.2310.17046,
title = {Proving the Absence of Microarchitectural Timing Channels},
author = {Scott Buckley and Robert Sison and Nils Wistoff and Curtis Millar and Toby Murray and Gerwin Klein and Gernot Heiser},
journal= {arXiv preprint arXiv:2310.17046},
year = {2023}
}
Comments
Scott Buckley and Robert Sison were joint lead authors