Paul Karger helped invent information security, pentests, secure coding, high assurance, and so on. He and the other old guard paved the way for the types of systems that survived rigorous pentesting. One of his works was a virtualization product for OpenVMS done because securing full OS's was too hard to achieve.
If we're talking experience and lineage, then we should ignore Theo on this issue immediately as he's never constructed a provably secure system. They don't even address covert channels much less be able to tell me every successful and failed execution trace of their OS w/ argument they obey security policy. Of course, if you look at Karger's design and assurance sections, you'll know the minimum required to get close to secure, predictable operation disqualifies Xen, KVM, VMware, etc from the picture as well.
Only the separation kernels (eg INTEGRITY-178B or LynxSecure), Nizza architecture, GenodeOS, JX OS, CHERIBSD, etc are consistently applying the lessons of the high-assurance community. One of them is that microkernels and core VMM's are the easiest to secure with other stuff running on top mediated by a security policy. Many such systems survived NSA and private pentesting. Monoliths and UNIXen rarely do.
http://lukemuehlhauser.com/wp-content/uploads/Karger-et-al-A...
If we're talking experience and lineage, then we should ignore Theo on this issue immediately as he's never constructed a provably secure system. They don't even address covert channels much less be able to tell me every successful and failed execution trace of their OS w/ argument they obey security policy. Of course, if you look at Karger's design and assurance sections, you'll know the minimum required to get close to secure, predictable operation disqualifies Xen, KVM, VMware, etc from the picture as well.
Only the separation kernels (eg INTEGRITY-178B or LynxSecure), Nizza architecture, GenodeOS, JX OS, CHERIBSD, etc are consistently applying the lessons of the high-assurance community. One of them is that microkernels and core VMM's are the easiest to secure with other stuff running on top mediated by a security policy. Many such systems survived NSA and private pentesting. Monoliths and UNIXen rarely do.