Re:
------------------------------
Date: Mon, 29 Aug 2016 23:01:45 +0000
From: <Gernot.Heiser@data61.csiro.au>
<snip>
You may *think* that the manufacturers don?t make changes to the more conventional bits of the hardware, and thus they are ?correct", but that isn?t true, of course. And on top of that we know that there are intentional backdoors in commercial hardware.
The only way around this is high-assurance hardware, and this doesn?t come at an affordable cost.

I think it?s an illusion to think one can partition hardware into trusted and untrusted bits. In the end, the OS is at the mercy of the hardware, if it?s faulty then you lose, there?s no way around it.

A key attraction of seL4 is the trustworthiness of the microkernel. Running it on hardware with known bugs or features (e.g. recent Intel CPUs) that compromise the kernel's trustworthiness counteracts the perceived advantages.

Perhaps, it would be possible to list CPUs (and possibly boards) that are recognised for being free of known potential attack vectors.

I would certainly not want to invest time and effort into making seL4 run on hardware that could have be reasonably known to be of low assurance.