Very accessible paper. They took the seL4 kernel, implemented a series of mitigations against timing leaks, and showed that their performance impact is tolerabl

Very accessible paper. They took the seL4 kernel, implemented a series of mitigations against timing leaks, and showed that their performance impact is tolerable and less than one might think. While some of these mitigations have seen common use, their chief innovation is the on-demand cloning of (the majority of) global kernel data and state, which reduces resource sharing and allows the other partition and padded-flush mitigations to work better. While they acknowledge that doing the same in a larger and differently-designed kernel would be a big undertaking, they also note that the hardware's uneven support and seeming lack of a formal mental model about this topic is unfortunate. Both software and hardware work would benefit from a focused approach in this area.