On 2020-01-29 04:17, Heiser, Gernot (Data61, Kensington NSW) wrote:

On 29 Jan 2020, at 09:37, Demi M. Obenour demiobenour@gmail.com wrote:

...

What is the current status of seL4 with respect to Meltdown, Spectre, L1TF, MDS and other CPU vulnerabilities?

Meltdown defence has been implemented on x86 for two years (i.e. as soon as it was announced).

Where manufacturers sell broken hardware we cannot do better than adding workarounds after the fact. And verification has to assume sane behaviour of the hardware.

All the usual timing-channel attacks should be eliminated in a principled fashion, rather than adding workarounds for each published attack. This is the aim of our time-protection work, see https://ts.data61.csiro.au/projects/TS/timingchannels https://ts.data61.csiro.au/projects/TS/timingchannels

Are mitigations for known attacks in place? Obviously, they cannot be perfect, but it would be interesting to re-run the tests with full mitigations for known attacks, and see how much of a channel remains.

This is on-going research. We demonstrated the mechanisms that can do it, and working on

1. turning the mechanisms into a proper system model
2. verifying the implementation against a suitable hardware-software contract
3. getting manufacturers to accept and adhere to such a contract

All three are in progress. (3) is under active discussion at the RISC-V Foundation, with concrete proposals up for discussion probably within months. We hope this will force the hands of the x86 and Arm folks.

Gernot

Is this possible in systems that need to overcommit resources such as CPU and memory? As an example, I often want compiling code to run when, and only when, no other task on the system needs the CPU. In practice, that is most of the time. While overcommitting is a terrible idea in an embedded environment, the situation is different when there is a human who can be told of a resource exhaustion situation and act accordingly.

I am aware that overcommit leads to an unavoidable covert channel. As a user, I usually am okay with cooperating pieces of untrusted code being able to exchange information, since they could do so anyway via the Internet. I am far more worried about malicious code being able to steal information from trusted code. If I ever needed to enforce confinement, I would be fine with statically allocating resources to the confined code.

Also, is it possible to have an unlimited number of protection domains? I can accept a limit on the number of domains that can be executing simultaneously, but web browsers need to support hundreds or even thousands of protection domains. It is okay if switching from one group of executing domains to another is costly, since I expect it to be relatively infrequent.

Sincerely,

Demi