On 30 Aug 2016, at 14:08 , Tyga mailto:cyberfonic@gmail.com> wrote: Re: ------------------------------ Date: Mon, 29 Aug 2016 23:01:45 +0000 From: mailto: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. such a list would be nice, although it might be empty. Anything that’s not from a trusted foundry likely has a deliberate backdoor, besides any bugs it might have. In any case, our expertise is not on finding hardware bugs, there are others who are better at that. We’re obviously interested learning in what is known to be buggy... Gernot