Safe to execute verification of software
First Claim
1. A computer-implemented method of verifying that untrusted software supplied by a code producer is safe to execute by a code consumer, comprising the steps of:
- defining a safety policy that specifies safe operating conditions of the untrusted software on the code consumer;
generating a safety predicate for the untrusted software that determines if execution by the code consumer of the untrusted software will violate said safety policy;
generating a safety proof that proves that said safety predicate is valid; and
validating the untrusted software for execution based on said safety proof and said safety predicate prior to execution of the untrusted software.
0 Assignments
0 Petitions
Accused Products
Abstract
A computer-implemented method of verifying that untrusted software supplied by a code producer is safe to execute by a code consumer. The method includes the step of defining a safety policy that specifies safe operating conditions of the untrusted software on the code consumer. The method also includes the steps of generating a safety predicate for the untrusted software that determines if execution by the code consumer of the untrusted software will violate said safety policy and generating a safety proof that proves that said safety predicate is valid. The method further includes the step of validating the untrusted software for execution based on said safety proof and said safety predicate.
-
Citations
29 Claims
-
1. A computer-implemented method of verifying that untrusted software supplied by a code producer is safe to execute by a code consumer, comprising the steps of:
-
defining a safety policy that specifies safe operating conditions of the untrusted software on the code consumer; generating a safety predicate for the untrusted software that determines if execution by the code consumer of the untrusted software will violate said safety policy; generating a safety proof that proves that said safety predicate is valid; and validating the untrusted software for execution based on said safety proof and said safety predicate prior to execution of the untrusted software. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8)
-
-
9. An apparatus for verifying that software supplied by a code producer is safe to execute by a code consumer, comprising:
-
a predicate generator module responsive to annotated untrusted software, said generator module for generating a safety predicate; a proof generator module responsive to said safety predicate, said proof generator module for generating a safety proof; and a proof checker module responsive to said safety predicate and said safety proof, said proof checker module for verifying that said safety predicate complies with a safety policy defined by the code consumer prior to execution of the software. - View Dependent Claims (10)
-
-
11. An apparatus for verifying that software supplied by a code producer is safe to execute by a code consumer, comprising:
-
means for generating a safety predicate for untrusted software; means for generating a safety proof from said safety predicate; and means for verifying that said safety predicate complies with a safety policy defined by the code consumer based on said safety predicate and said safety proof prior to execution of the untrusted software.
-
-
12. A computer system, comprising:
-
a processor; at least one input device for receiving untrusted software; a communication link enabling communications between said processor and said input device; and a memory coupled to said processor and storing a set of ordered data and a set of instructions which, when executed by said processor, cause said processor to perform the steps of; generating a safety predicate for said untrusted software for determining if execution by a code consumer of said untrusted software will violate a safety policy defined by said code consumer; generating a safety proof that proves that said safety predicate is valid; and validating said untrusted software for execution based on said safety proof and said safety predicate prior to execution of the untrusted software. - View Dependent Claims (13, 14, 15, 16, 17, 18, 19)
-
-
20. A computer-readable medium having stored thereon instructions which, when executed by a processor, cause said processor to perform the steps of:
-
generating a safety predicate for determining if execution by a code consumer of untrusted software will violate a safety policy defined by said code consumer; generating a safety proof that proves that said safety predicate is valid; and validating said untrusted software for execution based on said safety proof and said safety predicate prior to execution of the untrusted software. - View Dependent Claims (21, 22, 23, 24, 25, 26, 27)
-
-
28. A computer-readable medium having stored thereon instructions which, when executed by a code consumer, cause said code consumer to perform the steps of:
-
defining a safety policy that specifies safe operating conditions of untrusted software on the code consumer; generating a safety predicate that determines if execution by the code consumer of said untrusted software will violate said safety policy; and validating said untrusted software for execution based on a safety proof and said safety predicate prior to execution of untrusted software.
-
-
29. A computer-readable medium having stored thereon instructions which, when executed by a proof producer, cause said proof producer to perform the step of explicitly generating a safety proof that proves that a safety predicate is valid prior to execution of untrusted software.
Specification