# US 11,442,770 B2 · Formally verified trusted computing base with active security and policy enforcement > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 11,442,770 B2 - Document ID: US11442770B2 - Status: Granted - Kind: B2 - Application number: 17/500,728 - Filed: 2021-10-13 - Published: 2022-04-14 - Granted: 2022-09-13 - Earliest claimed: 2020-10-13 - Assignees: BedRock Systems, Inc. - Applicants: BedRock Systems, Inc. - Inventors: Osman Abdoul Ismael; Ashar Aziz; Jonas Pfoh - Web page: https://patentgrep.com/patent/US11442770B2 ## CPC - G06F 9/45558: {Hypervisor-specific management and integration aspects} - G06F 9/45545: {Guest-host, i.e. hypervisor is an application program itself, e.g. VirtualBox} - G06F 9/5077: {Logical partitioning of resources; Management or configuration of virtualized resources (specific details on emulation or internal functioning of virtual machines G06F9/455)} - G06F 9/545: {where tasks reside in different layers, e.g. user- and kernel-space} - G06F 2009/45566: {Nested virtual machines} - G06F 2009/4557: {Distribution of virtual machine instances; Migration and load balancing} - G06F 2009/45583: {Memory management, e.g. access or allocation} - G06F 2009/45587: {Isolation or security of virtual machine instances} - G06F 2009/45591: {Monitoring or debugging support} - G06F 2009/45595: {Network integration; Enabling network access in virtual machine instances} - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## Abstract A formally verified trusted computing base with active security and policy enforcement is described. The formally verified trusted computing base includes a formally verified microkernel and multiple formally verified hyper-processes including a virtual machine monitor (VMM), virtual machine introspection (VMI), policy enforcers including an active security policy enforcer (ASPE), and a virtual switch. The active security and policy enforcement continuously monitors for semantic behavior detection or policy violations and enforces the policies at the virtualization layer. Further, policies can be attached to the network layer to provide granular control of the communication of the computing device. ## Claims ### Claim 1 A computing device, comprising: a plurality of hardware resources including a set of one or more hardware processors, memory, and storage devices, wherein the storage devices include instructions that when executed by the set of hardware processors, cause the computing device to operate a virtualized system, the virtualized system including: a set of one or more virtual machines (VMs) that execute one or more guest operating systems; a formally verified microkernel running 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; and a plurality of formally verified hyper-processes including: a set of one or more virtual machine monitors (VMMs) corresponding to the set of one or more VMs respectively, wherein a particular VMM manages interactions between the corresponding VM and physical resources of the computing device; a set of one or more active security policy enforcers corresponding to the set of one or more VMMs respectively, wherein each active security policy enforcer uses virtual machine introspection (VMI) for introspection of at least some of the hardware resources including one or more hardware processors, wherein each active security policy enforcer enforces a plurality of policies based at least in part on the introspection; and a virtual switch coupled with each of the VMMs, wherein the virtual switch is not directly coupled with any of the set of VMs, wherein a virtual network policy enforcer enforces a set of one or more network policies at the virtual switch that affect communication of the one or more guest operating systems. ### Claim 2 (depends on 1) The computing device of claim 1, wherein policies are dynamically received remotely and installed to the set of one or more active security policy enforcers. ### Claim 3 (depends on 1) The computing device of claim 1, wherein the plurality of formally verified hyper-processes further includes a policy manager that manages policies for the virtualized system. ### Claim 4 (depends on 3) The computing device of claim 3, wherein the policy manager is configured to receive events from the set of active security policy enforcers, and wherein the policy manager is configured to disconnect network access from one of the guest operating systems upon a particular policy violation. ### Claim 5 (depends on 1) The computing device of claim 1, wherein the plurality of formally verified hyper-processes further includes a hardware and firmware policy enforcer. ### Claim 6 (depends on 1) The computing device of claim 1, wherein one of the plurality of policies is a process allow policy that indicates a set of one or more processes that are allowed to be executed by a particular one of the one or more guest operating systems. ### Claim 7 (depends on 1) The computing device of claim 1, wherein at least one of the one or more VMs that executes a guest operating system includes a local active security policy enforcer that can interact with encrypted memory used by the guest operating system. ### Claim 8 (depends on 1) The computing device of claim 1, wherein at least one of the one or more VMs includes a notification agent running in guest user mode space, wherein the notification agent is configured to notify a user of a detected event including a violation of policy. ### Claim 9 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. ### Claim 10 (depends on 9) The method of claim 9, wherein the virtual switch is coupled with the set of one or more virtual machine monitors and is not directly coupled with any VM. ### Claim 11 (depends on 9) The method of claim 9, wherein the policy is configured by an administrator of the computing device. ### Claim 12 (depends on 9) The method of claim 9, wherein the policy is received dynamically from a remote server. ### Claim 13 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. ### Claim 14 (depends on 13) The non-transitory machine-readable storage medium of claim 13, wherein the virtual switch executing in the computing device is coupled with the set of one or more virtual machine monitors and is not directly coupled with any VM. ### Claim 15 (depends on 13) The non-transitory machine-readable storage medium of claim 13, wherein the policy is configured by an administrator of the computing device. ### Claim 16 (depends on 13) The non-transitory machine-readable storage medium of claim 13, wherein the policy is received dynamically from a remote server.