Current computer systems are built in layers. The hardware increasingly has features to support security. Then a hypervisor/VMM is wrapped around the hardware. A guest OS runs on top of the hypervisor. Complex libraries use the OS. And finally the application sits on top of this whole stack. The current approach to building secure systems is to try to make each layer more solid and secure than the one on top. So we’re seeing significant effort going into hardware verification and verification of VMMs and OSs.
I see two problems with this. First, the more layers you have in your system, the more things that can fail and that can be attacked. Second, the real assets we want to protect are at the application layer, all the way on top of the stack. So it’s typically not necessary to subvert the machine all the way to the bottom of the stack. Attack any layer successfully, and you defeat every layer above. So computing platforms offer security that is more like “attack in depth” than “defense in depth”.
I think all the ongoing work on building verifiably correct and secure systems is great stuff. But the ability to build particular existing layers of software securely doesn’t absolve us of thinking about the overall system architecture and the security that is offered when all the components are put together.