Formally verified trusted computing base with active security and policy enforcement

A method in a computing device, comprising:

• executing a formally verified microkernel in a most privileged level to abstract hardware resources of the computing device, wherein the formally verified microkernel controls access to the hardware resources using explicit authorization;
• executing a plurality of virtual machine monitors (VMMs), wherein each of the plurality of VMMs runs as a user-level application in a different address space on top of the formally verified microkernel, wherein each of the plurality of VMMs support execution of a different guest operating system running in a different virtual machine (VM), wherein a particular VMM manages interactions between a corresponding VM and hardware resources of the computing device, and wherein the plurality of VMMs are formally verified;
• for each of the plurality of VMMs, continuously monitoring at least a portion of the hardware resources of the computing device including performing virtual machine introspection (VMI) on at least the portion of the hardware resources of the computing device outside of the guest operating system running in the virtual machine corresponding to that VMM;
• determining, from the continuously monitoring, a violation of a policy through one of the quest operating systems running in one of the VMs;
• and
• responsive to the determination of the violation of policy, taking one or more remedial steps, wherein taking the one or more remedial steps includes causing a virtual network policy enforcer to enforce a network policy at a virtual switch executing in the computing device that affects communication of that quest operating system, wherein the virtual network policy enforcer is formally verified.

A non-transitory machine-readable storage medium that provides instructions that, if executed by a processor of a computing device, will cause said processor to carry out the following operations:

• executing a formally verified microkernel in a most privileged level to abstract hardware resources of the computing device, wherein the formally verified microkernel controls access to the hardware resources using explicit authorization;
• executing a plurality of virtual machine monitors (VMMs), wherein each of the plurality of VMMs runs as a user-level application in a different address space on top of the formally verified microkernel, wherein each of the plurality of VMMs support execution of a different guest operating system running in a different virtual machine (VM), wherein a particular VMM manages interactions between a corresponding VM and hardware resources of the computing device, and wherein the plurality of VMMs are formally verified;
• for each of the plurality of VMMs, continuously monitoring at least a portion of the hardware resources of the computing device including performing virtual machine introspection (VMI) on at least the portion of the hardware resources of the computing device outside of the guest operating system running in the virtual machine corresponding to that VMM;
• determining, from the continuously monitoring, a violation of a policy through one of the quest operating systems running in one of the VMs;
• and
• responsive to the determination of the violation of policy, taking one or more remedial steps, wherein taking the one or more remedial steps includes causing a virtual network policy enforcer to enforce a network policy at a virtual switch executing in the computing device that affects communication of that quest operating system, wherein the virtual network policy enforcer is formally verified.