Oh, I agree with that. It could be a benefit on top of what they have. A Dom0/hypervisor solution from them could actually be safer given they have tools for mathematically verifying both driver interactions and low-level system code. SLAM has been applied to drivers for years now. HyperV was verified with their VCC toolkit. So, they'd be a stronger than average foundation.
The best route for isolation, though, is to apply one of the industry separation kernels or virtualization schemes from CompSci that leave more untrusted. Good news is that I found a great document that describes MILS in detail plus some prior work and terms:
http://www.euromils.eu/downloads/2014-EURO-MILS-MILS-Archite...
GenodeOS is OSS built similar to MILS from European CompSci:
http://genode.org/documentation/general-overview/index