VERIFICATION OF TRUSTED THREAT-AWARE MICROVISOR
First Claim
1. A method comprising:
- verifying a security property for an operational model of a microvisor adapted for deployment in a node of a network, wherein the operational model is created in a functional programming language;
generating an executable of the operational model;
initiating a state dump of the executable operational model;
initiating a corresponding state dump of the microvisor;
iteratively comparing the states of the executable operational model and the microvisor; and
continuing iterative comparison of the states of the executable operational model and the microvisor until a predetermined number of the states match, wherein the predetermined number of matched states correspond to a predetermined level of confidence that the security property is implemented by the microvisor.
5 Assignments
0 Petitions
Accused Products
Abstract
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.
156 Citations
20 Claims
-
1. A method comprising:
-
verifying a security property for an operational model of a microvisor adapted for deployment in a node of a network, wherein the operational model is created in a functional programming language; generating an executable of the operational model; initiating a state dump of the executable operational model; initiating a corresponding state dump of the microvisor; iteratively comparing the states of the executable operational model and the microvisor; and continuing iterative comparison of the states of the executable operational model and the microvisor until a predetermined number of the states match, wherein the predetermined number of matched states correspond to a predetermined level of confidence that the security property is implemented by the microvisor. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10)
-
-
11. A system comprising:
-
a central processing unit (CPU) adapted to execute a trusted microvisor for deployment in a network; a memory configured to store the trusted microvisor as a trusted computing base, the trusted computing base having a security property verified by a test computing environment configured to; verify the security property for an operational model of the microvisor, wherein the operational model is created in a functional programming language; generate an executable of the operational model; initiate a state dump of the executable operational model; initiate a corresponding state dump of the microvisor; iteratively compare the states of the operational model and the microvisor; and continue iterative comparison of the states of the executable operational model and the microvisor until a predetermined number of the states match, wherein the predetermined number of matched states correspond to a predetermined level of confidence that the security property is implemented by the microvisor. - View Dependent Claims (12, 13, 14, 15, 16, 17, 18, 19)
-
-
20. A non-transitory computer readable medium including program instructions for execution on a processor of a node on a network, the program instructions when executed operable to:
enforce a security property of a trusted microvisor of the node, the trusted microvisor having a security property verified by a test computing environment configured to; verify the security property for an operational model of the microvisor, wherein the operational model is created in a functional programming language; generate an executable of the operational model; initiate a state dump of the executable operational model; initiate a corresponding state dump of the microvisor; iteratively compare the states of the executable operational model and the microvisor; and continue iterative comparison of the states of the executable operational model and the microvisor until a predetermined number of the states match, wherein the predetermined number of matched states correspond to a predetermined level of confidence that the security property is implemented by the microvisor.
Specification