Re: [seL4] Kernel extensions and userspace options

On 30 Aug 2016, at 15:22 , Alex Elsayed wrote:

On Mon, 29 Aug 2016 23:01:45 +0000, Gernot.Heiser wrote:

...

[…]

The only way around this is high-assurance hardware, and this doesn’t come at an affordable cost.

Sure, and I don't disagree. It's part of why I'm so excited by the RISC-V work, especially MIT's progress on formal verification - that, at least, pushes the space problems can occur in down by one more level.

But to a certain extent, I think that there's value in reducing the amount of new API exposed. Furthermore, there's a large body of code exercising the "more conventional" bits in the wild, and a considerably smaller body of code exercising the newer bits. Bugs in the more conventional bits are thus more likely to break existing code - and thus be caught early.

It's not protection in the same sence as high-assurance hardware, no. But at least statistically, from looking at where severe hardware-based security vulnerabilities have cropped up, it seems to be better than the alternative of trusting the hardware virtualization to actually isolate.

The problem is that you don’t really know how the hardware is internally structured, and how modularised what you see as a separate feature really is. In the example you gave, if there’s a hardware bug that gives you privilege escalation from non-root Ring 3 to root Ring 0, what makes you think that the same bug doesn’t let you go from root Ring 3 to root Ring 0, which seems like a smaller step (switching only one mode instead of two)? Root Rings 3+0 is exactly what you’re using when using para-virtualisation. I claim that you cannot have more than zero confidence that hardware that allows the first type of escalation won’t allow the second type. Gernot