Verification of trusted threat-aware microvisor

Patent metadata

Field	Value
Publication number	US-2016004869-A1
Application number	US-201514615798-A
Country	US
Kind code	A1
Filing date	Feb 6, 2015
Priority date	Jul 1, 2014
Publication date	Jan 7, 2016
Grant date	—

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.

First claim

What is claimed is:

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.

2 . The method of claim 1 wherein the microvisor is configured to enable rapid compliance testing.

3 . The method of claim 1 wherein initiating the state dump of the executable operational model and initiating the corresponding state dump of the microvisor occur without human intervention.

4 . The method of claim 1 wherein conformance of the microvisor to the security property is verified when the predetermined number of matched states form a sufficient test coverage between the executable operational model and the microvisor.

5 . The method of claim 1 wherein verifying the security property is performed on a theorem prover.

6 . The method of claim 3 wherein the executable operational model initiates on-demand the state dump of the operational model and the corresponding state dump of the microvisor.

7 . The method of claim 1 wherein the microvisor includes a function to enable capture each respective state of the microvisor.

8 . The method of claim 1 wherein a theorem prover verifies a plurality of security properties of the operational model using Hoare logic.

9 . The method of claim 1 wherein trustedness of the microvisor increases monotonically with an amount of compliance testing.

10 . The method claim 1 wherein the predetermined level of confidence is appropriate for the deployment of the microvisor in the network.

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.

12 . The system of claim 11 wherein the microvisor is configured to enable rapid compliance testing.

13 . The system of claim 11 wherein initiating the state dump of the executable operational model and initiating the corresponding state dump of the microvisor occur without human intervention.

14 . The system of claim 11 wherein conformance of the microvisor to the security property is verified when the predetermined number of matched states form a sufficient test coverage between the executable operational model and the microvisor.

15 . The system of claim 11 wherein verifying the security property is performed on a theorem prover.

16 . The system of claim 13 wherein the executable operational model initiates on-demand the state dump of the operational model and the corresponding state dump of the microvisor.

17 . The system of claim 11 wherein the microvisor includes a function to enable capture of each respective state of the microvisor.

18 . The system of claim 11 wherein a theorem prover verifies a plurality of security properties of the operational model using Hoare logic.

19 . The system of claim 11 wherein the predetermined level of confidence is appropriate for the deployment of the microvisor in the network.

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.

Assignees

• Fireeye Inc

Inventors

• Ismael Osman Abdoul
• Tews Hendrik

Classifications

• G06F21/577 Primary

  Assessing vulnerabilities and evaluating computer system security · CPC title

• G06F2221/034

  Test or assess a computer or a system · CPC title