On 29 Jan 2020, at 09:37, Demi M. Obenour <demioben...@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> 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
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
