Method and apparatus for statically analyzing a computer program for data dependencies

Claim 2

A computerized method for providing secure information flow in a computer system by analyzing a computer program for data dependencies, comprising the steps of: generating a representation of the computer program by applying a function for transforming the computer program, the representation including a verification condition indicating a relationship between input data including private data to the computer program and an output of the computer program; and evaluating the verification condition using a theorem prover to determine whether the output would depend on the private data if the program were executed; and preventing execution of the program when the evaluation produces a predefined failure result.

Claim 3

The method of claim 1 wherein the representation is a Boolean expression.

Claim 4

The method of claim 1 wherein said steps of generating the representation and evaluating are statically performed before the computer program is executed.

Claim 5

The method of claim 1 wherein the output is independent of the private data when the step of evaluating proves that the verification condition to be true.

Claim 6

The method of claim 1 wherein the output depends on the private data when the step of evaluating proves that the verification condition is false.

Claim 7

The method of claim 1 wherein the verification condition is wlp.S.R.≡<∀h::wlp.S.R> where S represents the program, wlp represents a predefined weakest liberal precondition function, h represents the private data, R represents a set of post-states of the program S, and wlp.S.R represents a predicate that is independent of h when the theorem prover proves that the verification condition evaluates to a logical True value.

Claim 8

The method of claim 6 wherein the verification condition is a first verification condition, the method includes: determining whether the program is non-deterministic, and when the program is non-deterministic applying a second, weakest conservative precondition function to the program to generate a second verification condition: wp.S.true≡<∀h::wp.S.true>, where wp is the weakest conservative precondition function and wp.S.true represents pre-states of the program from which the program terminates; applying a third function to the program to generate a third verification condition: wlp.S.(v≠K)≡<∀h::wlp.S.(v≠K)>, where v is a variable represent the output of the program and K is a value not modified by execution of the program; evaluating the second and third verification conditions with the theorem prover, and logically combining the evaluation of the second and third verification conditions to determine whether the computer program may reveal information about the private data via selective termination of the program based on the private data.

Claim 9

The method of claim 6, wherein the verification condition is a first verification condition, the method includes determining whether the program is non-deterministic, and when the program is non-deterministic applying a second, weakest conservative precondition to the program to generate a second verification condition, evaluating the second verification condition with the theorem prover, and logically combining the evaluation of the first and second verification conditions to determine whether the output of the computer program may depend on the private data.

Claim 10

The method of claim 6, wherein the verification condition is a first verification condition; and representing the computer program as S, representing the output as a variable v, representing the input as a variable h, representing a variable that would be unchanged by an execution of the program as a variable K, and using a formula] the method includes: applying a second function to the program to generate a second verification condition: wlp.S.(v≠K)≡<∀h::wlp.S.(v≠K)>, where v is a variable represent the output of the program and K is a value not modified by execution of the program; evaluating the second verification condition with the theorem prover to determine whether the computer program may reveal information about the private data via selective termination of the program based on the private data; and combining the evaluations of the first and second verification conditions to determine whether to prevent execution of the program.

Claim 11

The method of claim 1 further including the step of: executing the computer program if said step of evaluating indicates that the output does not depend on the private data.

Claim 12

The method of claim 1 wherein the applied function is a weakest liberal precondition.

Claim 13

The method of claim 1 wherein the verification condition is a first verification condition, the method includes determining whether the program is non-deterministic, and when the program is non-deterministic applying a second, weakest conservative precondition to the program to generate a second verification condition, evaluating the second verification condition with the theorem prover, and logically combining the evaluation of the first and second verification conditions to determine whether the output of the computer program may depend on the private data.

Claim 14

The method of claim 1 wherein the applied function uses Hoare logic.

Claim 15

The method of claim 1 wherein the applied function is a strongest post-condition.

Claim 16

The method of claim 1 wherein the applied function uses dynamic logic.

Claim 17

The computerized method of claim 1, wherein the private data is on a local computer, and said steps of generating the representation and evaluating the verification condition are performed on the local computer; and further comprising the steps of: receiving the computer program from a remote computer; and executing the computer program when the evaluating step determines that the output of the computer program does not depend on the private data.

Claim 20

A computer program product for analyzing a computer program for data dependencies to preserve secure information flow, the computer program product for use in conjunction with a computer system, the computer program product comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising: a verification condition generator that generates a representation of the computer program by applying a function for transforming the computer program, the representation including a verification condition indicating a relationship between input data including private data to the computer program and an output of the computer program; a theorem prover receiving the verification condition from the verification condition generator and evaluating the verification condition to determine whether the output would depend on the private data if the program were executed; and instructions for preventing evaluation of the program when the theorem prover produces a failure result.

Claim 21

A computer program product for analyzing a computer program for data dependencies to preserve secure information flow, the computer program product for use in conjunction with a computer system, the computer program product comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising: a verification condition generator that generates a representation of the computer program by applying a function for transforming the computer program, the representation including a verification condition indicating a relationship between input data including private data to the computer program and an output of the computer program; a theorem prover receiving the verification condition from the verification condition generator and evaluating the verification condition to determine whether the output would depend on the private data if the program were executed; and instructions for preventing evaluation of the program when the theorem prover produces a failure result.

Claim 22

The computer program product of claim 18 wherein the verification condition is a first verification condition; the verification condition generator includes instructions for determining whether the program is non-deterministic, and when the program is non-deterministic applying a second, weakest conservative precondition to the program to generate a second verification condition; the theorem prover includes instructions for evaluating the second verification condition; and the computer program product includes instructions for and logically combining the evaluation of the first and second verification conditions to determine whether the output of the computer program may depend on the private data.

Claim 23

The computer program product of claim 18 wherein the verification condition is wlp.S.R≡<∀h::wlp.S.R> where S represents the program, wlp represents a predefined weakest liberal precondition function, h represents the private data, R represents a set of post-states of the program S, and wlp.S.R represents a predicate that is independent of h when the theorem prover proves that the verification condition evaluates to a logical True value.

Claim 24

The computer program product of claim 20 wherein the verification condition is a first verification condition; the verification condition generator includes instructions for determining whether the program is non-deterministic, and when the program is non-deterministic applying a second, weakest conservative precondition function to the program to generate a second verification condition: wp.S.true≡<∀h::wp.S.true>, where wp is the weakest conservative precondition function and wp.S.true represents pre-states of the program from which the program terminates; and applying a third function to the program to generate a third verification condition: wlp.S.(v≠K)≡<∀h::wlp.S.(v≠K)>, where v is a variable represent the output of the program and K is a value not modified by execution of the program; and the theorem prover includes instructions for evaluating the second and third verification conditions with the theorem prover; and the computer program product includes instructions for logically combining the evaluation of the second and third verification conditions to determine whether the computer program may reveal information about the private data via selective termination of the program based on the private data.

Claim 25

The computer program product of claim 20 wherein the verification condition is a first verification condition; the verification condition generator includes instructions for applying a second function to the program to generate a second verification condition: wlp.S.(v≠K)≡<∀h::wlp.S.(v≠K)>, where v is a variable represent the output of the program and K is a value not modified by execution of the program; the theorem prover includes instructions for evaluating the second verification condition to determine whether the computer program may reveal information about the private data via selective termination of the program based on the private data; and the computer program product includes instructions for combining the evaluations of the first and second verification conditions to determine whether to prevent execution of the program.