On Sat, 27 Aug 2016 00:36:35 +0000, Gernot.Heiser wrote:
Hi Jonathan,
<snip>
In terms of userspace, I believe I could use something like L4Linux (as long as it is still maintained), and I think there's one supplied, but are there other options? Has anyone ported OpenBSD to it?
L4Linux has always been a Fiasco-based thing. We had our own paravirtualised Linux (called Wombat) in the past, but we have stopped supporting that quite a while ago. There is no point really, given that all mainstream architectures now have virtualisation support that allows you to run unmodified guest binaries at minimal performance penalty. We routinely run Linux on seL4 using hardware-supported virtualisation. OpenBSD should be relatively straightforward.
I disagree with this assessment - in particular, hardware virtualization comes with a large, un-verified, and poorly-secured TCB. This can be seen in the swathes of hardware-level vulnerabilities that have arisen from it: http://danluu.com/cpu-bugs/ The AMD bug called out at the bottom of the article is particularly nasty, as it allowed an unprivileged user in an unprivileged guest to cause arbitrary code execution in host Ring 0. This would undercut seL4's entire security model. As a result, I think it'd be _very_ prudent to continue looking at purely- software, paravirtualized hypervisor implementations, especially for high- assurance systems. <snip>