You are absolutely deluded, if not stupid, if you think that a worldwide collection of software engineers who can't write operating systems or applications without security holes, can then turn around and suddenly write virtualization layers without security holes.
Instead, "nl2e" should have a data type preventing such a direct copy, and only allowing to test single bits.
The code should then be written to copy bits one by one (for bits where it is appropriate), with a comment for each bit stating why it is safe to copy them.
The fact that this is not the case means that none of the other code in Xen can really be trusted to be bug-free, and there is probably no way to fix that without starting over or doing an equivalent amount of rewriting work.
... I'll say a bit more ... I think it's sad that it's not practical anymore to write really high quality code. And most computer security researchers aren't interested in that anymore either, because it's not possible to force all other developers to write high quality code (and if you do you're called "mean" "alienating" etc.) So all they/we try to do is find new layers to contain all the bad code that has been and will be written.
Can we really be surprised when those layers, particularly if they are popular because they came out first and have lots of features, are also low-quality code? Is there anywhere a foot can be put down?
Also, openbsd is another good example of a project with code with a very very low bug density.
Not the space shuttle, but if you think things that go to space (and land on the goddamned Moon) are free of bugs then you are very sorely mistaken.
[1] http://www.fastcompany.com/28121/they-write-right-stuff/
But it would be especially important to have SOMETHING that can run multiple applications while being 100% sure that it is enforcing security between them.
So far everything has been a total disaster, with browsers getting completely owned every year at Pwn2Own, conventional kernels being effectively expected to be locally exploitable at all times (which means all mobile sandboxes are broken as well), and hypervisors where Xen seems to be the most secure of the ones that are mature, and is still terrible.
No, not even if you're counting in binary.
Of course, the velocity of development is very low, but that's because they want developers who can wrap their head around formal proofs.
I suspect hiring this company would make even a large budget wilt a bit. Just a bit :P
Heck, even without a type system, the problem is that the check is backwards. There shouldn't be a mask of flags that the guest isn't allowed to set, the flags should have been &ed with a mask that says which flags they are allowed to set, that way any new flag would have been disallowed by default.