spectra2

6 ms·

1. 1.▲
   by spectra2 23d ago

   I think a scheme as simple as running two Linux VMs, where you have isolated the services that have real-time guarantees into their own VM, lets you benefit from seL4. This is tangential to your comment, but it's worth mentioning that
2. 2.▲
   by spectra2 23d ago

   Sorry! I didn't read "side-channel" as also referring to microarchitectural timing channels, but mostly to refer to (architectural) storage channels. You are right, it's not covered at all until the experimental Time Pro
3. 3.▲
   by spectra2 23d ago

   I think the danger of a side-channel attack against seL4 is more dangerous than you believe. The security proofs ensure that threads should not be able to read data they do not have permission to, or write to places they do not have permiss
4. 4.▲
   by spectra2 23d ago

   Not all caches are cleared. There are some clever techniques to partition off-core caches (i.e. the L3) as part of the isolation boundaries enforced by the kernel. What I think is particularly exciting is that a new RISCV64 instruction to c