Verification of trusted threat-aware visualization layer
A trusted threat-aware microvisor may be deployed as a module of a trusted computing base (TCB). The microvisor is illustratively configured to enforce a security policy of the TCB, which may be implemented as a security property of the microvisor. The microvisor may manifest (i.e., demonstrate) the security property in a manner that enforces the security policy. Trustedness denotes a predetermined level of confidence that the security property is demonstrated by the microvisor. The predetermined level of confidence is based on an assurance (i.e., grounds) that the microvisor demonstrates the security property. Trustedness of the microvisor may be verified by subjecting the TCB to enhanced verification analysis configured to ensure that the TCB conforms to an operational model with an appropriate level of confidence over an appropriate range of activity. The operational model may then be configured to analyze conformance of the microvisor to the security property. A combination of conformance by the microvisor to the operational model and to the security property provides assurance (i.e., grounds) for the level of confidence and, thus, verifies trustedness.
1. A method comprising:
collecting state information associated with an operational model associated with a code base of a virtualization layer, the virtualization layer being configured to execute on a node including a processor and an operation system, to control access permissions to resources of the node;
collecting state information associated with the code base of the virtualization layer, the code base of the virtualization layer includes a function to enable capture of the state information associated with the code base of the virtualization layer by at least initiating a state dump of the code base;
iteratively comparing state information of the operational model and the state information of the code base of the virtualization layer; and
continuing iterative comparison of the state information of the operational model and the state information of the code base of the virtualization layer until a predetermined number of states match, wherein the predetermined number of matched states signifies a level of confidence of a security property being implemented by the code base of the virtualization layer.
2. The method of claim 1 wherein conformance of the code base of the virtualization layer to a security policy represented by one or more security properties including the security property is verified when the predetermined number of states of the operational model resulting from a state dump of the operational model match states of the code base of the virtualization layer resulting from the state dump of the code base.
3. The method claim 2 , wherein the virtualization layer enforces the security policy of the code base and a trustedness of the virtualization layer is based on the level of confidence of the security property being implemented by the code base of the virtualization layer.
4. The method of claim 2 , wherein a determination of the security property being implemented by the code base of the virtualization layer identifies compliance by the virtualization layer to a security policy represented at least in part by the security property.
5. The method of claim 1 , wherein the function to enable capture of each respective state of the code base of the virtualization layer after a number of instructions of the code base of the virtualization layer have executed.
6. The method of claim 1 , wherein the code base of the virtualization layer is configured for rapid compliance testing by the function of the code base of the virtualization layer initiating the state dump of the code base of the virtualization layer being in communication with the operational model.
7. The method of claim 1 , wherein trustedness of the code base of the virtualization layer is defined in terms of manifesting security properties including manifesting a first security property in the code base of the virtualization layer, the first security property operating as a static attribute representing no inherent security flaw in the code base of the virtualization layer.
8. The method of claim 1 , wherein the trustedness of the code base of the virtualization layer is further defined in terms of manifesting a second security property while the code base of the virtualization layer executes, the second security property operating as a dynamic attribute representing no alteration of the code base of the virtualization layer by an exploit.
9. The method of claim 1 further comprising:
maintaining trustedness of the code base of the virtualization layer by at least loading the virtualization layer for execution where the virtualization layer is executed as a first software module loaded into a memory of the node during a boot process.
10. The method of claim 9 , wherein the trustedness of the code base of the virtualization layer is further maintained by at least loading a root task of a trusted computing base for execution prior to any other software module other than the virtualization layer, the trusted computing base includes the virtualization layer and the root task.
11. The method of claim 1 , wherein the virtualization layer is a light-weight module disposed or layered beneath the operating system executing on the node to control privileges to the resources.
12. The method of claim 1 , wherein the collecting of the state information associated with the operational model is conducted by at least initiating a state dump of the operational model.
13. A system comprising:
a central processing unit (CPU) to execute a code base of a virtualization layer operating to control access permissions to resources of the system;
a memory configured to store the code base of the virtualization layer as a computing base, the computing base is associated with one or more security properties including a first security property verified by the system configured to:
collect state information associated with an operational model by at least initiating a state dump of the state information associated with the operational model;
collect state information associated with the code base of the virtualization layer by at least initiating a state dump of the state information associated with the code base of the virtualization layer;
iteratively compare the state information associated with the operational model and the state information associated with the code base of the virtualization layer; and
continue iterative comparison of states being part of the state information associated with the operational model and states being part of state information associated with the code base of the virtualization layer until a predetermined number of the states match, wherein the predetermined number of matched states correspond to a predetermined level of confidence that the first security property is implemented by the code base of the virtualization layer.
14. The system of claim 13 , wherein the operational model specifies a behavior of the code base of the virtualization layer as modeled in a functional programming language.
15. The system of claim 13 , wherein the initiating of the state dump of the state information associated with operational model and the initiating of the corresponding state dump of the state information associated with the code base of the virtualization layer occur without human intervention.
16. The system of claim 13 , wherein conformance of the code base of the virtualization layer to the first security property is verified when the predetermined number of the states of the operational model match the states of the code base of the virtualization layer.
17. A non-transitory computer readable medium including program instructions for execution on a processor of a node configured to be communicatively coupled a network, the program instructions configured to:
collect state information associated with an operational model for modules of a code base;
collect state information associated with the modules, wherein the code base comprises a function configured to initiate a state dump of the modules being in communication with the operational model to collect the state information;
iteratively compare the state information associated with the operational model and the state information associate with the modules; and
continue iterative comparison of the state information associated with the operational model and the state information associated with the modules until a predetermined number of the states match, wherein the predetermined number of matched states signifies a level of confidence of a security property being implemented by the code base and a compliance with a security policy represented at least in part by the security property.
18. The non-transitory computer readable medium of claim 17 , wherein the operational model specifies a behavior of the modules and is created in a functional programming language.
19. The non-transitory computer readable medium of claim 17 , wherein the code base includes a code base of a virtualization layer that is configured to execute on the node to control access permissions to resources of the node.
20. The non-transitory computer readable medium of claim 19 , wherein trustedness of the code base of the virtualization layer increases monotonically with an amount of compliance testing.
21. The non-transitory computer readable medium of claim 19 wherein trustedness of the code base of the virtualization layer is defined in terms of manifesting security properties including manifesting a first security property in the code base of the virtualization layer operating as a static attribute representing no inherent security flaw in the code base of the virtualization layer and manifesting a second security property while the code base of the virtualization layer executes thereby operating as a dynamic attribute representing no alteration of the code base of the virtualization layer by an exploit.
22. The non-transitory computer readable medium of claim 17 , wherein the program instructions are configured to initiate the state dump of the operational model to collect the state information associated with the operational model and initiate a corresponding state dump of the modules without human intervention.
23. The non-transitory computer readable medium of claim 17 , wherein a theorem prover, being a portion of the program instructions, is configured to verify a plurality of security properties of the operational model, including the security property, using Hoare logic.