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.
Great they're getting on it. I'll note that the early security kernels attempted to mitigate timing channels. GEMSOS used event counts and sequences IIRC. It was also mandatory for high-assurance security under TCSEC regulations to look for them and try to mitigate them. There was no reason to think it would actually work over time at the rate bypasses were discovered. They were trying, though.
More recently, under the MILS model for partitioning kernels, they've applied stuff like ARINC time and space partitioning to separation kernels for both safety- and security-critical applications. Big in aerospace for DO-178C regulations. One example [1] describing some timing protections. That can mitigate some timing channels. The one good thing about Meltdown/Spectre's publicity is CompSci folks are coming up with all kinds of stuff on this problem.
I actually support additional, cache-isolated, //USER OWNED// TPM / enclave like solutions for running the hardened parts of software (handling of actual keys/etc). 99% of the other work is better off picking the speed or power efficiency options.
(Edit to clarify User Owned: The end user should trust the computer, not anyone else, therefore they should be the one with full control, not any vendor or imaginary property creator.)
I highly recommend looking into the KeyKOS operating system, which allows time and space resource usage to be controlled via a common abstraction of authority (keys/capabilities) - and that recursively.
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.