Virtualization is not a security implementation. I've been saying this for years and I'll continue to keep my tinfoil hat on. As Theo DeRaadt said 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. I caugh…
I'm not trying to suggest that a virtualization layer with formal proofs of correctness is a security panacea (it's not--correctness is necessary but not sufficient for security). What I am suggesting is that there is a way forward to developing secure virtualization layers.
If anything, this paper suggests to me that it would be best if the lowest layer in the stack (be it the OS or the hypervisor) implemented some of the crypto primitives on behalf of the applications. I can't see any other way to run them while also guaranteeing that (1) their execution is correct with the specification, (2) they run in full isolation from one another, and (3) they avoid timing attacks and whatever side-channels we can think of.