[seL4] Re: Conclusions regarding speculation

"If people want to improve the hardware, focussing on generic mechanisms such as support for partitioning L2-LL caches would be far more beneficial than point-solutions that will be defeated by the next class of attacks." The path of partitioning some hardware resourse ends up in full partitioning of the computing platform including power supply. It is simpler (almost zero design effort) and the only "reasonably" secure solution. Whenever you share hardware resources, you open the path to side channels. On the other hand, PLUS full computing platform partitioning time protection is a must on each isolated computing platform. So here we have two problems that need to be addressed by different vendors: 1) Time protection, CPU/SoC vendors 2) Computing platform isolation (laptop/servers vendors). Figure out how wonderful would be to have a laptop with X full independent computing platforms inside (fun/work/banking...) and each one based on CPU/SoC solutions with Time Protection. On top of each of those platforms some verified hypervisor/kernel (seL4?). BTW, the step 2 is straight forward, just make laptops a bit bigger and add a screen swich to switch each isolated computing platform. Step 1 requires cpu/SoC vendors more effort and there will be some resilience to sell it. El jue., 9 nov. 2023 23:51, Gernot Heiser via Devel escribió:

On 10 Nov 2023, at 06:03, Demi Marie Obenour wrote:

- Speculative taint tracking provides complete protection against speculative attacks. This is sufficient to prevent leakage of cryptographic key material, even in fully dynamic systems. Furthermore, it is compatible with fast context switches between protection domains.

It’s also a point solution, that provides zero guarantees against unforeseen attacks.

- Full time partitioning eliminates all timing channels, but it is possible only in fully static systems, which severely limits its applicability.

I’m sorry, but this is simply false.

What you need for time protection (I assume this is what you mean with “full time partitioning”) are fixed time slices – ”fixed” in that their length cannot depend on any events in the system that can be controlled by an untrusted domain. It doesn’t mean they cannot be changed as domains come and go.

- Time protection without time partitioning does _not_ fully prevent Spectre v1 attacks, and still imposes a large penalty on protection domain switches.

Time protection does *not* impose a large penalty. Its context-switching cost is completely hidden by the cost of an L1 D-cache flush – as has been demonstrated by published work. And if you don’t flush the L1 cache, you’ll have massive leakage, taint-tracking or not.

Where time protection, *without further hardware support*, does have a cost is for partitioning the lower-level caches. This cost is two-fold:

1) Average cache utilisation is reduced due to the static partitioning (in contrast to the dynamic partitioning that happens as a side effect of the hardware’s cache replacement policy). This cost is generally in the single-digit percentage range (as per published work), but can also be negative – there’s plenty of work that uses static cache partitioning for performance *isolation/improvement*.

2) Memory utilisation is reduced, as colouring implicitly partitions memory. This is the most significant cost, and unavoidable without more hardware support. Intel CAT is one variant of such support (partitions the cache by ways rather than set, which has not effect on memory utilisation, but only works on the LLC, and has itself a performance cost due to reduced cache associativity).

And, of course, without partitioning the lower-level caches you have leakage again, and taint tracking isn’t going to help there either.

If people want to improve the hardware, focussing on generic mechanisms such as support for partitioning L2-LL caches would be far more beneficial than point-solutions that will be defeated by the next class of attacks.

Gernot _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems